From 5b1dab24f205ab7a3cd2f6a14086631de23683ef Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 9 May 2022 04:30:37 +0200
Subject: [PATCH] =?UTF-8?q?=F0=9D=92=B0=20=E2=86=92=20=E2=98=85?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/Tests/Equal.idr | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index bbed6a5..9671bb6 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -52,17 +52,17 @@ export
 tests : Test
 tests = "equality & subtyping" :- [
     "universes" :- [
-        testEq "𝒰₀ ≡ 𝒰₀" $
+        testEq "★₀ ≡ ★₀" $
           equalT (TYPE 0) (TYPE 0),
-        testNeq "𝒰₀ ≢ 𝒰₁" $
+        testNeq "★₀ ≢ ★₁" $
           equalT (TYPE 0) (TYPE 1),
-        testNeq "𝒰₁ ≢ 𝒰₀" $
+        testNeq "★₁ ≢ ★₀" $
           equalT (TYPE 1) (TYPE 0),
-        testEq "𝒰₀ <: 𝒰₀" $
+        testEq "★₀ <: ★₀" $
           subT (TYPE 0) (TYPE 0),
-        testEq "𝒰₀ <: 𝒰₁" $
+        testEq "★₀ <: ★₁" $
           subT (TYPE 0) (TYPE 1),
-        testNeq "𝒰₁ ≮: 𝒰₀" $
+        testNeq "★₁ ≮: ★₀" $
           subT (TYPE 1) (TYPE 0)
       ],
 
@@ -82,29 +82,29 @@ tests = "equality & subtyping" :- [
         let tm1 = Arr Zero (FT "A") (FT "B")
             tm2 = Arr One  (FT "A") (FT "B") in
         subT tm1 tm2,
-      testEq "𝒰₀ ⇾ 𝒰₀ ≡ 𝒰₀ ⇾ 𝒰₀" $
+      testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $
         let tm = Arr Zero (TYPE 0) (TYPE 0) in
         equalT tm tm,
-      testEq "𝒰₀ ⇾ 𝒰₀ <: 𝒰₀ ⇾ 𝒰₀" $
+      testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
         let tm = Arr Zero (TYPE 0) (TYPE 0) in
         subT tm tm,
-      testNeq "𝒰₁ ⊸ 𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₀" $
+      testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $
         let tm1 = Arr Zero (TYPE 1) (TYPE 0)
             tm2 = Arr Zero (TYPE 0) (TYPE 0) in
         equalT tm1 tm2,
-      testEq "𝒰₁ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₀" $
+      testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
         let tm1 = Arr One (TYPE 1) (TYPE 0)
             tm2 = Arr One (TYPE 0) (TYPE 0) in
         subT tm1 tm2,
-      testNeq "𝒰₀ ⊸ 𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₁" $
+      testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $
         let tm1 = Arr Zero (TYPE 0) (TYPE 0)
             tm2 = Arr Zero (TYPE 0) (TYPE 1) in
         equalT tm1 tm2,
-      testEq "𝒰₀ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₁" $
+      testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
         let tm1 = Arr One (TYPE 0) (TYPE 0)
             tm2 = Arr One (TYPE 0) (TYPE 1) in
         subT tm1 tm2,
-      testEq "𝒰₀ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₁" $
+      testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
         let tm1 = Arr One (TYPE 0) (TYPE 0)
             tm2 = Arr One (TYPE 0) (TYPE 1) in
         subT tm1 tm2
@@ -170,7 +170,7 @@ tests = "equality & subtyping" :- [
     todo "elim d-closure",
 
     "clashes" :- [
-      testNeq "𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₀" $
+      testNeq "★₀ ≢ ★₀ ⇾ ★₀" $
         equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
       todo "others"
     ]