fixed OCaml driver

added mach.int.Int
removed list.Length
parent 9d1ea986
......@@ -104,10 +104,6 @@ theory list.List
syntax function Cons "(%1 :: %2)"
end
theory list.Length
syntax function length "(List.length %1)"
end
theory list.Mem
syntax predicate mem "(List.mem %1 %2)"
end
......@@ -158,6 +154,11 @@ module array.Array
syntax val blit "Why3__Array.blit"
end
module mach.int.Int
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
end
module mach.int.Int31
(* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
syntax val of_int "Why3__BigInt.to_int"
......
Markdown is supported
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