From aa66fc376b9c0be4e87d9ade0e8dcc60014ae341 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Jun 2020 15:46:56 -0700 Subject: [PATCH] chore: fix test --- tests/lean/run/termParserAttr.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index b1f405173a..015ceaa66a 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -18,10 +18,10 @@ open Lean.Parser @[termParser] def boo : ParserDescr := ParserDescr.node `boo (ParserDescr.andthen - (ParserDescr.symbol "[|" 0) + (ParserDescr.symbol "[|") (ParserDescr.andthen (ParserDescr.parser `term 0) - (ParserDescr.symbol "|]" 0))) + (ParserDescr.symbol "|]"))) open Lean.Elab.Term