John Regehrwow so glad I can extract this minimal and efficient C++ from my verified Kernighan popcount in Lean 😅
https://gist.github.com/regehr/3461027009efbe9452d8a5c343174443
Whine Spectator@regehr how does it look at the other end of your compiler?
@secretasianman bad. there’s some proof-related code that is getting turned into C. I’m sure I can avoid that but I’m super slow at this due to being a noob
@secretasianman my goal for the day is to extract something that the compiler will turn into a popcount instruction
@regehr it had one job