rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

don't put a ∷ℕ on nat literals that's silly

Browse source
This commit is contained in:
rhiannon morris 2023-04-17 21:45:36 +02:00
parent 06b159973f
commit ac85dc9352
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/Quox/Parser/Parser.idr
View file

@ -306,7 +306,7 @@ mutual
<|> [|TYPE universe|] <|> [|TYPE universe|]
<|> Nat <$ resC "ℕ" <|> Nat <$ resC "ℕ"
<|> Zero <$ resC "zero" <|> Zero <$ resC "zero"
<|> (nat <&> \n => fromNat n :# Nat) <|> [|fromNat nat|]
<|> [|V name|] <|> [|V name|]
<|> [|Tag tag|] <|> [|Tag tag|]

8
tests/Tests/Parser.idr
View file

@ -229,7 +229,7 @@ tests = "parser" :- [
parsesAs term "Nat" Nat, parsesAs term "Nat" Nat,
parsesAs term "zero" Zero, parsesAs term "zero" Zero,
parsesAs term "succ n" (Succ $ V "n"), parsesAs term "succ n" (Succ $ V "n"),
parsesAs term "3" (Succ (Succ (Succ Zero)) :# Nat), parsesAs term "3" (Succ (Succ (Succ Zero))),
parseFails term "succ" parseFails term "succ"
], ],
@ -237,8 +237,8 @@ tests = "parser" :- [
parsesAs term "[1.ℕ]" $ BOX One Nat, parsesAs term "[1.ℕ]" $ BOX One Nat,
parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat), parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat),
parsesAs term "[a]" $ Box (V "a"), parsesAs term "[a]" $ Box (V "a"),
parsesAs term "[0]" $ Box (Zero :# Nat), parsesAs term "[0]" $ Box Zero,
parsesAs term "[1]" $ Box (Succ Zero :# Nat) parsesAs term "[1]" $ Box (Succ Zero)
], ],
"case" :- [ "case" :- [
@ -274,7 +274,7 @@ tests = "parser" :- [
CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"), CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"),
parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $ parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $
Case Any (V "n") (Nothing, Nat) $ Case Any (V "n") (Nothing, Nat) $
CaseNat (Zero :# Nat) (Nothing, One, Just "ih", V "ih"), CaseNat Zero (Nothing, One, Just "ih", V "ih"),
parseFails term "caseω n return A of { zero ⇒ a }", parseFails term "caseω n return A of { zero ⇒ a }",
parseFails term "caseω n return ℕ of { succ ⇒ 5 }" parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
], ],