package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

Coq proofs in a style that resembles non-mechanized mathematical proofs

Install

dune-project

Dependency

md5=6a1981f702a8d71b1407928e37ad9b95

sha512=149087397667a7dacaa8b6e9fa9552f829a8b807dd8a16ed0209b4ff82c3aeeb5f008d837a4cff1772debcb4929defd2588b53fa472c9d27d661e164404e98ac

Sourcemodule Backtracking : sig ... end

Sourcemodule Databases : sig ... end

Sourcemodule Exceptions : sig ... end

Sourcemodule G_waterproof : sig ... end

Sourcemodule Hint_dataset : sig ... end

Sourcemodule Hint_dataset_declarations : sig ... end

Sourcemodule Proofutils : sig ... end

Sourcemodule Waterprove : sig ... end

Sourcemodule Wp_auto : sig ... end

Sourcemodule Wp_bullets : sig ... end

This module registers two new bullet behaviors available for use in Waterproof. With

Sourcemodule Wp_eauto : sig ... end

Sourcemodule Wp_evars : sig ... end

Sourcemodule Wp_ffi : sig ... end

Sourcemodule Wp_rewrite : sig ... end