MonadState namespacing

Stream: lean4

[Brendan Seamas Murphy]

Why does MonadState export get, modifyGet and MonadStateOf export set? presumably this has to do with the semiOutParam modifier? I'm confused why these typeclasses are designed the way they are, and which one I should be using in client code

[Brendan Seamas Murphy]

Also, why does instMonadStateOf take a [MonadLift m n] parameter instead of [MonadLiftT m n]? Is this to make sure we only "peel back" the outermost layer of state when using the instMonadStateOf instance?