From 5e956b5074b092fb4983e4ce0bfc0086e91842cd Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Thu, 17 Feb 2011 19:52:29 +0100 Subject: [PATCH] added theory list.ListRich --- examples/programs/vstte10_aqueue.mlw | 6 +----- theories/list.why | 22 ++++++++++++++++++++-- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/examples/programs/vstte10_aqueue.mlw b/examples/programs/vstte10_aqueue.mlw index dac6519d4..0f747c571 100644 --- a/examples/programs/vstte10_aqueue.mlw +++ b/examples/programs/vstte10_aqueue.mlw @@ -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) diff --git a/theories/list.why b/theories/list.why index 9c61695aa..2ae38c8b2 100644 --- a/theories/list.why +++ b/theories/list.why @@ -58,9 +58,13 @@ theory HdTl "head and tail" | Cons _ t -> Some t end - (* TODO: move these lemmas into another theory? *) - use import Nth +end + +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) *) end + +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 +end -- 2.24.1