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/Example.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/Example.idr')
| -rw-r--r-- | src/Example.idr | 2 |
1 files changed, 1 insertions, 1 deletions
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 } |