def Aesop.CasesPattern.toExpr (p : Aesop.CasesPattern) : Lean.MetaM Lean.Expr

Equations

• p.toExpr = do let __discr ← Lean.Meta.openAbstractMVarsResult p match __discr with | (fst, fst_1, p) => pure p

inductive Aesop.CasesTarget' : Type

• decl (decl : Lean.Name) : Aesop.CasesTarget'
• patterns (ps : Array (Lean.Expr × Lean.Meta.SavedState)) : Aesop.CasesTarget'

def Aesop.CasesTarget.toCasesTarget' : Aesop.CasesTarget → Lean.MetaM Aesop.CasesTarget'

Equations

• One or more equations did not get rendered due to their size.
• (Aesop.CasesTarget.decl d).toCasesTarget' = pure (Aesop.CasesTarget'.decl d)

def Aesop.RuleTac.cases (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array Aesop.CtorNames) : Aesop.RuleTac

Equations

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

def Aesop.RuleTac.cases.findFirstApplicableHyp (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (excluded : Array Lean.FVarId) (goal : Lean.MVarId) : Lean.MetaM (Option Lean.FVarId)

Equations

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

partial def Aesop.RuleTac.cases.go (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array Aesop.CtorNames) (newGoals : Array Aesop.Subgoal) (excluded : Array Lean.FVarId) (diff : Aesop.GoalDiff) (goal : Lean.MVarId) : Aesop.ScriptM (Option (Array Aesop.Subgoal))