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

fix(library/playground/patch): updateArgs => modifyArgs

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-09 16:05:29 -07:00
parent 54312cfa51
commit f8199bb540
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/patch.lean
View file

@ -9,7 +9,7 @@ stx.rewriteBottomUp $ fun stx =>
(fun stx =>
let args := stx.getArgs;
let args := args.modify 1 $ fun patterns =>
let patterns := patterns.asNode.updateArgs $ fun args => args.map Syntax.removeParen;
let patterns := patterns.asNode.modifyArgs $ fun args => args.map Syntax.removeParen;
patterns.manyToSepBy ",";
let args := args.modify 2 $ fun assignTk => assignTk.setAtomVal "=>";
Syntax.node `Lean.Parser.Term.matchAlt args)