added implies__eq rule as a temporary fix, to do what scDefRewriteRul…

…es will eventually handle...
GaloisInc · May 30, 2018 · f160b98 · f160b98
1 parent 2268a80
commit f160b98
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -307,6 +307,10 @@ axiom xor__eq :: (b1 b2::Bool) ->
 implies :: Bool -> Bool -> Bool;
 implies = \ (a::Bool) (b::Bool) -> or (not a) b;
 
+-- FIXME: this rule should be derived by scDefRewriteRules
+implies__eq :: (a b::Bool) -> Eq Bool (implies a b) (or (not a) b);
+implies__eq a b = Refl Bool (implies a b);
+
 -- Decidable Boolean equality, also known as iff
 primitive boolEq :: Bool -> Bool -> Bool;
 axiom boolEq__eq :: (b1 b2::Bool) ->