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" :- [