def Aesop.CasesPattern.toExpr (p : 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) : CasesTarget'
• patterns (ps : Array (Lean.Expr × Lean.Meta.SavedState)) : CasesTarget'

def Aesop.CasesTarget.toCasesTarget' : CasesTarget → Lean.MetaM 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 : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) : RuleTac

Equations

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

def Aesop.RuleTac.cases.findFirstApplicableHyp (target : 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 : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) (newGoals : Array Subgoal) (excluded : Array Lean.FVarId) (diff : GoalDiff) (goal : Lean.MVarId) : ScriptM (Option (Array Subgoal))