lean4
lean4 copied to clipboard
feat: allow `EStateM` to be used polymorphically
This doesn't change IO
or ST
, but does enable downstream projects like Mathlib
to use EStateM
for their own purposes with full universe polymorphism.
The alternative is defining an entire copy of EStateM
, which is a lot of boilerplate.
Notably, the generalized EStateM.map
can be invoked (in the non-monadic spelling) with ULift.up
to move between universes.
Summary
Link to RFC
or bug
issue: this is a prerequisite for #3011, but may be justified in its own right.