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

fix(library/init/lean/elaborator): have serialization

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-16 14:02:39 +01:00
parent dce62fc190
commit 5ef30a9300
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/elaborator.lean
View file

@ -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,