Skip to content

Monad map

Eric Wieser edited this page Oct 10, 2023 · 20 revisions
flowchart TB
  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
Clone this wiki locally