
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)