20 lines
662 B
Text
20 lines
662 B
Text
|
(* The Rosetta Code linear list type can contain any vt@ype.
|
|||
|
|
(The ‘@’ means it doesn’t have to be the size of a pointer.
|
|||
|
|
You can read {0 <= n} as ‘for all non-negative n’. *)
|
|||
|
|
dataviewtype rclist_vt (vt : vt@ype+, n : int) =
|
|||
|
|
| rclist_vt_nil (vt, 0)
|
|||
|
|
| {0 <= n} rclist_vt_cons (vt, n + 1) of (vt, rclist_vt (vt, n))
|
|||
|
|
|
|||
|
|
(* A lemma one will need: lists never have negative lengths. *)
|
|||
|
|
extern prfun {vt : vt@ype}
|
|||
|
|
lemma_rclist_vt_param
|
|||
|
|
{n : int}
|
|||
|
|
(lst : !rclist_vt (vt, n)) :<prf> [0 <= n] void
|
|||
|
|
|
|||
|
|
(* Proof of the lemma. *)
|
|||
|
|
primplement {vt}
|
|||
|
|
lemma_rclist_vt_param lst =
|
|||
|
|
case+ lst of
|
|||
|
|
| rclist_vt_nil () => ()
|
|||
|
|
| rclist_vt_cons _ => ()
|