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/Compile.idr | |
| parent | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (diff) | |
Add quotation to help metaprogramming.
Diffstat (limited to 'src/Inky/Term/Compile.idr')
| -rw-r--r-- | src/Inky/Term/Compile.idr | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr index 0867cd2..0d42660 100644 --- a/src/Inky/Term/Compile.idr +++ b/src/Inky/Term/Compile.idr @@ -149,7 +149,7 @@ compileFold {a} wf prf target bind body = export compileSynths : {tmCtx : SnocList String} -> - {t : Term mode m tyCtx tmCtx} -> + {t : Term NoSugar m tyCtx tmCtx} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> @@ -159,7 +159,7 @@ compileSynths : export compileChecks : {tmCtx : SnocList String} -> - {t : Term mode m tyCtx tmCtx} -> + {t : Term NoSugar m tyCtx tmCtx} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> @@ -170,7 +170,7 @@ compileChecks : Doc ann compileSpine : {tmCtx : SnocList String} -> - {ts : List (Term mode m tyCtx tmCtx)} -> + {ts : List (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> @@ -182,7 +182,7 @@ compileSpine : Doc ann compileAllSynths : {tmCtx : SnocList String} -> - {ts : Context (Term mode m tyCtx tmCtx)} -> + {ts : Context (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> @@ -191,7 +191,7 @@ compileAllSynths : All (Assoc0 $ Doc ann) ts.names compileAllChecks : {tmCtx : SnocList String} -> - {ts : Context (Term mode m tyCtx tmCtx)} -> + {ts : Context (Term NoSugar m tyCtx tmCtx)} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> @@ -203,7 +203,7 @@ compileAllChecks : All (Assoc0 $ Doc ann) ts.names compileAllBranches : {tmCtx : SnocList String} -> - {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} -> + {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} -> {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> (0 tyWf : DAll WellFormed tyEnv) -> |