Module Cc_plugin.CcproofSource

Sourcetype rule =
  1. | Ax of Ccalgo.axiom
    (*

    if ⊢ t = u :: A, then ⊢ t = u :: A

    *)
  2. | SymAx of Ccalgo.axiom
    (*

    if ⊢ t = u : A, then ⊢ u = t :: A

    *)
  3. | Refl of Ccalgo.ATerm.t
  4. | Trans of proof * proof
    (*

    ⊢ t = u :: A -> ⊢ u = v :: A -> ⊢ t = v :: A

    *)
  5. | Congr of proof * proof
    (*

    ⊢ f = g :: forall x : A, B -> ⊢ t = u :: A -> f t = g u :: B

    Assumes that B

    ≡ Bu for this to make sense!

    *)
  6. | Inject of proof * Constr.pconstructor * int * int
    (*

    ⊢ ci v = ci w :: Ind(args) -> ⊢ v = w :: T where T is the type of the n-th argument of ci, assuming they coincide

    *)
Sourceand proof = private {
  1. p_lhs : Ccalgo.ATerm.t;
  2. p_rhs : Ccalgo.ATerm.t;
  3. p_rule : rule;
}

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