mach.int.Bounded_int: better posts (inlined extensionality)

parent 98139817
......@@ -71,10 +71,12 @@ module Bounded_int
ensures { to_int result = - to_int a }
val eq (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 ne (a:t) (b:t) : bool
ensures { result <-> to_int a <> to_int b }
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
......
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