|
|
|---|
|
|
|
|---|
(n256-to-i256 x) → *
Function:
(defun n256-to-i256$inline (x) (declare (type (unsigned-byte 256) x)) (declare (xargs :guard (n256p x))) (mbe :logic (logext 256 x) :exec (if (< x 57896044618658097711785492504343953926634992332820282019728792003956564819968) x (- x 115792089237316195423570985008687907853269984665640564039457584007913129639936))))