Commit 7c97e32d authored by Andrei Paskevich's avatar Andrei Paskevich

protect booleans

parent 4f34dfda
......@@ -108,19 +108,16 @@ theory real.Real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "BITVECTOR(1)"
syntax type bool "BITVECTOR(1)"
syntax function True "0bin1"
syntax function False "0bin0"
syntax function andb "(%1 & %2)"
syntax function orb "(%1 | %2)"
syntax function xorb "(BVXOR(%1,%2))"
syntax function notb "(~ %1)"
meta cloned "encoding_decorate : kept" type bool
meta "encoding : kept" type bool
end
*)
(*
theory int.EuclideanDivision
......
......@@ -106,19 +106,16 @@ theory real.Real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
meta "encoding : kept" type bool
end
*)
theory int.EuclideanDivision
......
......@@ -108,18 +108,15 @@ theory real.Real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
meta "encoding : kept" type bool
end
*)
theory int.EuclideanDivision
......
......@@ -108,20 +108,16 @@ theory real.Real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
meta "encoding : kept" type bool
end
*)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
......
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