package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz

sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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

Module `Sorts`Source

The sorts of CCI.

Sourcetype family =

| InSProp
| InProp
| InSet
| InType

Sourceval all_families : family list

Sourcetype t = private

| SProp
| Prop
| Set
| 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 sort_of_univ : Univ.Universe.t -> t

Sourceval levels : t -> Univ.Level.Set.t

Sourceval super : t -> t

Sourcetype relevance =

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

On This Page

The sorts of CCI.