Siddharth
Siddharth
@alexkeizer @ineol @luisacicolini , I would appreciate it if you could try this again. Please run ``` cd lean-mlir/bv-evaluation;./toplevel-hackersdelight.sh ```
> It seems the mathlib cache is download twice for me: > > ``` > Using cache from origin: leanprover-community/mathlib4-nightly-testing > Attempting to download 7045 file(s) from leanprover-community/mathlib4 cache >...
@tobiasgrosser I have an LGTM from Alex, so I propose to merge this.
After working on this more, I come to the conclusion that I need to be able to manipulate a different encoding of automata, where the next state is not necessarily...
awaiting-review
Also, note that `popcount` is uniquely defined by three equations: ``` popCount (x ++ y) = popCount x + popCount y popCount (x#0) = 0 popCount (BitVec.ofBool b) = b.toNat...