Remove symeq

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Parser.elm

@@ -8,7 +8,7 @@ import Parser exposing (Parser, Trailing(..), (|.), (|=))
 import Set exposing (Set)
 
 reserved : Set String
-reserved = Set.fromList ["section"]
+reserved = Set.fromList ["hidden", "section"]
 
 strLit : Parser String
 strLit =
@@ -120,7 +120,13 @@ rules = Parser.sequence
 
 sectionExp : Parser Section
 sectionExp =
-    Parser.succeed (\n rs -> { name = n, rules = rs })
+    Parser.succeed (\h n rs -> { hidden = h, name = n, rules = rs })
+    |= Parser.oneOf
+        [ Parser.succeed True
+          |. Parser.symbol "hidden"
+          |. Parser.spaces
+        , Parser.succeed False
+        ]
     |. Parser.symbol "section" |. Parser.spaces
     |= strLit |. Parser.spaces
     |. Parser.symbol "{" |. Parser.spaces
@@ -137,7 +143,7 @@ sectionImp =
                 _ -> Parser.succeed (Parser.Done <| List.reverse rs)
             ])
     |> Parser.loop []
-    |> Parser.map (\rs -> { name = "", rules = rs })
+    |> Parser.map (\rs -> { hidden = False, name = "", rules = rs })
 
 program : Parser RuleEnv
 program =

src/Bergamot/Rules.elm

@@ -15,6 +15,7 @@ type alias Rule =
 type alias Section =
     { name : String
     , rules : List Rule
+    , hidden: Bool
     }
 
 type ProofTree = MkProofTree
@@ -205,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)

src/Main.elm

@@ -181,10 +181,13 @@ viewRuleSection env sec =
     List.map (viewRule env) sec.rules
     |> sequenceMaybes
     |> Maybe.map (\rs ->
-        Html.div [ class "bergamot-rule-section" ]
-        [ Html.div [ class "bergamot-rule-list" ] rs
-        , Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
-        ])
+        case sec.hidden of
+            True -> Html.div [ class "bergamot-rule-section" ] []
+            False ->
+                Html.div [ class "bergamot-rule-section" ]
+                [ Html.div [ class "bergamot-rule-list" ] rs
+                , Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
+                ])
 
 viewRules : String -> String -> Html Msg
 viewRules renderProgs progs =