Operator for Bitwise-Not

Stream: new members

[Philogy]

Does Lean4 have bitwise-NOT for its types? What's the operator? I assume no for Nat since it doesn't make sense in that context but maybe for Fin N types of base-2?

Appreciate any suggestions.

[Kyle Miller]

Yes:

variable (x : BitVec 32)
#check ~~~x

[Julian Berman]

It would appear to be docs#Complement