Module Libzipperposition.Classify_cstSource

Classification of Constants

Sourcetype res =
  1. | Ty of Logtk.Ind_ty.t
  2. | Cstor of Logtk.Ind_ty.constructor * Logtk.Ind_ty.t
  3. | Inductive_cst of Ind_cst.t option
  4. | Projector of Logtk.ID.t
    (*

    projector of some constructor (id: type)

    *)
  5. | DefinedCst of int * Logtk.Statement.definition
    (*

    (recursive) definition of given stratification level + definition

    *)
  6. | Parameter of int
  7. | Skolem
  8. | Other
Sourceval classify : Logtk.ID.t -> res

classify id returns the role id plays in inductive reasoning

Sourceval id_is_cstor : Logtk.ID.t -> bool
Sourceval id_is_projector : Logtk.ID.t -> bool
Sourceval id_is_defined : Logtk.ID.t -> bool

Print classification of signature

Sourceval prec_constr : [ `partial ] Logtk.Precedence.Constr.t

Partial order on ID.t, with: regular > constant > sub_constant > cstor