lean4-htt/src/Init/System
Leonardo de Moura fad6235abb feat: give a name to EIO Empty
@Kha I am calling it `ST` for lack of a better name. It makes some
sense since only the `IO.Ref` operations are in `EIO Empty` :)
That being said, it may confuse Haskell users.

BTW, I had to give the name to avoid a nontermination in the TC
procedure when using
```lean
instance EIOEmpty.monadLift {ε} : HasMonadLift (EIO Empty) (EIO ε) :=
{ monadLift := fun α => fromEmptyEIO }
```
2020-08-20 15:47:27 -07:00
..
FilePath.lean chore: remove { <structure-name> . ... } from stdlib 2020-05-20 15:43:21 -07:00
IO.lean feat: give a name to EIO Empty 2020-08-20 15:47:27 -07:00
IOError.lean fix: we cannot export constants 2020-03-23 11:54:54 -07:00
Platform.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00