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

chore(library/system/IO): suppress unnecessary universe

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-26 11:19:52 -07:00
parent a5908ad671
commit 6eb377033b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/system/IO.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
-/
constant IO : Type → Type
constant IO.{l} : Type.{l} → Type.{l}
constant functorIO : functor IO
constant monadIO : monad IO