jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

words: extend usimdN to allow returning a word of different size #75

Closed aqjune closed 1 year ago

aqjune commented 1 year ago

This is a simple pull request that extends the usimdN functions in Library/words.ml to allow returning a word whose size is different from the input word size.

The updated functions are to be used in an upcoming new pull request in awslabs/s2n-bignum that adds formal definitions of new SIMD operations.

jrh13 commented 1 year ago

Thanks, a useful generalization, I'll merge this in.