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)