diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-02-01 16:33:26 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-02-02 13:33:09 +0000 |
| commit | fa4de437fa3861189b506538f6ca4a39771ecbbb (patch) | |
| tree | 70b77e7d0f5c0f80c3695242fe530a67462f034f /src/SOAS/Context.idr | |
| parent | 6dde244c14410ede6d41e9a8607016e23c19e320 (diff) | |
Improve runtime behaviour of variables.
Operations like `weakl`, `weakr` and `copair` now treat variables as
integers at runtime, instead of treating them as unary naturals.
Reimplent `lift` in terms of `copair`.
Diffstat (limited to 'src/SOAS/Context.idr')
| -rw-r--r-- | src/SOAS/Context.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr index 25d2308..ef657ae 100644 --- a/src/SOAS/Context.idr +++ b/src/SOAS/Context.idr @@ -19,6 +19,11 @@ data (.Erased) : type.Ctx -> Type where S : ctx.Erased -> (ctx :< x).Erased public export +(.toNat) : ctx.Erased -> Nat +(Z).toNat = 0 +(S length).toNat = S length.toNat + +public export (++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx ctx1 ++ [<] = ctx1 ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty |