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

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

• Aesop.runTacticMAsTermElabM goal x = (ReaderT.run x { elaborator := Lean.Name.anonymous }).run' { goals := [goal] }

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

Equations

• Aesop.runTacticMAsElabM x = do let __do_lift ← read liftM (Aesop.runTacticMAsTermElabM __do_lift.goal x)

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

Equations

• Aesop.withFullElaboration x = Lean.Elab.Term.withSynthesize (Lean.Elab.Term.withoutErrToSorry (Lean.Elab.Term.withoutAutoBoundImplicit x))

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

Equations

• Aesop.elabRuleTermForApplyLikeCore goal stx = Aesop.withFullElaboration (Aesop.runTacticMAsTermElabM goal (Lean.Elab.Tactic.elabTermForApply stx.raw false))

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

Equations

• Aesop.elabRuleTermForApplyLikeMetaM goal stx = (Aesop.elabRuleTermForApplyLikeCore goal stx).run'

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

Equations

• Aesop.elabRuleTermForApplyLike stx = do let __do_lift ← read liftM (Aesop.elabRuleTermForApplyLikeCore __do_lift.goal stx)

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)

Equations

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

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

Equations

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

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)

Equations

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

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

Equations

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

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)

Equations

• Aesop.elabRuleTermForSimpMetaM goal term ctx simprocs isSimpAll = (Aesop.elabRuleTermForSimpCore goal term ctx simprocs isSimpAll).run'