def Auto.genMonadContext : Lean.ParserDescr

Equations

• Auto.genMonadContext = Lean.ParserDescr.node `Auto.genMonadContext 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#genMonadContext") (Lean.ParserDescr.cat `term 0))

def Auto.genMonadState : Lean.ParserDescr

Equations

• Auto.genMonadState = Lean.ParserDescr.node `Auto.genMonadState 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#genMonadState") (Lean.ParserDescr.cat `term 0))

def Auto.structureProjs (structTy : Lean.Expr) : Lean.CoreM (Lean.Name × Lean.Expr × Array (Lean.Name × Lean.Expr))

instStructTy: An expression of the form <structure> param₁ param₂ ⋯ paramₙ Name: The name of the structure Expr: <structure>.mk with parameters instantiated Array (Name × Expr) Name: Name of the field Expr: The projection function of this field, with parameters instantiated

Equations

• One or more equations did not get rendered due to their size.

def Auto.elabGenMonadContext : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.

def Auto.elabGenMonadState : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.