Lean.Meta.CasesOn

source

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

source

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.

source

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.

source

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.

source

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.

source

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.