Monad with LocalContext in State

Stream: lean4

[Alexander Bentkamp]

Hi, I would like to define a monad like MetaM, but with the LocalContext in the (modifiable) state instead of in the (read-only) context.
In essence, I would like to be able to write

let fvar ← withLocalDecl id b type
... fvar ...

instead

withLocalDecl id b type fun fvar => do
  ... fvar ...

Is there a way to do this so that I can still use the functions defined on MetaM in the new monad?

[Wojciech Nawrocki]

The usual way to make functions of type M a available in N a is to define a MonadLift M N instance. Since your monad has more capabilities than MetaM (can read/write the localctx), it should be possible to define MonadLift MetaM ... Then do notation can usually auto-lift calls in MetaM to the target.

[Alexander Bentkamp]

Ah, thanks, I will try that.