Content deleted Content added
|
|
|
(lst : sorted_entier_list n)
:<prf> [0 <= n] void
(*
extern fn
sorted_entier_list_length
{n : int}
(lst : sorted_entier_list n)
:<> [0 <= n] int n
*)
extern fn
| SNIL => ()
| _ ::: _ => ()
(*
implement
sorted_entier_list_length {n} lst =
(* This implementation is tail-recursive. *)
let
fun
count {m : nat | m <= n} .<n - m>.
(lst : sorted_entier_list (n - m),
m : int m)
:<> [0 <= n] int n =
case+ lst of
| SNIL => m
| _ ::: tail => count {m + 1} (tail, succ m)
prval () = lemma_sorted_entier_list_param lst
in
count (lst, 0)
end
*)
implement
|
