From e3c3fc31658043461d6d464b6c8dfcecfd4b5740 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Feb 2021 16:36:30 -0800 Subject: [PATCH] feat: add helper macro `forIn!` We are going to write a custom elaborator for `forIn` applications. --- 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 67a4534de0..5aa4b9fe96 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -188,6 +188,8 @@ def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls @[builtinTermParser] def binrel := parser! "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec +@[builtinTermParser] def forInMacro := parser! "forIn! " >> termParser maxPrec >> 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