structure Lean.Meta.CasesOnApp : Type

• declName : Lean.Name
• us : List Lean.Level
• params : Array Lean.Expr
• motive : Lean.Expr
• indices : Array Lean.Expr
• major : Lean.Expr
• alts : Array Lean.Expr
• altNumParams : Array Nat
• remaining : Array Lean.Expr

• true if the casesOn can only eliminate into Prop

  propOnly : Bool

def Lean.Meta.toCasesOnApp? (e : Lean.Expr) : Lean.MetaM (Option Lean.Meta.CasesOnApp)

Return some c if e is a casesOn application.

Equations

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

def Lean.Meta.CasesOnApp.toExpr (c : Lean.Meta.CasesOnApp) : Lean.Expr

Convert c back to Expr

Equations

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

def Lean.Meta.CasesOnApp.addArg (c : Lean.Meta.CasesOnApp) (arg : Lean.Expr) (checkIfRefined : optParam Bool false) : Lean.MetaM Lean.Meta.CasesOnApp

Given a casesOn application c of the form

casesOn As (fun is x => motive[i, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining

and an expression e : B[is, major], construct the term

casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining

We use kabstract to abstract the is and major from B[is, major].

Equations

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

def Lean.Meta.CasesOnApp.addArg.updateAlts (c : Lean.Meta.CasesOnApp) (checkIfRefined : optParam Bool false) (argType : Lean.Expr) (auxType : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Equations

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

def Lean.Meta.CasesOnApp.addArg? (c : Lean.Meta.CasesOnApp) (arg : Lean.Expr) (checkIfRefined : optParam Bool false) : Lean.MetaM (Option Lean.Meta.CasesOnApp)

Similar CasesOnApp.addArg, but returns none on failure.

Equations

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