Documentation

Init.Fix

source
def bfix1 {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :
Nat → α → β
Equations
source
@[extern c inline "lean_fixpoint(#4, #5)"]
def fixCore1 {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :
α → β
Equations
source
@[inline]
def fixCore {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :
α → β
Equations
source
@[inline]
def fix1 {α : Type u} {β : Type u} [inst : Inhabited β] (rec : (α → β) → α → β) :
α → β
Equations
source
@[inline]
def fix {α : Type u} {β : Type u} [inst : Inhabited β] (rec : (α → β) → α → β) :
α → β
Equations
source
def bfix2 {α₁ : Type u} {α₂ : Type u} {β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :
Nat → α₁ → α₂ → β
Equations
  • bfix2 base rec 0 _fun_discr _fun_discr = base _fun_discr _fun_discr
  • bfix2 base rec (Nat.succ n) _fun_discr _fun_discr = rec (bfix2 base rec n) _fun_discr _fun_discr
source
@[extern c inline "lean_fixpoint2(#5, #6, #7)"]
def fixCore2 {α₁ : Type u} {α₂ : Type u} {β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :
α₁ → α₂ → β
Equations
source
@[inline]
def fix2 {α₁ : Type u} {α₂ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :
α₁ → α₂ → β
Equations
source
def bfix3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :
Nat → α₁ → α₂ → α₃ → β
Equations
  • bfix3 base rec 0 _fun_discr _fun_discr _fun_discr = base _fun_discr _fun_discr _fun_discr
  • bfix3 base rec (Nat.succ n) _fun_discr _fun_discr _fun_discr = rec (bfix3 base rec n) _fun_discr _fun_discr _fun_discr
source
@[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"]
def fixCore3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :
α₁ → α₂ → α₃ → β
Equations
source
@[inline]
def fix3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :
α₁ → α₂ → α₃ → β
Equations
source
def bfix4 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) :
Nat → α₁ → α₂ → α₃ → α₄ → β
Equations
  • bfix4 base rec 0 _fun_discr _fun_discr _fun_discr _fun_discr = base _fun_discr _fun_discr _fun_discr _fun_discr
  • bfix4 base rec (Nat.succ n) _fun_discr _fun_discr _fun_discr _fun_discr = rec (bfix4 base rec n) _fun_discr _fun_discr _fun_discr _fun_discr
source
@[extern c inline "lean_fixpoint4(#7, #8, #9, #10, #11)"]
def fixCore4 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) :
α₁ → α₂ → α₃ → α₄ → β
Equations
source
@[inline]
def fix4 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) :
α₁ → α₂ → α₃ → α₄ → β
Equations
source
def bfix5 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) :
Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
Equations
  • bfix5 base rec 0 _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr = base _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr
  • bfix5 base rec (Nat.succ n) _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr = rec (bfix5 base rec n) _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr
source
@[extern c inline "lean_fixpoint5(#8, #9, #10, #11, #12, #13)"]
def fixCore5 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) :
α₁ → α₂ → α₃ → α₄ → α₅ → β
Equations
source
@[inline]
def fix5 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) :
α₁ → α₂ → α₃ → α₄ → α₅ → β
Equations
source
def bfix6 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {α₆ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) :
Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
Equations
  • bfix6 base rec 0 _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr = base _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr
  • bfix6 base rec (Nat.succ n) _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr = rec (bfix6 base rec n) _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr _fun_discr
source
@[extern c inline "lean_fixpoint6(#9, #10, #11, #12, #13, #14, #15)"]
def fixCore6 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {α₆ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) :
α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
Equations
source
@[inline]
def fix6 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {α₆ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) :
α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
Equations