From e90a79f996072d1af67910df092969ee7eb1a823 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jun 2019 14:19:24 -0700 Subject: [PATCH] chore(tests/playground/parser/syntax): fix test --- tests/playground/parser/syntax.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/playground/parser/syntax.lean b/tests/playground/parser/syntax.lean index 199e198ef4..0df325e6e6 100644 --- a/tests/playground/parser/syntax.lean +++ b/tests/playground/parser/syntax.lean @@ -148,7 +148,7 @@ def flipScopes (scopes : MacroScopes) : Syntax → Syntax @[inline] def toSyntaxNode {α : Type} (s : Syntax) (base : α) (fn : SyntaxNode → α) : α := match s with | Syntax.node kind args [] := fn ⟨Syntax.node kind args [], IsNode.mk _ _ _⟩ -| Syntax.node kind args scopes := fn ⟨Syntax.node kind (args.hmap (flipScopes scopes)) [], IsNode.mk _ _ _⟩ +| Syntax.node kind args scopes := fn ⟨Syntax.node kind (args.map (flipScopes scopes)) [], IsNode.mk _ _ _⟩ | other := base local attribute [instance] monadInhabited