• Mário Pereira's avatar
    Why3 "bootstrap": · 0da5f41e
    Mário Pereira authored
    The code in file /src/util/pqueue.ml has been extracted from a Why3 proof,
    and is now a correct-by-construction OCaml code. This file depends on the Vector
    module, which is also an OCaml implementation extracted from another Why3 proof.
    The proofs can be found in /examples/util/
    
    This is the result of Aymeric Walch bachelor internship.
    0da5f41e
Name
Last commit
Last update
..
PQueue_impl Loading commit data...
Vector_impl Loading commit data...
PQueue.mli Loading commit data...
PQueue_impl.mlw Loading commit data...
Vector.mli Loading commit data...
Vector.mli.equiv Loading commit data...
Vector_impl.mlw Loading commit data...
vocal.mlw Loading commit data...