package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/cc_plugin/Cc_plugin/Ccproof/index.html

Module `Cc_plugin.Ccproof`Source

Sourcetype rule =

| Ax of Constr.constr
| SymAx of Constr.constr
| Refl of Ccalgo.term
| Trans of proof * proof
| Congr of proof * proof
| Inject of proof * Constr.pconstructor * int * int

Sourceand proof = private {

p_lhs : Ccalgo.term;
p_rhs : Ccalgo.term;
p_rule : rule;

}

Proof smart constructors

Sourceval prefl : Ccalgo.term -> proof

Sourceval pcongr : proof -> proof -> proof

Sourceval ptrans : proof -> proof -> proof

Sourceval psym : proof -> proof

Source

val pax : 
  (Ccalgo.term * Ccalgo.term) Cc_plugin.Ccalgo.Constrhash.t ->
  Cc_plugin.Ccalgo.Constrhash.key ->
  proof

Source

val psymax : 
  (Ccalgo.term * Ccalgo.term) Cc_plugin.Ccalgo.Constrhash.t ->
  Cc_plugin.Ccalgo.Constrhash.key ->
  proof

Sourceval pinject : proof -> Constr.pconstructor -> int -> int -> proof

Proof building functions

Source

val equal_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  int ->
  int ->
  proof

Source

val edge_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  ((int * int) * Ccalgo.equality) ->
  proof

Source

val path_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  int ->
  ((int * int) * Ccalgo.equality) list ->
  proof

Source

val congr_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  int ->
  int ->
  proof

Source

val ind_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  int ->
  Ccalgo.pa_constructor ->
  int ->
  Ccalgo.pa_constructor ->
  proof

Main proof building function

Source

val build_proof : 
  Environ.env ->
  Evd.evar_map ->
  Ccalgo.forest ->
  [ `Discr of int * Ccalgo.pa_constructor * int * Ccalgo.pa_constructor
  | `Prove of int * int ] ->
  proof

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cc_plugin/Cc_plugin/Ccproof/index.html

Module Cc_plugin.CcproofSource

Module `Cc_plugin.Ccproof`Source