• 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
Name
Last commit
Last update
..
mach Loading commit data...
array.mlw Loading commit data...
hashtbl.mlw Loading commit data...
impset.mlw Loading commit data...
io.mlw Loading commit data...
matrix.mlw Loading commit data...
null.mlw Loading commit data...
pqueue.mlw Loading commit data...
queue.mlw Loading commit data...
random.mlw Loading commit data...
ref.mlw Loading commit data...
stack.mlw Loading commit data...
string.mlw Loading commit data...