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

feat(library/init/lean/elaborator): inaccessible

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-20 16:41:33 +01:00
parent 69e363446d
commit b24796d98e
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -271,6 +271,9 @@ def to_pexpr : syntax → elaborator_m expr
| explicit_modifier.view.explicit _ := `@
| explicit_modifier.view.partial_explicit _ := `@@,
expr.mk_annotation ann <$> to_pexpr (review ident_univs v.id)
| @inaccessible := do
let v := view inaccessible stx,
expr.mk_annotation `innaccessible <$> to_pexpr v.term -- sic
| @number := do
let v := view number stx,
pure $ expr.lit $ literal.nat_val v.to_nat