fsdoc: no-summary-found
fsdoc: no-comment-found
let ((shift_right (a:t) (s:UInt32.t)):(Pure t ((requires (/\(<=(0, v a), <(UInt32.v s, n))))) ((ensures ((fun c -> =(FStar.Int.shift_right (v a) (UInt32.v s), v c))))))):(Mk (shift_right (v a) (UInt32.v s)))If a is negative the result is implementation-defined
let ((shift_left (a:t) (s:UInt32.t)):(Pure t ((requires (/\(/\(<=(0, v a), <=(*(v a, pow2 (UInt32.v s)), max_int n)), <(UInt32.v s, n))))) ((ensures ((fun c -> =(FStar.Int.shift_left (v a) (UInt32.v s), v c))))))):(Mk (shift_left (v a) (UInt32.v s)))If a is negative or a * pow2 s is not representable the result is undefined