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

feat: add binrel! parser

Browse source 
It is a helper macro for using binary relations such as `<` and `>`.
This commit is contained in:
Leonardo de Moura 2020-12-29 15:11:28 -08:00
parent b0f1bfb580
commit bf88656288
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -175,6 +175,8 @@ def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
@[builtinTermParser] def noindex := parser! "noindex!" >> termParser maxPrec
@[builtinTermParser] def binrel := parser! "binrel!" >> ident >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := parser! "ensureExpectedType! " >> strLit >> termParser maxPrec