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

fix(library/init/lean/elaborator): structure instances

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-19 15:35:11 +01:00
parent 543c3d21ff
commit 1708fc74f8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -304,7 +304,7 @@ def to_pexpr : syntax → elaborator_m expr
| none := pure sources
| some src := do { src ← to_pexpr src.source, pure $ sources ++ [src]},
let m := kvmap.set_nat {} `structure_instance fields.length,
let m := kvmap.set_nat {} "structure instance" fields.length,
let m := kvmap.set_bool m `catchall catchall,
let m := kvmap.set_name m `struct $
(mangle_ident <$> struct_inst_type.view.id <$> v.type).get_or_else name.anonymous,