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=7cfe30aceb61e154ed905e048bdf2cb7

sha512=006bf05727d2aa21cebe332ff5a027fdd8843c574753fd5b8d0486e4df7bd447a4f538c3c92736011734c29c601d3a77c2f1a1ee5b3645a7666766ed32907777

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 Unfold_framework : sig ... end

In this module we keep two tables:

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