Previous  Up  Next

Module Theory.Sym

module Sym: sig .. end

Dynamically typed morphisms

type pack = {
   ar : Constr.t;
   value : Constr.t;
   morph : Constr.t;
}

mimics the Coq record Sym.pack

val typ : Coq.lazy_ref
val mk_pack : Coq.Relation.t -> pack -> EConstr.constr

mk_pack rlt (ar,value,morph)

val null : Coq.Relation.t -> EConstr.constr

null builds a dummy (identity) symbol, given an Coq.Relation.t