package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct