Use stable version of NixOS for nixpkgs

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

flake.lock

@@ -5,11 +5,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1694529238,
-        "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
         "type": "github"
       },
       "original": {
@@ -20,16 +20,16 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1701068326,
-        "narHash": "sha256-vmMceA+q6hG1yrjb+MP8T0YFDQIrW3bl45e7z24IEts=",
+        "lastModified": 1766736597,
+        "narHash": "sha256-BASnpCLodmgiVn0M1MU2Pqyoz0aHwar/0qLkp7CjvSQ=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "8cfef6986adfb599ba379ae53c9f5631ecd2fd9c",
+        "rev": "f560ccec6b1116b22e6ed15f4c510997d99d5852",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-unstable",
+        "ref": "nixos-25.11",
         "repo": "nixpkgs",
         "type": "github"
       }

flake.nix

@@ -1,6 +1,6 @@
 {
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-25.11";
     flake-utils.url = "github:numtide/flake-utils";
   };
   outputs = { self, nixpkgs, flake-utils }:

src/Bergamot/Latex.elm

@@ -68,4 +68,5 @@ metavariableToLatex (MkMetavariable s) =
         noQuestion = String.dropLeft 1 s
     in
         if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
-        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
+        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else
+        if String.startsWith "rho" noQuestion then "\\" ++ noQuestion else noQuestion

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
@@ -158,6 +159,10 @@ builtinRules t =
             Call "int" [Var output] ->
                 let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
                 in rec 0
+            Call "add" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinAdd" (IntLit (i1 + i2)) output
+            Call "subtract" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinSubtract" (IntLit (i1 - i2)) output
             Call "float" [FloatLit f] ->
                 MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
                 |> pure
@@ -201,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 =