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

chore(tests/lean/run/IO3): remove unnecessary 'open'

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-25 16:05:39 -07:00
parent 4b002e5bf0
commit d763ea1abf
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/run/IO3.lean
View file

@ -1,5 +1,4 @@
import system.IO
open string
definition main : IO unit :=
do { l ← get_line,