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

chore: use MetaM.toIO

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-20 19:20:11 -07:00
parent c018c333b4
commit d519a5d526
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/Reformat.lean
View file

@ -14,7 +14,7 @@ let (debug, f) : Bool × String := match args with
table ← Parser.builtinTokenTable.get;
env ← mkEmptyEnvironment;
stx ← Lean.Parser.parseFile env args.head!;
(f, _) ← IO.runMeta (PrettyPrinter.ppModule table stx) env { opts := KVMap.insert {} `trace.PrettyPrinter.format debug };
f ← (PrettyPrinter.ppModule table stx).toIO env (KVMap.insert {} `trace.PrettyPrinter.format debug);
IO.print f;
let inputCtx := Parser.mkInputContext (toString f) "<foo>";
let (stx', state, messages) := Parser.parseHeader env inputCtx;

5
tests/lean/run/Reparen.lean
View file

@ -30,8 +30,8 @@ IO.print s;
let cmds := stx.getArgs.extract 1 stx.getArgs.size;
cmds.forM $ fun cmd => do
let cmd := unparen cmd;
(cmd, _) ← IO.runMeta (PrettyPrinter.parenthesizeCommand cmd)
env { opts := KVMap.insert {} `trace.PrettyPrinter.parenthesize debug };
cmd ← (PrettyPrinter.parenthesizeCommand cmd).toIO
env (KVMap.insert {} `trace.PrettyPrinter.parenthesize debug);
some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
IO.print s
@ -50,4 +50,3 @@ open Lean
syntax:80 term " ^~ " term:80 : term
syntax:70 term " *~ " term:71 : term
#eval check $ Unhygienic.run `(((1 + 2) *~ 3) ^~ 4)