src/Bergamot/Parser.elm

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

src/Bergamot/Rules.elm

@@ -15,7 +15,6 @@ type alias Rule =
 type alias Section =
     { name : String
     , rules : List Rule
-    , hidden: Bool
     }
 
 type ProofTree = MkProofTree
@@ -206,6 +205,10 @@ 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,13 +181,10 @@ viewRuleSection env sec =
     List.map (viewRule env) sec.rules
     |> sequenceMaybes
     |> Maybe.map (\rs ->
-        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)]
-                ])
+        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 =