Module AAC_theory.Sym

module Sym: sig .. end

Dynamically typed morphisms

type pack = {

}

mimics the Coq record Sym.pack

val typ : Term.constr lazy_t

val mk_pack : AAC_coq.Relation.t -> pack -> Term.constr

mk_pack rlt (ar,value,morph)

val null : AAC_coq.Relation.t -> Term.constr

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