Remove symeq

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:13:14 -08:00
parent 0b4a1f2ebd
commit 2af1692bf4
1 changed files with 0 additions and 4 deletions
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -206,10 +206,6 @@ builtinRules t =
                    case mp of
                        Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
                        Just _ -> fail)
-            Call "symeq" [Call s1 [], Call s2 []] ->
-                if s1 == s2
-                then pure <| MkProofTree { name = "BuiltinSymEq", conclusion = t, premises = [] }
-                else fail
            _ -> fail

 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)