package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.kernel/Sorts/index.html

Module SortsSource

The sorts of CCI.
Sourcetype family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
  5. | InQSort
Sourceval all_families : family list
Sourcemodule QVar : sig ... end
Sourcetype t = private
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
  5. | QSort of QVar.t * Univ.Universe.t
Sourceval sprop : t
Sourceval set : t
Sourceval prop : t
Sourceval type1 : t
Sourceval qsort : QVar.t -> Univ.Universe.t -> 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 sort_of_univ : Univ.Universe.t -> t
Sourceval levels : t -> Univ.Level.Set.t
Sourceval super : t -> t
Sourceval subst_instance_sort : Univ.Instance.t -> t -> t
Sourcetype relevance =
  1. | Relevant
  2. | Irrelevant
  3. | RelevanceVar of QVar.t

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
On This Page
  1. The sorts of CCI.