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

feat(library/init/lean/{parser/term,elaborator}): support @& borrowed annotations

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-14 17:49:00 +01:00 • committed by Leonardo de Moura
parent 9da149c2df
commit dbc470d7e4
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -277,6 +277,9 @@ def to_pexpr : syntax → elaborator_m expr
| @inaccessible := do
let v := view inaccessible stx,
expr.mk_annotation `innaccessible <$> to_pexpr v.term -- sic
| @borrowed := do
let v := view borrowed stx,
expr.mk_annotation `borrowed <$> to_pexpr v.term
| @number := do
let v := view number stx,
pure $ expr.lit $ literal.nat_val v.to_nat

7
library/init/lean/parser/term.lean
View file

@ -340,6 +340,10 @@ node! anonymous_inaccessible ["._":max_prec]
def sorry.parser : term_parser :=
node! «sorry» ["sorry":max_prec]
@[derive parser.has_tokens parser.has_view]
def borrowed.parser : term_parser :=
node! borrowed ["@&":max_prec, term: term.parser]
-- TODO(Sebastian): replace with attribute
@[derive has_tokens]
def builtin_leading_parsers : token_map term_parser := token_map.of_list [
@ -369,7 +373,8 @@ def builtin_leading_parsers : token_map term_parser := token_map.of_list [
("{", subtype.parser),
(".(", inaccessible.parser),
("._", anonymous_inaccessible.parser),
("sorry", sorry.parser)
("sorry", sorry.parser),
("@&", borrowed.parser)
]
@[derive parser.has_tokens parser.has_view]