From 4b284d6e0184445a42c38a65c2e4202b4bd7e6a6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Feb 2023 19:14:11 +0100
Subject: [PATCH] =?UTF-8?q?rename=20=CE=BB=E1=B4=B0=20to=20=CE=B4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

sorry fen
---
 lib/Quox/Syntax/Term/Pretty.idr | 14 +++++++-------
 lib/Quox/Typechecker.idr        |  2 +-
 tests/Tests/Equal.idr           |  4 ++--
 tests/Tests/Typechecker.idr     | 16 ++++++++--------
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 5a3dd6c..caed70a 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -13,13 +13,13 @@ import Data.Vect
 private %inline
 arrowD, timesD, darrowD, lamD, eqndD, dlamD, annD :
   Pretty.HasEnv m => m (Doc HL)
-arrowD  = hlF Syntax $ ifUnicode "→"  "->"
-timesD  = hlF Syntax $ ifUnicode "×"  "**"
-darrowD = hlF Syntax $ ifUnicode "⇒"  "=>"
-lamD    = hlF Syntax $ ifUnicode "λ"  "fun"
-eqndD   = hlF Syntax $ ifUnicode "≡"  "=="
-dlamD   = hlF Syntax $ ifUnicode "λᴰ" "dfun"
-annD    = hlF Syntax $ ifUnicode "∷"  "::"
+arrowD  = hlF Syntax $ ifUnicode "→" "->"
+timesD  = hlF Syntax $ ifUnicode "×" "**"
+darrowD = hlF Syntax $ ifUnicode "⇒" "=>"
+lamD    = hlF Syntax $ ifUnicode "λ" "fun"
+eqndD   = hlF Syntax $ ifUnicode "≡" "=="
+dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
+annD    = hlF Syntax $ ifUnicode "∷" "::"
 
 private %inline
 typeD, eqD, colonD, commaD, caseD, returnD, ofD : Doc HL
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 2d9c493..8213959 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -174,7 +174,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     equal ctx ty.zero body.zero l
     -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
     equal ctx ty.one body.one  r
-    -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
   check' ctx sg (E e) ty = do
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 0ce5908..669351e 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -169,7 +169,7 @@ tests = "equality & subtyping" :- [
       refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
   in
   [
-    note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
+    note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
     note "binds before ∥ are globals, after it are BVs",
     testEq "refl [A] a = refl [A] a" $
       equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
@@ -250,7 +250,7 @@ tests = "equality & subtyping" :- [
   "term d-closure" :- [
     testEq "★₀‹𝟎› = ★₀ : ★₁" $
       equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
-    testEq "(λᴰ i ⇒ a)‹𝟎› = (λᴰ i ⇒ a) : (a ≡ a : A)" $
+    testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $
       equalTD 1 empty
         (Eq0 (FT "A") (FT "a") (FT "a"))
         (DCloT (["i"] :\\% FT "a") (K Zero ::: id))
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index c19e51b..88d3f1e 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -246,7 +246,7 @@ tests = "typechecker" :- [
     note "(fail) runtime-relevant type",
     testTCFail "1 · A ⇏ ★₀" $
       infer_ (ctx [<]) sone (F "A"),
-    note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
+    note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
     testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy,
     testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
   ],
@@ -279,7 +279,7 @@ tests = "typechecker" :- [
       check_ (ctx [<]) sone
         (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
         reflTy,
-    testTC "1 · (λ A x ⇒ λᴰ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
+    testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
       check_ (ctx [<]) sone reflDef reflTy
   ],
 
@@ -289,7 +289,7 @@ tests = "typechecker" :- [
     testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
       checkQ (ctx [< FT "A"]) sone
         (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
-    testTC "1 · (a, λᴰ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
+    testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
       check_ (ctx [<]) sone
         (Pair (FT "a") (["i"] :\\% FT "a"))
         (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
@@ -360,16 +360,16 @@ tests = "typechecker" :- [
   ],
 
   "equalities" :- [
-    testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
+    testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
       check_ (ctx [<]) sone (DLam $ SN $ FT "a")
         (Eq0 (FT "A") (FT "a") (FT "a")),
-    testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
+    testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ (ctx [<]) szero
         (["p","q"] :\\ ["i"] :\\% BVT 1)
         (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
-    testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
+    testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ (ctx [<]) szero
         (["p","q"] :\\ ["i"] :\\% BVT 0)
         (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
@@ -380,7 +380,7 @@ tests = "typechecker" :- [
   "misc" :- [
     note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
     note "⊢",
-    note "1 · λ x y xy ⇒ λᴰ i ⇒ p (xy i)",
+    note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
     note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
     testTC "cong" $
       check_ (ctx [<]) sone
@@ -393,7 +393,7 @@ tests = "typechecker" :- [
     note "0·A : Type, 0·P : ω·A → Type,",
     note "ω·p q : (1·x : A) → P x",
     note "⊢",
-    note "1 · λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i",
+    note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
     note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
     testTC "funext" $
       check_ (ctx [<]) sone