theorem Hex.Kernel.land_eq (a b : Nat) : a.land b = a &&& b

theorem Hex.Kernel.lor_eq (a b : Nat) : a.lor b = a ||| b

theorem Hex.Kernel.xor_eq (a b : Nat) : a.xor b = a ^^^ b

theorem Hex.Kernel.shiftRight_eq (a b : Nat) : a.shiftRight b = a >>> b

theorem Hex.Kernel.shiftLeft_eq (a b : Nat) : a.shiftLeft b = a <<< b

theorem Hex.Kernel.mul_eq (a b : Nat) : a.mul b = a * b

theorem Hex.Kernel.add_eq (a b : Nat) : a.add b = a + b

theorem Hex.Kernel.sub_eq (a b : Nat) : a.sub b = a - b

theorem Hex.Kernel.div_eq (a b : Nat) : a.div b = a / b

theorem Hex.Kernel.mod_eq (a b : Nat) : a.mod b = a % b

theorem Hex.Kernel.cond_beq {α : Type} (a b : Nat) (x y : α) : (bif a.beq b then x else y) = if a = b then x else y

theorem Hex.Kernel.cond_blt {α : Type} (a b : Nat) (x y : α) : (bif a.blt b then x else y) = if a < b then x else y

theorem Hex.Kernel.cond_ble {α : Type} (a b : Nat) (x y : α) : (bif a.ble b then x else y) = if a ≤ b then x else y

theorem Hex.Kernel.beq_eq_beq (a b : Nat) : a.beq b = (a == b)

theorem Hex.Kernel.blt_eq_decide (a b : Nat) : a.blt b = decide (a < b)

theorem Hex.Kernel.ble_eq_decide (a b : Nat) : a.ble b = decide (a ≤ b)

theorem Hex.Kernel.beq_eq_decide (a b : Nat) : a.beq b = decide (a = b)

theorem Hex.Kernel.cond_beq_true {α : Type} (a : Bool) (x y : α) : (bif a then x else y) = if a = true then x else y

def Hex.Kernel.iterUpImpl {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : α

The compiled form of iterUp.

Equations

• Hex.Kernel.iterUpImpl k f a = Hex.Kernel.iterUpImpl.go✝ f k 0 a

@[implemented_by Hex.Kernel.iterUpImpl]

def Hex.Kernel.iterUp {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : α

iterUp k f a = f (k - 1) (… (f 0 a)), one Nat.rec step per iteration.

Equations

• Hex.Kernel.iterUp k f a = Nat.rec (motive := fun (x : Nat) => α → α) (fun (a : α) => a) (fun (i : Nat) (ih : α → α) (a : α) => ih (f ((k.sub 1).sub i) a)) k a

theorem Hex.Kernel.iterUp_go {α : Type} (k : Nat) (f : Nat → α → α) (j : Nat) (a : α) : j ≤ k → Nat.rec (motive := fun (x : Nat) => α → α) (fun (a : α) => a) (fun (i : Nat) (ih : α → α) (a : α) => ih (f ((k.sub 1).sub i) a)) j a = List.foldl (fun (a : α) (i : Nat) => f i a) a (List.range' (k - j) j)

theorem Hex.Kernel.iterUp_eq_foldl {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : iterUp k f a = List.foldl (fun (a : α) (i : Nat) => f i a) a (List.range k)

def Hex.Kernel.fuelRecImpl {β : Type} : Nat → β → (β → β) → β

The compiled form of fuelRec.

Equations

• Hex.Kernel.fuelRecImpl 0 x✝¹ x✝ = x✝¹
• Hex.Kernel.fuelRecImpl k.succ x✝¹ x✝ = x✝ (Hex.Kernel.fuelRecImpl k x✝¹ x✝)

@[implemented_by Hex.Kernel.fuelRecImpl]

def Hex.Kernel.fuelRec {β : Type} (k : Nat) (base : β) (step : β → β) : β

fuelRec k base step = step (… (step base)), k times: the fuel-bounded recursion of a loop with an early exit as one Nat.rec step per unfolding (β is the loop's function type).

Equations

• Hex.Kernel.fuelRec k base step = Nat.rec base (fun (x : Nat) (ih : β) => step ih) k

theorem Hex.Kernel.fuelRec_zero {β : Type} (base : β) (step : β → β) : fuelRec 0 base step = base

theorem Hex.Kernel.fuelRec_succ {β : Type} (k : Nat) (base : β) (step : β → β) : fuelRec (k + 1) base step = step (fuelRec k base step)

def Hex.Kernel.mapRange {α : Type} (k : Nat) (f : Nat → α) : List α

(List.range k).map f, built by the loop driver.

Equations

• Hex.Kernel.mapRange k f = (Hex.Kernel.iterUp k (fun (o : Nat) (acc : List α) => f o :: acc) []).reverse

theorem Hex.Kernel.mapRange_eq {α : Type} (k : Nat) (f : Nat → α) : mapRange k f = List.map f (List.range k)

def Hex.Kernel.allRange (k : Nat) (p : Nat → Bool) : Bool

(List.range k).all p, by the loop driver.

Equations

• Hex.Kernel.allRange k p = Hex.Kernel.iterUp k (fun (v : Nat) (b : Bool) => b && p v) true

theorem Hex.Kernel.allRange_eq (k : Nat) (p : Nat → Bool) : allRange k p = (List.range k).all p