Module Libzipperposition.Classify_cst

Classification of Constants

type res =
| Ty of Logtk.Ind_ty.t
| Cstor of Logtk.Ind_ty.constructor * Logtk.Ind_ty.t
| Inductive_cst of Ind_cst.t option
| Projector of Logtk.ID.t

projector of some constructor (id: type)

| DefinedCst of int * Logtk.Statement.definition

(recursive) definition of given stratification level + definition

| Parameter of int
| Skolem
| Other
val classify : Logtk.ID.t -> res

classify id returns the role id plays in inductive reasoning

val id_is_cstor : Logtk.ID.t -> bool
val id_is_projector : Logtk.ID.t -> bool
val id_is_defined : Logtk.ID.t -> bool
val pp_res : res CCFormat.printer
val pp_signature : Logtk.Signature.t CCFormat.printer

Print classification of signature

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

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

val weight_fun : Logtk.Precedence.weight_fun