Lean 4 Info View

Stream: lean4

[Guilherme Silva]

Is it possible to create other kinds of info views in Lean?
For example, creating another tactic like Mtac2 of Coq or using it in another monad.

[Sebastian Ullrich]

If you can represent your custom goal state using the same data structure as the default one, this is possible. Otherwise, it will likely fall under https://github.com/leanprover/lean4/issues/399.