diff options
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 |