Monad map

graph TB
  TacticM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Tactic.TacticM'>TacticM</a>"]
  TermElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Term.TermElabM'>TermElabM</a>"]
  MetaM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.MetaM'>MetaM</a>"]
  CoreM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Core.CoreM'>CoreM</a>"]
  EIO["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=EIO'>EIO</a>"]
  CommandElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Command.CommandElabM'>CommandElabM</a>"]
  SimpM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.Simp.SimpM'>SimpM</a>"]
  FrontendM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Frontend.FrontendM'>FrontendM</a>"]

  TacticM --> TermElabM;
  TermElabM --> MetaM;
  MetaM --> CoreM;
  CoreM --> EIO;
  TermElabM -. Lean.Elab.Tactic.run .-> TacticM;
  CoreM -. MetaM.run .-> MetaM;
  EIO -. CoreM.run .-> CoreM;
  CommandElabM -. runTermElabM .-> TermElabM;
  CommandElabM -. liftTermElabM .-> TermElabM;
  CommandElabM -. liftCoreM .-> CoreM;
  CommandElabM --> EIO;
  IO -. MetaM.toIO .-> MetaM;
  IO -. CoreM.toIO .-> CoreM;
  IO --> EIO;
  SimpM --> MetaM;
  FrontendM -. runCommandElabM .-> CommandElabM;
  FrontendM --> IO;

Loading