From 14414e34009dda02cbcd50f14092261df8b4a64f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Oct 2020 17:04:35 -0700 Subject: [PATCH] feat: nested `do` parser --- src/Lean/Parser/Do.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index f6fe09f6b2..78d951bf98 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -95,6 +95,7 @@ Note that parser priorities would not solve this problem since the `doIf` parser parser is succeeding. -/ @[builtinDoElemParser] def doExpr := parser! notFollowedByRedefinedTermToken >> termParser +@[builtinDoElemParser] def doNested := parser! "do " >> doSeq @[builtinTermParser] def «do» := parser!:maxPrec "do " >> doSeq