diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2025-01-07 13:50:13 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2025-01-07 13:50:13 +0000 |
| commit | f2490f5ca35b528c7332791c6932045eb9d5438b (patch) | |
| tree | 9a4caa4715705dcc4965d4507213ce4ca29e0add /src/Inky/Term/Pretty | |
| parent | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (diff) | |
Add quotation to help metaprogramming.
Diffstat (limited to 'src/Inky/Term/Pretty')
| -rw-r--r-- | src/Inky/Term/Pretty/Error.idr | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr index d87178f..ee0f28a 100644 --- a/src/Inky/Term/Pretty/Error.idr +++ b/src/Inky/Term/Pretty/Error.idr @@ -25,7 +25,7 @@ Pretty (ChecksOnly t) where export prettyNotSynths : {tyCtx, tmCtx : SnocList String} -> - {e : Term mode m tyCtx tmCtx} -> + {e : Term NoSugar m tyCtx tmCtx} -> {tyEnv : _} -> {tmEnv : _} -> NotSynths tyEnv tmEnv e -> List (m, Doc ann) @@ -33,33 +33,33 @@ export prettyNotChecks : {tyCtx, tmCtx : SnocList String} -> {a : Ty [<]} -> - {t : Term mode m tyCtx tmCtx} -> + {t : Term NoSugar m tyCtx tmCtx} -> {tyEnv : _} -> {tmEnv : _} -> NotChecks tyEnv tmEnv a t -> List (m, Doc ann) prettyNotCheckSpine : {tyCtx, tmCtx : SnocList String} -> {a : Ty [<]} -> - {ts : List (Term mode m tyCtx tmCtx)} -> + {ts : List (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : _} -> {tmEnv : _} -> NotCheckSpine tyEnv tmEnv a ts -> List (m, Doc ann) prettyAnyNotSynths : {tyCtx, tmCtx : SnocList String} -> - {es : Context (Term mode m tyCtx tmCtx)} -> + {es : Context (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : _} -> {tmEnv : _} -> AnyNotSynths tyEnv tmEnv es -> List (m, Doc ann) prettyAnyNotChecks : {tyCtx, tmCtx : SnocList String} -> - {ts : Context (Term mode m tyCtx tmCtx)} -> + {ts : Context (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> (meta : m) -> AnyNotChecks tyEnv tmEnv as ts -> List (m, Doc ann) prettyAnyNotBranches : {tyCtx, tmCtx : SnocList String} -> - {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} -> + {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} -> {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} -> (meta : m) -> AnyNotBranches tyEnv tmEnv as a ts -> |