• 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.
Vector_impl.mlw 15 KB