From 308834a1c0bc9ed8368511bd6fa2dbde7e98243b Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 1 Apr 2023 22:07:01 +0200 Subject: [PATCH] 3 more tests --- tests/Tests/PrettyTerm.idr | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index 0c56a82..249d398 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/tests/Tests/PrettyTerm.idr @@ -68,8 +68,7 @@ tests = "pretty printing terms" :- [ ], "function types" :- [ - skipWith "todo: non-dependent notation" $ - testPrettyT [<] [<] (Arr One (FT "A") (FT "B")) "A ⊸ B" "A -o B", + testPrettyT [<] [<] (Arr One (FT "A") (FT "B")) "1.A → B" "1.A -> B", testPrettyT [<] [<] (Pi_ One "x" (FT "A") (E $ F "B" :@ BVT 0)) "1.(x : A) → B x" @@ -78,12 +77,18 @@ tests = "pretty printing terms" :- [ (Pi_ Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0)) "0.(A : ★₀) → ω.A → A" "0.(A : Type0) -> #.A -> A", - todo #"print (and parse) the below as "(A ↠ A) ↠ A""#, testPrettyT [<] [<] (Arr Any (Arr Any (FT "A") (FT "A")) (FT "A")) "ω.(ω.A → A) → A" "#.(#.A -> A) -> A", - todo "non-dependent, left and right nested" + testPrettyT [<] [<] + (Arr Any (FT "A") (Arr Any (FT "A") (FT "A"))) + "ω.A → ω.A → A" + "#.A -> #.A -> A", + testPrettyT [<] [<] + (Pi_ Zero "P" (Arr Zero (FT "A") (TYPE 0)) (E $ BV 0 :@ FT "a")) + "0.(P : 0.A → ★₀) → P a" + "0.(P : 0.A -> Type0) -> P a" ], "pair types" :- [