mergesort_list still in progress

examples/programs/mergesort_list.mlw

@@ -8,6 +8,10 @@
  lemma Permut_append: 
     forall l1 l2 k1 k2 : list 'a.
     permut l1 k1 -> permut l2 k2 -> permut (append l1 l2) (append k1 k2)
+
+ lemma Permut_cons_append:
+   forall x : 'a, l1 l2 : list 'a.
+   permut (append (Cons x l1) l2) (append l1 (Cons x l2))
 }
 
 let split l0 =

tests/test-jcf.why

@@ -3,13 +3,11 @@
 
 theory Test
 
-  use export int.Int
+  use import list.List
 
-  use real.Real as R
-  logic ( *. ) (x:real) (y:real) : real = R.(*) x y 
+  logic p (list 'a)
 
-  logic power (x : real) (n : int) : real =
-     if n = 0 then 1.0 else x *. power x (n-1)
+  goal G : p (Nil : list 'a) -> not (p (Nil : list 'b)) -> false
 
 end
 

theories/list.why

@@ -12,7 +12,7 @@ theory Length
   logic length (l : list 'a) : int = 
     match l with
     | Nil      -> 0
-    | Cons _ r -> 1 + length(r)
+    | Cons _ r -> 1 + length r
     end
 
   lemma Length_nonnegative : forall l:list 'a. length(l) >= 0