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

feat: add notation for helper elaboration function

Browse source 
This similar to `binrel%` but for binary operators.

See issue #382
This commit is contained in:
Leonardo de Moura 2021-04-30 17:14:17 -07:00
parent ee6a9e74e8
commit f8ac5d25dd
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Term.lean
View file

@ -188,7 +188,8 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def noindex := leading_parser "no_index " >> termParser maxPrec
@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser "forIn% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec