summaryrefslogtreecommitdiff
path: root/src/Inky/Type
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2024-10-09 16:26:23 +0100
committerGreg Brown <greg.brown01@ed.ac.uk>2024-10-09 16:26:23 +0100
commit8b326bb4a879be72cb6382519350cbb5231f7a6e (patch)
treebeff7c254f31795bb6cfee2b0b90ad147ab5ba32 /src/Inky/Type
parent405519b406174bec161bc4d23deb0551b1ed31ac (diff)
Do a lot.
- Add type aliases. - Make `suc` a symbol. - Fix incorrect specification for `IsFunction`. - Write parser for terms. - Use `collie` to improve command line experience.
Diffstat (limited to 'src/Inky/Type')
-rw-r--r--src/Inky/Type/Pretty.idr2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 1f2d35b..83253b4 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -19,7 +19,7 @@ prettyType TNat d = pretty "Nat"
prettyType (TArrow a b) d =
parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
let parts = stripArrow b in
- concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts)
+ concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts)
where
stripArrow : Ty ctx () -> List (Doc ann)
stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b