rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

use ★ for Type in unicode mode

Browse source
This commit is contained in:
rhiannon morris 2023-02-25 19:14:26 +01:00
parent 4b284d6e01
commit 79a828449a
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Syntax/Term/Pretty.idr
View file

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