Remove rules ecEq_unfold and ecEq_refl.

(Proofs can now use `add_cryptol_defs ["ecEq"]` instead.)
GaloisInc · Dec 6, 2018 · 45959b9 · 45959b9
1 parent 5794a3a
commit 45959b9
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/saw/Cryptol.sawcore b/saw/Cryptol.sawcore
@@ -1284,11 +1284,6 @@ ecSle =
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
-ecEq_unfold : (a : sort 0) -> (pa : PCmp a) -> Eq (a -> a -> Bool) (ecEq a pa) pa.eq;
-ecEq_unfold a pa = Refl (a -> a -> Bool) (ecEq a pa);
-
-axiom ecEq_refl : (a : sort 0) -> (pa : PCmp a) -> (x : a) -> Eq Bool (ecEq a pa x x) True;
-
 axiom replicate_False : (n : Nat) -> Eq (bitvector n) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;