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=0d402d92c1d3309dcb01fcbdb7f72c37

sha512=7a82041ef05b3edd0fbe2f63507a7ce7d910f6bf3f2a5d615b0c6f55986fd60ae2d5006983929d08a63a3a2c917801709aa4a47d2c1161a2d72d223081d341a9

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