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