Tactic Monad Definition

Stream: metaprogramming / tactics

[Tanner Duve]

Hi, where in the Lean docs can I find the monad instance for tactic defined explicitly?

[Adam Topaz]

src#Lean.Elab.Tactic.TacticM

[Adam Topaz]

Is that what you’re looking for?

[Adam Topaz]

Most of Lean's metaprogramming monads are defined as ReaderT Context (StateRefT State M) for some monad M. We have a summary of the hierarchy in the mathlib wiki: https://github.com/leanprover-community/mathlib4/wiki/Monad-map

[Tanner Duve]

This is what I was looking for. Thanks.