John RegehrMar 22

wow so glad I can extract this minimal and efficient C++ from my verified Kernighan popcount in Lean 😅

https://gist.github.com/regehr/3461027009efbe9452d8a5c343174443

gist:3461027009efbe9452d8a5c343174443

GitHub Gist: instantly share code, notes, and snippets.

Gist
Show threadJohn RegehrMar 22
after much struggling I got the code below, which turns into the instructions that I wanted! but that's as much a testament to modern compilers as it is to Lean :)
Show threadash
@regehr Someone should subject themselves to the torment of doing this in idris, rocq, liquid haskell, and just like basic OCaml and then make a tier list if their sanity is still in tact
Mar 23 at 5:48amWeb