Commit 5ccab507 authored by François Bobot's avatar François Bobot

add a test for booleans

parent 683e162e
theory Test
use import bool.Bool
goal G1 : True <> False
goal G2 : forall x:bool. x = True or x = False
goal G3 : forall x y z:bool. x<>y and y<>z and z<>x -> false
end
......@@ -32,6 +32,15 @@ transformation "encoding_tptp"
theory BuiltIn
syntax logic (=) "(EQ %1 %2)"
(* use with explicit polymorphism *)
(* meta "enco_poly" "explicit" *)
meta "encoding : base" type int
(* use with encoding_decorate *)
meta "enco_poly" "decorate"
meta "encoding : kept" type int
end
theory int.Int
......@@ -66,14 +75,6 @@ theory int.Int
remove prop NonTrivialRing
remove prop CompatOrderAdd
(* use with explicit polymorphism *)
(* meta "enco_poly" "explicit" *)
meta "encoding : base" type int
(* use with encoding_decorate *)
meta "enco_poly" "decorate"
meta "encoding : kept" type int
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