fact: Definition unop_tests x := let bitsX := bitsFromInt32 x in let toNatX := toNat bitsX in allb [:: native_repr (succ x) (incB bitsX) ; native_repr (lnot x) (invB bitsX) ; native_repr (neg x) (negB bitsX) ; native_repr (dec x) (decB bitsX) ; if (toNatX <= wordsize) then forallInt32 (fun y => let bitsY := bitsFromInt32 y in (binop_tests x bitsX y bitsY) && (shift_tests x toNatX y bitsY)) else forallInt32 (fun y => binop_tests x bitsX y (bitsFromInt32 y))].
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic