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

fix(library/init/lean/elaborator): to_pexpr: explicitness modifiers

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-14 14:48:49 +01:00
parent 93d8431d00
commit 0945a87fbb
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

@ -254,8 +254,8 @@ def to_pexpr : syntax → elaborator_m expr
| @explicit := do
let v := view explicit stx,
let ann := match v.mod with
| explicit_modifier.view.explicit _ := `explicit
| explicit_modifier.view.partial_explicit _ := `partial_explicit,
| explicit_modifier.view.explicit _ := `@
| explicit_modifier.view.partial_explicit _ := `@@,
expr.mk_annotation ann <$> to_pexpr (review ident_univs v.id)
| @number := do
let v := view number stx,