diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-01-26 15:14:48 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-01-26 15:14:48 +0000 |
| commit | 8dfd872384d32998886d9938f9c741002fd47253 (patch) | |
| tree | 568d6f4d0b2791c46198f01a6397bbba4de04264 | |
| parent | f252e7753887e9d7db5bf9c50cb763ef6ed6d71e (diff) | |
Remove runtime dependency on the context.
| -rw-r--r-- | src/SOAS.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SOAS.idr b/src/SOAS.idr index befd53c..8540c83 100644 --- a/src/SOAS.idr +++ b/src/SOAS.idr @@ -136,12 +136,12 @@ record MonStruct (m : type.SortedFamily) where var : Var -|> m mult : m -|> (m ^ m) -(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {ctx : type.Ctx} -> +(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {0 ctx : type.Ctx} -> (mon : MonStruct m) => m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx t.sub s = mon.mult t (extend m s mon.var) (.sub2) : {m : type.SortedFamily} -> {ty1,ty2,sy : type} -> - {ctx : type.Ctx} -> + {0 ctx : type.Ctx} -> (mon : MonStruct m) => m sy (ctx :< (x :- ty1) :< (x :- ty2)) -> m ty1 ctx -> m ty2 ctx -> m sy ctx t.sub2 s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var)) |