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/Recompute.idr | |
| parent | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (diff) | |
Add quotation to help metaprogramming.
Diffstat (limited to 'src/Inky/Term/Recompute.idr')
| -rw-r--r-- | src/Inky/Term/Recompute.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr index dd0e809..71ba6b9 100644 --- a/src/Inky/Term/Recompute.idr +++ b/src/Inky/Term/Recompute.idr @@ -76,7 +76,7 @@ dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf export synthsWf : - {e : Term mode m tyCtx tmCtx} -> + {e : Term NoSugar m tyCtx tmCtx} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> DAll WellFormed tyEnv -> DAll WellFormed tmEnv -> @@ -85,7 +85,7 @@ checkSpineWf : CheckSpine tyEnv tmEnv a ts b -> WellFormed a -> WellFormed b allSynthsWf : - {es : Context (Term mode m tyCtx tmCtx)} -> + {es : Context (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> DAll WellFormed tyEnv -> DAll WellFormed tmEnv -> |