Module Stack

Meta-data

Contents

pop : forall {n : Nat, a : Type} 
    . Vec (n + 1) a -> (a, Vec n a)
Pop most recently added item from the stack
push : forall {n : Nat, a : Type} 
     . a -> Vec n a -> Vec (n + 1) a
Push item onto the stack
peek : forall {n : Nat, a : Type} 
     . (Vec (n + 1) a) [1..2] -> (a, Vec (n + 1) a)
Pop the most recent item from the stack without removing it
peek' : forall {m : Ext Nat, a : _ka, n : Nat} 
      . Vec (n + 1) (a [m..(m + 1)]) -> (a, Vec (n + 1) (a [m..m]))

peek'' : forall {n : Nat, a : Type} 
       . Vec (n + 1) (a [1..2]) -> (a, Vec (n + 1) a)