new theory list.Prefix

fb2b1efa · Jean-Christophe Filliâtre · 8b293634 · fb2b1efa
Commit fb2b1efa authored Jan 09, 2013 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 14 additions and 0 deletions

theories/list.why theories/list.why +14 -0

No files found.
--- a/theories/list.why
+++ b/theories/list.why
@@ -341,6 +341,20 @@ theory Distinct

 end

+theory Prefix
+
+  use export List
+  use import int.Int
+
+  function prefix (n: int) (l: list 'a) : list 'a =
+    if n <= 0 then Nil else
+    match l with
+    | Nil -> Nil
+    | Cons x r -> Cons x (prefix (n-1) r)
+    end
+
+end
+
 (** {2 Induction on lists} *)

 theory Induction