Commit 008aef67 authored by MARCHE Claude's avatar MARCHE Claude

Simplified definitions of bool.Bool.xorb and bool.Bool.implb

parent 16a90e40
......@@ -130,6 +130,7 @@ end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
(* not uniformly interpreted by provers
......
......@@ -19,23 +19,22 @@ theory Bool
| True -> True
end
function xorb (x y : bool) : bool =
match x, y with
| True, False -> True
| False, True -> True
| _ , _ -> False
end
function notb (x : bool) : bool =
match x with
| False -> True
| True -> False
end
function xorb (x y : bool) : bool =
match x with
| False -> y
| True -> notb y
end
function implb (x y : bool) : bool =
match x,y with
| True, False -> False
| _,_ -> True
match x with
| False -> True
| True -> y
end
end
......
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