From 099354eb5f9c0dcadeb95bfc00d10ff8e1e82cf8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Jan 2019 22:07:10 +0100 Subject: [PATCH] fix(library/init/lean/expander): expansion of parameterized `let` --- library/init/lean/expander.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 3c74cc6b32..3a87d45b50 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -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],