Commit 5e956b50 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

added theory list.ListRich

parent 854a61f0
......@@ -4,11 +4,7 @@ module M
Problem 5: amortized queue *)
use import int.Int
use export list.List
use export list.Length
use export list.Append
use export list.Reverse
use export list.HdTl
use export list.ListRich
type queue 'a = Q (front : list 'a) (lenf : int)
(rear : list 'a) (lenr : int)
......@@ -58,9 +58,13 @@ theory HdTl "head and tail"
| Cons _ t -> Some t
(* TODO: move these lemmas into another theory? *)
use import Nth
theory NthHdTl
use import int.Int
use import Nth
use import HdTl
lemma Nth_tl :
forall l1 l2 : list 'a. tl l1 = Some l2 ->
......@@ -219,3 +223,17 @@ end
theory Fold
(* TODO (a la Map) *)
theory ListRich
use export List
use export Length
use export Mem
use export Nth
use export HdTl
use export NthHdTl
use export Append
use export Reverse
use export Sorted
use export NumOcc
use export Permut
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment