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)) =