mach.int.Int63: no more function eq

parent 8fea2e84
Pipeline #12165 failed with stage
in 2 minutes and 59 seconds
......@@ -223,8 +223,6 @@ module mach.int.Int63
syntax val ( * ) "%1 * %2"
syntax val ( / ) "%1 / %2"
syntax val ( % ) "%1 mod %2"
syntax val eq "%1 = %2"
syntax val ne "%1 <> %2"
syntax val (=) "%1 = %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
......
......@@ -71,18 +71,11 @@ module Bounded_int
requires { "expl:integer overflow" in_bounds (- a) }
ensures { result = - a }
val eq (a:t) (b:t) : bool
ensures { to_int a = to_int b -> result } (* leave this to_int ? *)
ensures { result -> a = b }
val ne (a:t) (b:t) : bool
ensures { a <> b -> result }
ensures { result -> to_int a <> to_int b }
axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
val (=) (a:t) (b:t) : bool
ensures { result <-> to_int a = to_int b }
ensures { to_int a = to_int b -> result }
ensures { result -> a = b }
val (<=) (a:t) (b:t) : bool
ensures { result <-> to_int a <= to_int b }
......
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