def Aesop.elabGlobalRuleIdent? (stx : Lean.Term) : Lean.Elab.TermElabM (Option Lean.Name)

def Aesop.matchInductiveTypeSynonym? (decl : Lean.Name) : Lean.MetaM (Option Lean.InductiveVal)

def Aesop.elabInductiveRuleIdent? (stx : Lean.Term) (md : Lean.Meta.TransparencyMode) : Lean.Elab.TermElabM (Option (Lean.Name × Lean.InductiveVal))

Elaborate an identifier for a rule that applies to inductive types, e.g. cases. The identifier must unambiguously refer to a global constant that is either an inductive type or reduces to one. For the reduction test, we use the larger transparency among default and md.

def Aesop.runTacticMAsTermElabM {α : Type} (goal : Lean.MVarId) (x : Lean.Elab.Tactic.TacticM α) : Lean.Elab.TermElabM α

def Aesop.runTacticMAsElabM {α : Type} (x : Lean.Elab.Tactic.TacticM α) : ElabM α

def Aesop.withFullElaboration {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

def Aesop.elabRuleTermForApplyLikeCore (goal : Lean.MVarId) (stx : Lean.Term) : Lean.Elab.TermElabM Lean.Expr

def Aesop.elabRuleTermForApplyLikeMetaM (goal : Lean.MVarId) (stx : Lean.Term) : Lean.MetaM Lean.Expr

def Aesop.elabRuleTermForApplyLike (stx : Lean.Term) : ElabM Lean.Expr

def Aesop.elabSimpTheorems (stx : Lean.Syntax) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (isSimpAll : Bool) : Lean.Elab.Tactic.TacticM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)

def Aesop.mkSimpArgs (simpTheorem : Lean.Term) : Lean.Syntax

def Aesop.elabRuleTermForSimpCore (goal : Lean.MVarId) (term : Lean.Term) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (isSimpAll : Bool) : Lean.Elab.TermElabM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)

def Aesop.checkElabRuleTermForSimp (term : Lean.Term) (isSimpAll : Bool) : ElabM Unit

def Aesop.elabRuleTermForSimpMetaM (goal : Lean.MVarId) (term : Lean.Term) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (isSimpAll : Bool) : Lean.MetaM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)