From 79a828449a51d73d3d414743d803cf1017c04601 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Feb 2023 19:14:26 +0100
Subject: [PATCH] =?UTF-8?q?use=20=E2=98=85=20for=20Type=20in=20unicode=20m?=
 =?UTF-8?q?ode?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Syntax/Term/Pretty.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index caed70a..f84efc3 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -11,8 +11,9 @@ import Data.Vect
 
 
 private %inline
-arrowD, timesD, darrowD, lamD, eqndD, dlamD, annD :
+typeD, arrowD, timesD, darrowD, lamD, eqndD, dlamD, annD :
   Pretty.HasEnv m => m (Doc HL)
+typeD   = hlF Syntax $ ifUnicode "★" "Type"
 arrowD  = hlF Syntax $ ifUnicode "→" "->"
 timesD  = hlF Syntax $ ifUnicode "×" "**"
 darrowD = hlF Syntax $ ifUnicode "⇒" "=>"
@@ -22,8 +23,7 @@ dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
 annD    = hlF Syntax $ ifUnicode "∷" "::"
 
 private %inline
-typeD, eqD, colonD, commaD, caseD, returnD, ofD : Doc HL
-typeD   = hl Syntax "Type"
+eqD, colonD, commaD, caseD, returnD, ofD : Doc HL
 eqD     = hl Syntax "Eq"
 colonD  = hl Syntax ":"
 commaD  = hl Syntax ","
@@ -95,7 +95,7 @@ mutual
   export covering
   PrettyHL q => PrettyHL (Term q d n) where
     prettyM (TYPE l) =
-      parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
+      parensIfM App $ !typeD <//> !(withPrec Arg $ prettyM l)
     prettyM (Pi qty s (S [x] t)) =
       prettyBindType [qty] x s !arrowD t
     prettyM (Lam (S x t)) =