max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/playground/parser/syntax): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-05 14:19:24 -07:00
parent e081332ef8
commit e90a79f996
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/playground/parser/syntax.lean
View file

@ -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