English
ldiff(a,b) computes the bitwise difference: at each position the resulting bit is a_i ∧ ¬b_i.
Русский
ldiff(a,b) выполняет побитовую разность: на каждой позиции i получаемый бит равен a_i ∧ ¬b_i.
LaTeX
$$$$ \forall i:\, \text{bit}_i(\mathrm{ldiff}(a,b)) = \text{bit}_i(a) \land \lnot \text{bit}_i(b). $$$$
Lean4
/-- `ldiff a b` performs bitwise set difference. For each corresponding
pair of bits taken as Booleans, say `aᵢ` and `bᵢ`, it applies the
Boolean operation `aᵢ ∧ ¬bᵢ` to obtain the `iᵗʰ` bit of the result. -/
def ldiff : ℕ → ℕ → ℕ :=
bitwise fun a b => a && not b
