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/Example.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Example.idr')

diff --git a/src/Example.idr b/src/Example.idr
index 83d6acc..3676d5e 100644
--- a/src/Example.idr
+++ b/src/Example.idr
@@ -24,7 +24,7 @@ strSTLC = MkStrength
   { strength = \p,x,mon => \case
     (App f x) => \theta => App (f theta) (x theta)
     (Lam str {ty1} body) => \theta =>
-        Lam str $ body $ extend p (mon.var (%% str))
+        Lam str $ body $ p.extend (mon.var (%% str))
       $ \v => mon.ren (theta v)
                       (\u => ThereVar u) -- Bug: can't eta-reduce
   }
-- 
cgit v1.2.3