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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-06 14:05:00 -07:00
parent 3293e9ef08
commit 8acbb55632
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/Reformat.lean
View file

@ -1,5 +1,5 @@
/-! Parse and reformat file -/
import Lean.PrettyPrinter
/-! Parse and reformat file -/
open Lean
open Lean.Elab

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

@ -1,5 +1,5 @@
/-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
import Lean.Parser
/-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
open Lean
open Std.Format open Std