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

Equations

• p.toExpr = do let __x ← Lean.Meta.openAbstractMVarsResult p match __x 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.