Module Classify_cst

module Classify_cst: sig .. end

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