flâneur

Polymorphic Universes — Coq 8.18.0 documentation

coq.inria.fr · 5,247 words · saved by 1 readers

This section describes the universe polymorphic extension of Coq. Universe polymorphism makes it possible to write generic definitions making use of universes and reuse them at different and sometimes incompatible universe levels. A standard example of the difference between universe polymorphic and monomorphic definitions is given by the identity function: By default, constant declarations are monomorphic, hence the identity function declares a global universe (automatically named identity.u0) for its domain. Subsequently, if we try to self-apply the identity, we will get an error: Indeed, the global level identity.u0 would have to be strictly smaller than itself for this self-application to type check, as the type of (@identity) is forall (A : Type@{identity.u0}), A -> A whose type is itself Type@{identity.u0+1}. A universe polymorphic identity function binds its domain universe level at the definition level instead of making it global. It is then possible to reuse the constant at di

Polymorphic Universes - Coq 8.18.0 documentation >> Core language >> Polymorphic Universes Edit on GitHub \[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newc

saved by

related reading