natBitwise — Mathlib

English

natBitwise f m n constructs an integer from natural bitwise values using f on the bits of m and n.

Русский

natBitwise f m n строит целое число из битовых значений на натуральных разрядах m и n с помощью f.

LaTeX

$$$\\mathrm{natBitwise}: (\\mathsf{Bool}\\to\\mathsf{Bool}\\to \\mathsf{Bool}) \\to \\mathbb{N} \\to \\mathbb{N} \\to \\mathbb{Z}$$$

Lean4

/-- `Int.natBitwise` is an auxiliary definition for `Int.bitwise`. -/
def natBitwise (f : Bool → Bool → Bool) (m n : ℕ) : ℤ :=
  cond (f false false) -[Nat.bitwise (fun x y => not (f x y)) m n+1] (Nat.bitwise f m n)

Похожие утверждения