search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

Notation pow2 #1

Closed vmurali closed 6 years ago

vmurali commented 6 years ago

Changed pow2 to be a notation for (Nat.pow 2). This enables using theorems about Nat.pow, which is quite extensive

samuelgruetter commented 6 years ago

Thanks, just tried it out on my compiler project, and it doesn't break anything, and the fiat-crypto people told me they're ok with it as well, so I'm merging this.