Init.Fix

source

def bfix1 {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :

Nat → α → β

Equations

bfix1 base rec 0 x = base x
bfix1 base rec (Nat.succ n) x = rec (bfix1 base rec n) x

source

@[extern c inline "lean_fixpoint(#4, #5)"]

def fixCore1 {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :

α → β

Equations

fixCore1 base rec = bfix1 base rec USize.size

source

@[inline]

def fixCore {α : Type u} {β : Type u} (base : α → β) (rec : (α → β) → α → β) :

α → β

Equations

fixCore base rec = fixCore1 base rec

source

@[inline]

def fix1 {α : Type u} {β : Type u} [inst : Inhabited β] (rec : (α → β) → α → β) :

α → β

Equations

fix1 rec = fixCore1 (fun x => default) rec

source

@[inline]

def fix {α : Type u} {β : Type u} [inst : Inhabited β] (rec : (α → β) → α → β) :

α → β

Equations

fix rec = fixCore1 (fun x => default) rec

source

def bfix2 {α₁ : Type u} {α₂ : Type u} {β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :

Nat → α₁ → α₂ → β

Equations

bfix2 base rec 0 x x = base x x
bfix2 base rec (Nat.succ n) x x = rec (bfix2 base rec n) x x

source

@[extern c inline "lean_fixpoint2(#5, #6, #7)"]

def fixCore2 {α₁ : Type u} {α₂ : Type u} {β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :

α₁ → α₂ → β

Equations

fixCore2 base rec = bfix2 base rec USize.size

source

@[inline]

def fix2 {α₁ : Type u} {α₂ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) :

α₁ → α₂ → β

Equations

fix2 rec = fixCore2 (fun x x => default) rec

source

def bfix3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :

Nat → α₁ → α₂ → α₃ → β

Equations

bfix3 base rec 0 x x x = base x x x
bfix3 base rec (Nat.succ n) x x x = rec (bfix3 base rec n) x x x

source

@[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"]

def fixCore3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :

α₁ → α₂ → α₃ → β

Equations

fixCore3 base rec = bfix3 base rec USize.size

source

@[inline]

def fix3 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) :

α₁ → α₂ → α₃ → β

Equations

fix3 rec = fixCore3 (fun x x x => default) rec

source

def bfix4 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) :

Nat → α₁ → α₂ → α₃ → α₄ → β

Equations

bfix4 base rec 0 x x x x = base x x x x
bfix4 base rec (Nat.succ n) x x x x = rec (bfix4 base rec n) x x x x

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

fixCore4 base rec = bfix4 base rec USize.size

source

@[inline]

def fix4 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) :

α₁ → α₂ → α₃ → α₄ → β

Equations

fix4 rec = fixCore4 (fun x x x x => default) rec

source

def bfix5 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) :

Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β

Equations

bfix5 base rec 0 x x x x x = base x x x x x
bfix5 base rec (Nat.succ n) x x x x x = rec (bfix5 base rec n) x x x x x

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

fixCore5 base rec = bfix5 base rec USize.size

source

@[inline]

def fix5 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) :

α₁ → α₂ → α₃ → α₄ → α₅ → β

Equations

fix5 rec = fixCore5 (fun x x x x x => default) rec

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 x x x x x x = base x x x x x x
bfix6 base rec (Nat.succ n) x x x x x x = rec (bfix6 base rec n) x x x x x x

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

fixCore6 base rec = bfix6 base rec USize.size

source

@[inline]

def fix6 {α₁ : Type u} {α₂ : Type u} {α₃ : Type u} {α₄ : Type u} {α₅ : Type u} {α₆ : Type u} {β : Type u} [inst : Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) :

α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β

Equations

fix6 rec = fixCore6 (fun x x x x x x => default) rec