From ac85dc93521d7641f9b832dbe9dedad1d29738bc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 17 Apr 2023 21:45:36 +0200 Subject: [PATCH] =?UTF-8?q?don't=20put=20a=20=E2=88=B7=E2=84=95=20on=20nat?= =?UTF-8?q?=20literals=20that's=20silly?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/Parser/Parser.idr | 2 +- tests/Tests/Parser.idr | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 5072bdc..3e3a71f 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -306,7 +306,7 @@ mutual <|> [|TYPE universe|] <|> Nat <$ resC "ℕ" <|> Zero <$ resC "zero" - <|> (nat <&> \n => fromNat n :# Nat) + <|> [|fromNat nat|] <|> [|V name|] <|> [|Tag tag|] diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 4776ea2..6ca28fd 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -229,7 +229,7 @@ tests = "parser" :- [ parsesAs term "Nat" Nat, parsesAs term "zero" Zero, 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" ], @@ -237,8 +237,8 @@ tests = "parser" :- [ parsesAs term "[1.ℕ]" $ BOX One Nat, parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat), parsesAs term "[a]" $ Box (V "a"), - parsesAs term "[0]" $ Box (Zero :# Nat), - parsesAs term "[1]" $ Box (Succ Zero :# Nat) + parsesAs term "[0]" $ Box Zero, + parsesAs term "[1]" $ Box (Succ Zero) ], "case" :- [ @@ -274,7 +274,7 @@ tests = "parser" :- [ CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"), parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $ 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 ℕ of { succ ⇒ 5 }" ],