package libzipperposition

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Classification of Constants

type 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
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