From 849311af001dc42b2bc999e4d5c6698f5ab03f11 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Aug 2019 10:47:19 -0700 Subject: [PATCH] test(tests/playground/patch): do-nothing transformer --- tests/playground/patch.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/playground/patch.lean diff --git a/tests/playground/patch.lean b/tests/playground/patch.lean new file mode 100644 index 0000000000..3f45a83c98 --- /dev/null +++ b/tests/playground/patch.lean @@ -0,0 +1,16 @@ +import init.lean.parser +open Lean +open Lean.Parser + +def fixEqnSyntax (stx : Syntax) : Syntax := +stx + +def main (xs : List String) : IO Unit := +do +[fname] ← pure xs | throw (IO.userError "usage `patch `"); +env ← mkEmptyEnvironment; +stx ← parseFile env fname; +let stx := fixEqnSyntax stx; +match stx.reprint with +| some out => IO.print out +| none => throw (IO.userError "failed to reprint")