diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 23 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 25 |
2 files changed, 42 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index cdd31fcb86..2474c784b8 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -336,20 +336,23 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info hint_info + .. insertprodn hint_info one_pattern .. prodn:: - hint_info ::= %| {? @natural } {? @one_term } + hint_info ::= %| {? @natural } {? @one_pattern } + one_pattern ::= @one_term Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of the class. - Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` - specifies the hint priority, where 0 is the highest priority as for + Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` + may be used to specify the hint priority, where 0 is the highest priority as for :tacn:`auto` hints. If the priority is not specified, the default is the number - of non-dependent binders of the instance. + of non-dependent binders of the instance. If :token:`one_pattern` is given, terms + matching that pattern will trigger use of the instance. Otherwise, + use is triggered based on the conclusion of the type. This command supports the :attr:`global` attribute that can be used on instances declared in a section so that their @@ -388,6 +391,16 @@ Summary of the commands equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. + .. flag:: Instance Generalized Output + + .. deprecated:: 8.13 + + Disabled by default, this provides compatibility with Coq + version 8.12 and earlier. + + When enabled, the type of the instance is implicitly generalized + over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``. + .. cmd:: Print Instances @reference Shows the list of instances associated with the typeclass :token:`reference`. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1fb337b30a..064107d088 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation: .. coqtop:: all Polymorphic Cumulative Record packType := {pk : Type}. + About packType. :g:`packType` binds a covariant universe, i.e. @@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j +Specifying cumulativity +~~~~~~~~~~~~~~~~~~~~~~~ + +The variance of the universe parameters for a cumulative inductive may be specified by the user. + +For the following type, universe ``a`` has its variance automatically +inferred (it is irrelevant), ``b`` is required to be irrelevant, +``c`` is covariant and ``d`` is invariant. With these annotations +``c`` and ``d`` have less general variances than would be inferred. + +.. coqtop:: all + + Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy. + About Dummy. + +Insufficiently restrictive variance annotations lead to errors: + +.. coqtop:: all + + Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}. + An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -280,7 +302,7 @@ An example of a proof using cumulativity End down. Cumulativity Weak Constraints ------------------------------ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. flag:: Cumulativity Weak Constraints @@ -383,6 +405,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names |