libzipperposition

Library for Zipperposition
IN THIS PACKAGE

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

Print classification of signature

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

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