• Clément Fumex's avatar
    Coq realization of bv theory: · 1a0d9e4a
    Clément Fumex authored
    - generation in the makefile
    - proofs done
    Remove complex axioms from Pow2int in bv.why.
    Add guards in rotates axioms in bv.why.
    1a0d9e4a
hackers-delight.mlw 11.2 KB