def Lean.mkBelow (declName : Lake.Name) : Lean.MetaM Unit

Equations

• Lean.mkBelow declName = Lean.mkBelowOrIBelow declName true

def Lean.mkIBelow (declName : Lake.Name) : Lean.MetaM Unit

Equations

• Lean.mkIBelow declName = Lean.mkBelowOrIBelow declName false

def Lean.mkBRecOnOrBInductionOn (indName : Lake.Name) (ind : Bool) : Lean.MetaM Unit

Constructs the .brecon or .binductionon definition for a inductive predicate.

For example for the List type, it constructs,

@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
    t
  ).1

and

@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
fun {α} {motive} t F_1 => (
  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
    ⟨F_1 [] True.intro, True.intro⟩
    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
    t
  ).1

Equations

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

def Lean.mkBRecOn (declName : Lake.Name) : Lean.MetaM Unit

Equations

• Lean.mkBRecOn declName = Lean.mkBRecOnOrBInductionOn declName false

def Lean.mkBInductionOn (declName : Lake.Name) : Lean.MetaM Unit

Equations

• Lean.mkBInductionOn declName = Lean.mkBRecOnOrBInductionOn declName true