Fix some typing errors and/or warnings in examples.

examples/dijkstra.mlw

@@ -26,9 +26,8 @@ module DijkstraShortestPath
   axiom G_succ_sound :
     forall x: vertex. S.subset (g_succ x) v
 
-  function weight vertex vertex : int (* edge weight, if there is an edge *)
-
-  axiom Weight_nonneg: forall x y: vertex. weight x y >= 0
+  val function weight vertex vertex : int (* edge weight, if there is an edge *)
+    ensures { result >= 0 }
 
   (** Data structures for the algorithm. *)
 

examples/fibonacci.mlw

@@ -275,7 +275,9 @@ theory Mat22 "2x2 integer matrices"
   (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *)
 
   clone export
-    int.Exponentiation with type t = t, function one = id, function (*) = mult
+    int.Exponentiation with
+      type t = t, function one = id, function (*) = mult,
+      goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
 
 end
 

examples/in_progress/cek.mlw

@@ -187,8 +187,8 @@ type context =
 let rec function recompose (c:context) (t:term) (e:environment) : term =
   match c with
   | Empty -> t
-  | Left c t1 e1 -> App (recompose c t e) t1
-  | Right (Closure x t1 e1) c -> App (Lambda x t1) (recompose c t e)
+  | Left c t1 _e1 -> App (recompose c t e) t1
+  | Right (Closure x t1 _e1) c -> App (Lambda x t1) (recompose c t e)
   end
 
 (*
@@ -218,7 +218,7 @@ let rec lemma recompose_values (c:context) (t1 t2:expr) (e:environment) : unit
 
 let rec eval (t:term) (e:environment) (c:context) : value
   diverges
-  returns { Closure x t1 e1 ->
+  returns { Closure x t1 _e1 ->
     weak_normalize (recompose c t e) (Lambda x t1) }
 = match t with
   | Var x -> cont c (lookup x e)

examples/in_progress/gmp_square_root.mlw

@@ -16,9 +16,8 @@
 
 module GmpModel
 
-  use export int.Int
-  use export int.ComputerDivision
-  use export array.Array
+  use import int.Int
+  use import array.Array
 
   constant beta' : int
   axiom beta'_gt_1: 1 < beta'
@@ -75,8 +74,11 @@ end
 module GmpAuxiliaryfunctions
 
   use export GmpModel
-  use export ref.Ref
-  use export int.Power
+  use import int.Int
+  use import int.ComputerDivision
+  use import int.Power
+  use import ref.Ref
+  use import array.Array
 
   val rb: ref bool
 

examples/in_progress/immutable_string.mlw

@@ -10,7 +10,7 @@ module String
 
   function ([]) (s: string) (i: int) : char = s.chars i
 
-  constant empty : string = { length = 0; chars = fun (i: int) -> dummy_char }
+  constant empty : string = { length = 0; chars = fun (_: int) -> dummy_char }
 
   val get (s: string) (i:int) : char
     requires { 0 <= i < s.length }

examples/random_access_list.mlw

@@ -250,7 +250,7 @@ module RandomAccessListWithSeq
   function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
     set s i (f s[i])
 
-  function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
+  let function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
     fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
 
   let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a

examples/vstte12_ring_buffer.mlw

@@ -152,7 +152,7 @@ module RingBufferSeq
     mutable first: int;
     mutable len  : int;
             data : array 'a;
-    ghost mutable sequence: S.seq 'a;
+    ghost mutable sequence: S.seq {'a};
   }
   invariant {
     let size = Array.length data in