Documentation

Lean.Meta.Constructions.BRecOn

Equations
Instances For
    Equations
    Instances For

      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.
      Instances For
        Equations
        Instances For