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

test(tests/playground/patch): do-nothing transformer

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-08 10:47:19 -07:00
parent 10a8822ac5
commit 849311af00
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/playground/patch.lean Normal file
View file

@ -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 <file-name>`");
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")