Module Classify_cst

module Classify_cst: sig .. end

Classification of Constants

type res =

`\|`	`Ty of Libzipperposition.Ind_ty.t`
`\|`	`Cstor of Libzipperposition.Ind_ty.constructor * Libzipperposition.Ind_ty.t`
`\|`	`Inductive_cst of Ind_cst.cst option`
`\|`	`Projector of Libzipperposition.ID.t`	`(*`	projector of some constructor (id: type)	`*)`
`\|`	`DefinedCst of int`	`(*`	(recursive) definition of given stratification level	`*)`
`\|`	`Other`

val classify : Libzipperposition.ID.t -> res

classify id returns the role id plays in inductive reasoning

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

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