package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/cc_plugin/Cc_plugin/Ccproof/index.html

Module Cc_plugin.CcproofSource

Sourcetype rule =
  1. | Ax of Constr.constr
  2. | SymAx of Constr.constr
  3. | Refl of Ccalgo.ATerm.t
  4. | Trans of proof * proof
  5. | Congr of proof * proof
  6. | Inject of proof * Constr.pconstructor * int * int
Sourceand proof = private {
  1. p_lhs : Ccalgo.ATerm.t;
  2. p_rhs : Ccalgo.ATerm.t;
  3. p_rule : rule;
}

Proof smart constructors

Sourceval pcongr : proof -> proof -> proof
Sourceval ptrans : proof -> proof -> proof
Sourceval psym : proof -> proof
Sourceval pax : (Ccalgo.ATerm.t * Ccalgo.ATerm.t) Cc_plugin.Ccalgo.Constrhash.t -> Cc_plugin.Ccalgo.Constrhash.key -> proof
Sourceval psymax : (Ccalgo.ATerm.t * Ccalgo.ATerm.t) Cc_plugin.Ccalgo.Constrhash.t -> Cc_plugin.Ccalgo.Constrhash.key -> proof
Sourceval pinject : proof -> Constr.pconstructor -> int -> int -> proof

Proof building functions

Sourceval equal_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> int -> proof
Sourceval edge_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> ((int * int) * Ccalgo.equality) -> proof
Sourceval path_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> ((int * int) * Ccalgo.equality) list -> proof
Sourceval congr_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> int -> proof

Main proof building function

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