From 022a130b867c7ec5c3169fbe74fa3f1a2c0180a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Aug 2019 20:57:54 -0700
Subject: [PATCH] feat(tests/playground/patch): path equation syntax

---
 tests/playground/patch.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tests/playground/patch.lean b/tests/playground/patch.lean
index 3f45a83c98..5c194797e6 100644
--- a/tests/playground/patch.lean
+++ b/tests/playground/patch.lean
@@ -1,9 +1,19 @@
 import init.lean.parser
+import init.lean.parser.transform
 open Lean
 open Lean.Parser
 
 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 :=
 do