From 6db45891e206929df3e8bbe09cb4e744617c5303 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Oct 2020 14:20:40 -0700 Subject: [PATCH] feat: add `typeOf!` and `ensureTypeOf!` parsers --- src/Lean/Parser/Term.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 76433d1dc8..c058c71625 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -170,6 +170,9 @@ def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", " @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec @[builtinTermParser] def decide := parser! "decide! " >> termParser maxPrec +@[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec +@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser + @[builtinTermParser] def not := parser! "¬" >> termParser 40 @[builtinTermParser] def bnot := parser! "!" >> termParser 40 -- symbol precedence should be higher, but must match the one of `sub` below