max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/expander): expansion of parameterized let

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-21 22:07:10 +01:00
parent 814ceb43fe
commit 099354eb5f
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/lean/expander.lean
View file

@ -354,9 +354,9 @@ def let.transform : transformer :=
let v := view «let» stx,
match v.lhs with
| let_lhs.view.id {id := _, binders := [], type := some _} := no_expansion
| let_lhs.view.id lli@{id := _, binders := _, type := none} :=
| let_lhs.view.id lli@{id := _, binders := [], type := none} :=
pure $ review «let» {v with lhs := let_lhs.view.id {lli with type := some {type := review hole {}}}}
| let_lhs.view.id lli@{id := _, binders := _, type := some ty} :=
| let_lhs.view.id lli@{id := _, binders := _, type := ty} :=
let bindrs := binders.view.extended {
leading_ids := [],
remainder := binders_remainder.view.mixed $ lli.binders.map mixed_binder.view.bracketed} in
@ -364,8 +364,8 @@ def let.transform : transformer :=
lhs := let_lhs.view.id {
id := lli.id,
binders := [],
type := some {type := review pi {op := syntax.atom {val := "Π"}, binders := bindrs, range := ty.type}}},
body := review lambda {binders := bindrs, body := v.body}}
type := some {type := review pi {op := syntax.atom {val := "Π"}, binders := bindrs, range := get_opt_type ty}}},
value := review lambda {binders := bindrs, body := v.body}}
| let_lhs.view.pattern llp :=
pure $ review «match» {
scrutinees := [v.value],