diff options
author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-09-30 18:20:08 +0100 |
---|---|---|
committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-09-30 18:20:08 +0100 |
commit | 405519b406174bec161bc4d23deb0551b1ed31ac (patch) | |
tree | 86e53a7f168d63516562e5da9a7a1f786b83b973 /src/Inky/Term | |
parent | 39bd40eea9c0b8935f7feabdeb20802e98e5b603 (diff) |
Make tags for tuples and cases unique.
Diffstat (limited to 'src/Inky/Term')
-rw-r--r-- | src/Inky/Term/Pretty.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index 71028ba..7c5ee4d 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -31,10 +31,10 @@ prettyAllCheck : List (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) prettyCheckCtx : {tyCtx, tmCtx : Context ()} -> - Context (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) + Row (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) prettyCheckCtxBinding : {tyCtx, tmCtx : Context ()} -> - Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann) + Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann) prettySynth (Var i) d = pretty (unVal $ nameOf i) prettySynth (Lit k) d = pretty k |