package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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
and proof = private {
  1. p_lhs : Ccalgo.ATerm.t;
  2. p_rhs : Ccalgo.ATerm.t;
  3. p_rule : rule;
}

Proof smart constructors

val prefl : Ccalgo.ATerm.t -> proof
val pcongr : proof -> proof -> proof
val ptrans : proof -> proof -> proof
val psym : proof -> proof
val pinject : proof -> Constr.pconstructor -> int -> int -> proof

Proof building functions

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

Main proof building function

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