The file redblack.v contains a formalization of red-black trees in the Coq proof assistant by Andrew W. Appel. The formalization is available under the open source BSD-3-Clause license.
The file redblack.v contains a formalization of red-black trees in the Coq proof assistant by Andrew W. Appel. The formalization is available under the open source BSD-3-Clause license.