From 95a0b38d7489bdf260b220869a46712b04af6354 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 12 Apr 2024 22:00:08 +0200
Subject: [PATCH] update pretty-printing tests

---
 tests/Tests/PrettyTerm.idr | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index b15cadc..551a444 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -105,8 +105,8 @@ tests = "pretty printing terms" :- [
   ],
 
   "type universes" :- [
-    testPrettyT [<] [<] (^TYPE 0) "★⁰" "Type 0",
-    testPrettyT [<] [<] (^TYPE 100) "★¹⁰⁰" "Type 100"
+    testPrettyT [<] [<] (^TYPE 0) "★" "Type",
+    testPrettyT [<] [<] (^TYPE 100) "★¹⁰⁰" "Type^100"
   ],
 
   "function types" :- [
@@ -120,8 +120,8 @@ tests = "pretty printing terms" :- [
       "1.(x : A) -> B x",
     testPrettyT [<] [<]
       (^PiY Zero "A" (^TYPE 0) (^Arr Any (^BVT 0) (^BVT 0)))
-      "0.(A : ★⁰) → ω.A → A"
-      "0.(A : Type 0) -> #.A -> A",
+      "0.(A : ★) → ω.A → A"
+      "0.(A : Type) -> #.A -> A",
     testPrettyT [<] [<]
       (^Arr Any (^Arr Any (^FT "A" 0) (^FT "A" 0)) (^FT "A" 0))
       "ω.(ω.A → A) → A"
@@ -133,8 +133,8 @@ tests = "pretty printing terms" :- [
     testPrettyT [<] [<]
       (^PiY Zero "P" (^Arr Zero (^FT "A" 0) (^TYPE 0))
         (E $ ^App (^BV 0) (^FT "a" 0)))
-      "0.(P : 0.A → ★⁰) → P a"
-      "0.(P : 0.A -> Type 0) -> P a"
+      "0.(P : 0.A → ★) → P a"
+      "0.(P : 0.A -> Type) -> P a"
   ],
 
   "pair types" :- [
@@ -193,8 +193,8 @@ tests = "pretty printing terms" :- [
   "case" :- [
     testPrettyE [<] [<]
       (^CasePair One (^F "a" 0) (SN $ ^TYPE 1) (SN $ ^TYPE 0))
-      "case1 a return ★¹ of { (_, _) ⇒ ★⁰ }"
-      "case1 a return Type 1 of { (_, _) => Type 0 }",
+      "case1 a return ★¹ of { (_, _) ⇒ ★ }"
+      "case1 a return Type^1 of { (_, _) => Type }",
     testPrettyT [<] [<]
       (^LamY "u" (E $
         ^CaseEnum One (^F "u" 0)
@@ -209,10 +209,10 @@ tests = "pretty printing terms" :- [
 
   "type-case" :- [
     testPrettyE [<] [<]
-      {label = "type-case ℕ ∷ ★⁰ return ★⁰ of { ⋯ }"}
+      {label = "type-case ℕ ∷ ★ return ★ of { ⋯ }"}
       (^TypeCase (^Ann (^NAT) (^TYPE 0)) (^TYPE 0) empty (^NAT))
-      "type-case ℕ ∷ ★⁰ return ★⁰ of { _ ⇒ ℕ }"
-      "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
+      "type-case ℕ ∷ ★ return ★ of { _ ⇒ ℕ }"
+      "type-case Nat :: Type return Type of { _ => Nat }"
   ],
 
   skipWith "(todo: print user-written redundant annotations)" $
@@ -236,6 +236,6 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^Ann (^Arr One (^FT "A" 0) (^FT "A" 0)) (^TYPE 7))
       "(1.A → A) ∷ ★⁷"
-      "(1.A -> A) :: Type 7"
+      "(1.A -> A) :: Type^7"
   ]
 ]