From fa4de437fa3861189b506538f6ca4a39771ecbbb Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 16:33:26 +0000
Subject: 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`.
---
 src/SOAS/Context.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/SOAS/Context.idr')

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
@@ -18,6 +18,11 @@ data (.Erased) : type.Ctx -> Type where
   Z : [<].Erased
   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
-- 
cgit v1.2.3