Compare commits

..

4 Commits

Author SHA1 Message Date
ceca48840e Use stable version of NixOS for nixpkgs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-12-26 22:30:08 +00:00
000d95ae5b Update flake.lock
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-12-26 21:25:04 +00:00
2af1692bf4 Remove symeq
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:13:14 -08:00
0b4a1f2ebd Implement hidden sections
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:13:05 -08:00
5 changed files with 25 additions and 19 deletions

14
flake.lock generated
View File

@@ -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"
}

View File

@@ -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 }:

View File

@@ -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 =

View File

@@ -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)

View File

@@ -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 =