From 5ef30a93007afb5a8aad0d07c4075ea62af3f858 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 16 Jan 2019 14:02:39 +0100 Subject: [PATCH] fix(library/init/lean/elaborator): `have` serialization --- library/init/lean/elaborator.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 35ad5bb8b7..19f70e0ea3 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -234,8 +234,8 @@ def to_pexpr : syntax → elaborator_m expr let proof := match v.proof with | have_proof.view.term hpt := hpt.term | have_proof.view.from hpf := hpf.from.proof, - lam ← expr.lam id binder_info.default <$> to_pexpr v.prop <*> to_pexpr proof, - pure $ expr.mk_annotation `have lam + lam ← expr.lam id binder_info.default <$> to_pexpr v.prop <*> to_pexpr v.body, + expr.app (expr.mk_annotation `have lam) <$> to_pexpr proof | @«show» := do let v := view «show» stx, prop ← to_pexpr v.prop,