structure Lean.Meta.CasesOnApp : Type

• declName : Lake.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
• propOnly : Bool

  true if the casesOn can only eliminate into Prop

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[is, 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].

This is used in in Lean.Elab.PreDefinition.WF.Fix when replacing recursive calls with calls to the argument provided by fix to refine the termination argument, which may mention major. See there for how to use this function.

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 to CasesOnApp.addArg, but returns none on failure.

Equations

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

def Lean.Meta.CasesOnApp.refineThrough (c : Lean.Meta.CasesOnApp) (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Given a casesOn application c of the form

casesOn As (fun is x => motive[is, 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 B[is, major] (which may not be a type, e.g. n : Nat) for every alternative i, construct the expression fun ys_i => B[_, C_i[ys_i]]

This is similar to CasesOnApp.addArg when you only have an expression to refined, and not a type with a value.

This is used in in Lean.Elab.PreDefinition.WF.GuessFix when constructing the context of recursive calls to refine the functions' paramter, which may mention major. See there for how to use this function.

Equations

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

def Lean.Meta.CasesOnApp.refineThrough? (c : Lean.Meta.CasesOnApp) (e : Lean.Expr) : Lean.MetaM (Option (Array Lean.Expr))

A non-failing version of CasesOnApp.refineThrough

Equations

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