Calling CommandElabM from MetaM

Stream: metaprogramming / tactics

[Eric Wieser]

Is it possible to jump monads in this direction? The motivation is to be able to generate a Command term, then elaborate it in some discarded environment to check that it round-trips to the expected object.

[Kyle Miller]

Yes, liftCommandElabM. It has some bugs, though there is a PR (lean4#5800)

[Eric Wieser]

Added to the monad map, thanks!