search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

read Ltac2 integer bits using bitwise right shift #355

Closed robertzhidealx closed 1 year ago

robertzhidealx commented 1 year ago

Now that Ltac2 supports integer operations like the bitwise right shift (Int.lsr), we can use it directly for converting an Ltac2 integer into a bool list representation of its bits, obviating the original workaround.

Compiles in Coq version 8.17.0.

robertzhidealx commented 1 year ago

Please squash and merge if approved. Thanks!

samuelgruetter commented 1 year ago

nice, thanks :+1: