From bf886562886cedc00da696fcb479df939102fa9b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Dec 2020 15:11:28 -0800 Subject: [PATCH] feat: add `binrel!` parser It is a helper macro for using binary relations such as `<` and `>`. --- src/Lean/Parser/Term.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 1bc6d6c334..dba40bc3dd 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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