Equations
- Lean.mkBelow declName = Lean.mkBelowOrIBelow declName true
Instances For
Equations
- Lean.mkIBelow declName = Lean.mkBelowOrIBelow declName false
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
- Lean.mkBRecOn declName = Lean.mkBRecOnOrBInductionOn declName false
Instances For
Equations
- Lean.mkBInductionOn declName = Lean.mkBRecOnOrBInductionOn declName true