fact: Definition lxor_test: bool := forallInt8 (fun i => forallInt8 (fun i' => native_repr (lxor i i') (xorB (bitsFromInt8 i) (bitsFromInt8 i')))).
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)