package coq

  1. Overview
  2. Docs
On This Page
  1. The sorts of CCI.
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module SortsSource

The sorts of CCI.
Sourcetype family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
Sourceval all_families : family list
Sourcetype t = private
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
Sourceval sprop : t
Sourceval set : t
Sourceval prop : t
Sourceval type1 : t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
Sourceval is_sprop : t -> bool
Sourceval is_set : t -> bool
Sourceval is_prop : t -> bool
Sourceval is_small : t -> bool
Sourceval family : t -> family
Sourceval hcons : t -> t
Sourceval family_compare : family -> family -> int
Sourceval family_equal : family -> family -> bool
Sourceval family_leq : family -> family -> bool
Sourceval univ_of_sort : t -> Univ.Universe.t
Sourceval sort_of_univ : Univ.Universe.t -> t
Sourceval super : t -> t
Sourcetype relevance =
  1. | Relevant
  2. | Irrelevant

On binders: is this variable proof relevant

Sourceval relevance_hash : relevance -> int
Sourceval relevance_equal : relevance -> relevance -> bool
Sourceval relevance_of_sort : t -> relevance
Sourceval relevance_of_sort_family : family -> relevance
Sourceval debug_print : t -> Pp.t
Sourceval pr_sort_family : family -> Pp.t
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