Stack: Difference between revisions
Content added Content deleted
| Line 980: | Line 980: | ||
(* Create an empty nonlinear stack. *) |
(* Create an empty nonlinear stack. *) |
||
fn {} |
fn {} |
||
stack_t_nil () |
stack_t_nil {t : t@ype} () :<> stack_t (t, 0) = |
||
list_nil () |
|||
(* Create an empty linear stack. *) |
(* Create an empty linear stack. *) |
||
fn {} |
fn {} |
||
stack_vt_nil () |
stack_vt_nil {vt : vt@ype} () :<> stack_vt (vt, 0) = |
||
list_vt_nil () |
|||
(* Is a nonlinear stack empty? *) |
(* Is a nonlinear stack empty? *) |
||