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

feat(tests/playground/patch): path equation syntax

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-08 20:57:54 -07:00
parent f546b13b6c
commit 022a130b86
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/playground/patch.lean
View file

@ -1,9 +1,19 @@
import init.lean.parser import init.lean.parser
import init.lean.parser.transform
open Lean open Lean
open Lean.Parser open Lean.Parser
def fixEqnSyntax (stx : Syntax) : Syntax := def fixEqnSyntax (stx : Syntax) : Syntax :=
stx stx.rewriteBottomUp $ fun stx =>
stx.ifNodeKind `Lean.Parser.Term.equation3
(fun stx =>
let args := stx.getArgs;
let args := args.modify 1 $ fun patterns =>
let patterns := patterns.asNode.updateArgs $ fun args => args.map Syntax.removeParen;
patterns.manyToSepBy ",";
let args := args.modify 2 $ fun assignTk => assignTk.setAtomVal "=>";
Syntax.node `Lean.Parser.Term.matchAlt args)
(fun _ => stx)
def main (xs : List String) : IO Unit := def main (xs : List String) : IO Unit :=
do do