diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 37 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 36 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 93 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 44 |
14 files changed, 173 insertions, 198 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3af3115a59..3e414a714c 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _canonicalstructures: Canonical Structures @@ -75,7 +74,7 @@ We amend that by equipping ``nat`` with a comparison relation. Check 3 == 3. Eval compute in 3 == 4. -This last test shows that |Coq| is now not only able to typecheck ``3 == 3``, +This last test shows that |Coq| is now not only able to type check ``3 == 3``, but also that the infix relation was bound to the ``nat_eq`` relation. This relation is selected whenever ``==`` is used on terms of type nat. This can be read in the line declaring the canonical structure diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index f7fd4b9146..cb267576b2 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -1,15 +1,13 @@ -.. include:: ../replaces.rst - .. _extendedpatternmatching: -Extended pattern-matching +Extended pattern matching ========================= :Authors: Cristina Cornes and Hugo Herbelin .. TODO links to figures -This section describes the full form of pattern-matching in |Coq| terms. +This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -38,7 +36,7 @@ same values as ``pattern`` does and ``identifier`` is bound to the matched value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only -occur at the root of pattern-matching equations. Disjunctions of +occur at the root of pattern matching equations. Disjunctions of *multiple patterns* are allowed though. Since extended ``match`` expressions are compiled into the primitive ones, @@ -46,7 +44,7 @@ the expressiveness of the theory remains the same. Once parsing has finished only simple patterns remain. The original nesting of the ``match`` expressions is recovered at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing -(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print` +(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print` if the term is a constant, or using the command :cmd:`Check`. The extended ``match`` still accepts an optional *elimination predicate* @@ -88,7 +86,7 @@ Using multiple patterns in the definition of ``max`` lets us write: which will be compiled into the previous form. -The pattern-matching compilation strategy examines patterns from left +The pattern matching compilation strategy examines patterns from left to right. A match expression is generated **only** when there is at least one constructor in the column of patterns. E.g. the following example does not build a match expression. @@ -262,9 +260,9 @@ When we use parameters in patterns there is an error message: | cons A _ l' => l' end). -.. opt:: Asymmetric Patterns +.. flag:: Asymmetric Patterns -This option (off by default) removes parameters from constructors in patterns: + This flag (off by default) removes parameters from constructors in patterns: .. coqtop:: all @@ -407,12 +405,11 @@ length, by writing .. coqtop:: in - Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. @@ -598,7 +595,7 @@ situation: incorrect (because constructors are not applied to the correct number of the arguments, because they are not linear or they are wrongly typed). -.. exn:: Non exhaustive pattern-matching. +.. exn:: Non exhaustive pattern matching. The pattern matching is not exhaustive. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 8c1eacf085..3d58f522dd 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extraction: Extraction of programs in |OCaml| and Haskell @@ -131,14 +129,14 @@ order to produce more readable code. The type-preserving optimizations are controlled by the following |Coq| options: -.. opt:: Extraction Optimize +.. flag:: Extraction Optimize Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this option off if you want a ML term as close as possible to the Coq term. -.. opt:: Extraction Conservative Types +.. flag:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -146,7 +144,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. -.. opt:: Extraction KeepSingleton +.. flag:: Extraction KeepSingleton Default is off. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -155,7 +153,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: The typical example is ``sig``. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -.. opt:: Extraction AutoInline +.. flag:: Extraction AutoInline Default is on. The extraction mechanism inlines the bodies of some defined constants, according to some heuristics @@ -227,7 +225,7 @@ When an actual extraction takes place, an error is normally raised if the if any of the implicit arguments still occurs in the final code. This behavior can be relaxed via the following option: -.. opt:: Extraction SafeImplicits +.. flag:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted instead of an error if some implicit arguments still occur in the @@ -319,15 +317,15 @@ native boolean type instead of the |Coq| one. The syntax is the following: extractions for the type itself (first `string`) and all its constructors (all the `string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native - pattern-matching of the language will be used. + pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra `string` that indicates how to - perform pattern-matching over this inductive type. In this form, + perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. For an inductive type with `k` constructors, the function used to - emulate the pattern-matching should expect `(k+1)` arguments, first the `k` + emulate the pattern matching should expect `(k+1)` arguments, first the `k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no @@ -344,7 +342,7 @@ native boolean type instead of the |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an - ad-hoc pattern-matching) will often **not** be fully rigorously + ad-hoc pattern matching) will often **not** be fully rigorously correct. For instance, when extracting ``nat`` to |OCaml| ``int``, it is theoretically possible to build ``nat`` values that are larger than |OCaml| ``max_int``. It is the user's responsibility to @@ -423,7 +421,7 @@ a generic type ``'a`` to any term. First, if some part of the program is *very* polymorphic, there may be no ML type for it. In that case the extraction to ML works alright but the generated code may be refused by the ML -type-checker. A very well known example is the ``distr-pair`` +type checker. A very well known example is the ``distr-pair`` function: .. coqtop:: in @@ -458,7 +456,7 @@ In |OCaml|, we must cast any argument of the constructor dummy Even with those unsafe castings, you should never get error like ``segmentation fault``. In fact even if your program may seem -ill-typed to the |OCaml| type-checker, it can't go wrong : it comes +ill-typed to the |OCaml| type checker, it can't go wrong : it comes from a Coq well-typed terms, so for example inductive types will always have the correct number of arguments, etc. Of course, when launching manually some extracted function, you should apply it to arguments @@ -469,7 +467,7 @@ found in :cite:`Let02`. We have to say, though, that in most "realistic" programs, these problems do not occur. For example all the programs of Coq library are accepted by the |OCaml| -type-checker without any ``Obj.magic`` (see examples below). +type checker without any ``Obj.magic`` (see examples below). Some examples ------------- diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index c7df250672..403b163196 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _generalizedrewriting: Generalized rewriting @@ -22,18 +19,18 @@ The new implementation is a drop-in replacement for the old one [#tabareau]_, hence most of the documentation still applies. The work is a complete rewrite of the previous implementation, based -on the type class infrastructure. It also improves on and generalizes +on the typeclass infrastructure. It also improves on and generalizes the previous implementation in several ways: + User-extensible algorithm. The algorithm is separated into two parts: generation of the rewriting constraints (written in ML) and solving - these constraints using type class resolution. As type class + these constraints using typeclass resolution. As typeclass resolution is extensible using tactics, this allows users to define general ways to solve morphism constraints. + Subrelations. An example extension to the base algorithm is the ability to define one relation as a subrelation of another so that morphism declarations on one relation can be used automatically for - the other. This is done purely using tactics and type class search. + the other. This is done purely using tactics and typeclass search. + Rewriting under binders. It is possible to rewrite under binders in the new implementation, if one provides the proper morphisms. Again, most of the work is handled in the tactics. @@ -126,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. coqtop:: in - forall (A : Type) (S1 S1’ S2 S2’ : list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` for all ``A``. @@ -226,7 +223,7 @@ following command. This command declares ``f`` as a parametric morphism of signature ``sig``. The identifier :token:`ident` gives a unique name to the morphism and it is used as - the base name of the type class instance definition and as the name of + the base name of the typeclass instance definition and as the name of the lemma that proves the well-definedness of the morphism. The parameters of the morphism as well as the signature may refer to the context of variables. The command asks the user to prove interactively @@ -309,7 +306,7 @@ following command. Proof. intros. rewrite empty_neutral. reflexivity. Qed. - The tables of relations and morphisms are managed by the type class + The tables of relations and morphisms are managed by the typeclass instance mechanism. The behavior on section close is to generalize the instances by the variables of the section (and possibly hypotheses used in the proofs of instance declarations) but not to export them in @@ -350,7 +347,7 @@ prove that the argument of the morphism is defined. .. example:: Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the - smallest PER over non zero elements). Division can be declared as a + smallest PER over nonzero elements). Division can be declared as a morphism of signature ``eq ==> eq0 ==> eq``. Replacing ``x`` with ``y`` in ``div x n = div y n`` opens an additional goal ``eq0 n n`` which is equivalent to ``n = n /\ n <> 0``. @@ -446,12 +443,12 @@ First class setoids and morphisms The implementation is based on a first-class representation of -properties of relations and morphisms as type classes. That is, the +properties of relations and morphisms as typeclasses. That is, the various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: -.. coqtop:: in +.. coqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -462,7 +459,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqtop:: in +.. coqdoc:: Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] @@ -472,9 +469,9 @@ is equivalent to an instance declaration: The declaration itself amounts to the definition of an object of the record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added to the ``typeclass_instances`` hint database. Morphism declarations are -also instances of a type class defined in ``Classes.Morphisms``. See the -documentation on type classes :ref:`typeclasses` -and the theories files in Classes for further explanations. +also instances of a typeclass defined in ``Classes.Morphisms``. See the +documentation on :ref:`typeclasses` and the theories files in Classes +for further explanations. One can inform the rewrite tactic about morphisms and relations just by using the typeclass mechanism to declare them using Instance and @@ -703,7 +700,7 @@ example of a mostly user-space extension of the algorithm. Constant unfolding ~~~~~~~~~~~~~~~~~~ -The resolution tactic is based on type classes and hence regards user- +The resolution tactic is based on typeclasses and hence regards user- defined constants as transparent by default. This may slow down the resolution due to a lot of unifications (all the declared ``Proper`` instances are tried at each node of the search tree). To speed it up, diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index f134022eb6..fc5a366caf 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _implicitcoercions: Implicit Coercions @@ -256,19 +254,16 @@ Displaying Available Coercions Activating the Printing of Coercions ------------------------------------- -.. opt:: Printing Coercions +.. flag:: Printing Coercions When on, this option forces all the coercions to be printed. By default, coercions are not printed. -.. cmd:: Add Printing Coercion @qualid - - This command forces coercion denoted by :n:`@qualid` to be printed. - By default, a coercion is never printed. - -.. cmd:: Remove Printing Coercion @qualid +.. table:: Printing Coercion @qualid + :name: Printing Coercion - Use this command, to skip the printing of coercion :n:`@qualid`. + Specifies a set of qualids for which coercions are always displayed. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. .. _coercions-classes-as-records: @@ -315,7 +310,7 @@ are also forgotten. Coercions and Modules --------------------- -.. opt:: Automatic Coercions Import +.. flag:: Automatic Coercions Import Since |Coq| version 8.3, the coercions present in a module are activated only when the module is explicitly imported. Formerly, the coercions @@ -325,6 +320,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- @@ -352,7 +353,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behaviour of + Note that ``Check true=O`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d03a31c044..3b9760f586 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -112,11 +112,11 @@ and checked to be :math:`-1`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` -tactics. Roughly speaking, the deductive power of lia is the combined deductive -power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear -goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following -so-called *omega nightmare* :cite:`TheOmegaPaper`. + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and -:tacn:`romega` is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 0f2d35d044..2cde65dcdc 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _miscellaneousextensions: Miscellaneous extensions diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 9adeca46fc..e7a8c238ac 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,5 +1,3 @@ -.. include:: ../preamble.rst - .. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1ed3bffd2c..03d4f148e3 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -11,7 +11,7 @@ Description of ``omega`` .. tacn:: omega :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequations over the + i.e. for proving formulas made of equations and inequalities over the type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. Formulas on ``nat`` are automatically injected into ``Z``. The procedure may use any hypothesis of the current proof session to solve the goal. @@ -23,11 +23,6 @@ Description of ``omega`` If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -.. tacv:: romega - :name: romega - - To be documented. - Arithmetical goals recognized by ``omega`` ------------------------------------------ @@ -114,23 +109,23 @@ loaded by Options ------- -.. opt:: Stable Omega +.. flag:: Stable Omega .. deprecated:: 8.5 This deprecated option (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. -.. opt:: Omega UseLocalDefs +.. flag:: Omega UseLocalDefs This option (on by default) allows :tacn:`omega` to use the bodies of local variables. -.. opt:: Omega System +.. flag:: Omega System This option (off by default) activate the printing of debug information -.. opt:: Omega Action +.. flag:: Omega Action This option (off by default) activate the printing of debug information @@ -140,12 +135,12 @@ Technical data Overview of the tactic ~~~~~~~~~~~~~~~~~~~~~~ - * The goal is negated twice and the first negation is introduced as an hypothesis. - * Hypotheses are decomposed in simple equations or inequations. Multiple + * The goal is negated twice and the first negation is introduced as a hypothesis. + * Hypotheses are decomposed in simple equations or inequalities. Multiple goals may result from this phase. - * Equations and inequations over ``nat`` are translated over + * Equations and inequalities over ``nat`` are translated over ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequations are normalized. + * Equations and inequalities are normalized. * Goals are solved by the OMEGA decision procedure. * The script of the solution is replayed. @@ -156,17 +151,17 @@ The OMEGA decision procedure involved in the :tacn:`omega` tactic uses a small subset of the decision procedure presented in :cite:`TheOmegaPaper` Here is an overview, refer to the original paper for more information. - * Equations and inequations are normalized by division by the GCD of their + * Equations and inequalities are normalized by division by the GCD of their coefficients. * Equations are eliminated, using the Banerjee test to get a coefficient equal to one. - * Note that each inequation cuts the Euclidean space in half. - * Inequations are solved by projecting on the hyperspace + * Note that each inequality cuts the Euclidean space in half. + * Inequalities are solved by projecting on the hyperspace defined by cancelling one of the variables. They are partitioned according to the sign of the coefficient of the eliminated - variable. Pairs of inequations from different classes define a + variable. Pairs of inequalities from different classes define a new edge in the projection. - * Redundant inequations are eliminated or merged in new + * Redundant inequalities are eliminated or merged in new equations that can be eliminated by the Banerjee test. * The last two steps are iterated until a contradiction is reached (success) or there is no more variable to eliminate (failure). diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8ee8f52227..8b7214e2ab 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _asynchronousandparallelproofprocessing: Asynchronous and Parallel Proof Processing @@ -60,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 28fe68d78d..fad45995d2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: @@ -18,7 +15,7 @@ program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole |Coq| proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of -PVS :cite:`Rushby98`, which generates type-checking conditions while typing a +PVS :cite:`Rushby98`, which generates type checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a complete |Coq| term. |Program| replaces the |Program| tactic by Catherine @@ -45,7 +42,7 @@ be considered as an object of type :g:`{x : T | P}` for any well-formed will generate an obligation for every such coercion. In the other direction, Russell will automatically insert a projection. -Another distinction is the treatment of pattern-matching. Apart from +Another distinction is the treatment of pattern matching. Apart from the following differences, it is equivalent to the standard match operation (see :ref:`extendedpatternmatching`). @@ -72,8 +69,8 @@ operation (see :ref:`extendedpatternmatching`). This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. -+ Generation of inequalities. If a pattern intersects with a previous - one, an inequality is added in the context of the second branch. See ++ Generation of disequalities. If a pattern intersects with a previous + one, a disequality is added in the context of the second branch. See for example the definition of div2 below, where the second branch is typed in a context where :g:`∀ p, _ <> S (S p)`. + Coercion. If the object being matched is coercible to an inductive @@ -84,15 +81,15 @@ operation (see :ref:`extendedpatternmatching`). There are options to control the generation of equalities and coercions. -.. opt:: Program Cases +.. flag:: Program Cases - This controls the special treatment of pattern-matching generating equalities - and inequalities when using |Program| (it is on by default). All + This controls the special treatment of pattern matching generating equalities + and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. -.. opt:: Program Generalized Coercion +.. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| (the option is on by default). Coercion of subset types and pairs is still @@ -104,8 +101,8 @@ Syntactic control over equalities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To give more control over the generation of equalities, the -typechecker will fall back directly to |Coq|’s usual typing of dependent -pattern-matching if a return or in clause is specified. Likewise, the +type checker will fall back directly to |Coq|’s usual typing of dependent +pattern matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -175,7 +172,7 @@ Program Definition .. TODO refer to production in alias -See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` +.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: @@ -213,7 +210,7 @@ with mutually recursive definitions too. end. Here we have one obligation for each branch (branches for :g:`0` and -``(S 0)`` are automatically generated by the pattern-matching +``(S 0)`` are automatically generated by the pattern matching compilation algorithm). .. coqtop:: all @@ -320,19 +317,19 @@ optional tactic is replaced by the default one if not specified. Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. -.. opt:: Transparent Obligations +.. flag:: Transparent Obligations Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. -.. opt:: Hide Obligations +.. flag:: Hide Obligations Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. -.. opt:: Shrink Obligations +.. flag:: Shrink Obligations *Deprecated since 8.7* @@ -378,6 +375,3 @@ Frequently Asked Questions using lazy evaluation; #. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible. - -.. bibliography:: ../biblio.bib - :keyprefix: p- diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index d5c33dc1d4..58617916c0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,11 +1,9 @@ -.. include:: ../replaces.rst .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` - .. _theringandfieldtacticfamilies: The ring and field tactic families @@ -19,7 +17,7 @@ field equations. What does this tactic do? ------------------------------ -``ring`` does associative-commutative rewriting in ring and semi-ring +``ring`` does associative-commutative rewriting in ring and semiring structures. Assume you have two binary functions :math:`\oplus` and :math:`\otimes` that are associative and commutative, with :math:`\oplus` distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for @@ -37,7 +35,7 @@ order. It is an easy theorem to show that every polynomial is equivalent (modulo the ring properties) to exactly one canonical sum. This canonical sum is called the normal form of the polynomial. In fact, the actual representation shares monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over -any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring +any ring or semiring structure. The basic use of ``ring`` is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity. @@ -103,7 +101,7 @@ Concrete usage in Coq .. tacn:: ring The ``ring`` tactic solves equations upon polynomial expressions of a ring -(or semi-ring) structure. It proceeds by normalizing both sides +(or semiring) structure. It proceeds by normalizing both sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation, rewriting of monomials) and comparing syntactically the results. @@ -264,13 +262,13 @@ are the implementations of the ring operations, ``==`` is the equality of the coefficients, ``?+!`` is an implementation of this equality, and ``[x]`` is a notation for the image of ``x`` by the ring morphism. -Since |Z| is an initial ring (and |N| is an initial semi-ring), it can +Since |Z| is an initial ring (and |N| is an initial semiring), it can always be considered as a set of coefficients. There are basically three kinds of (semi-)rings: abstract rings to be used when operations are not effective. The set - of coefficients is |Z| (or |N| for semi-rings). + of coefficients is |Z| (or |N| for semirings). computational rings to be used when operations are effective. The @@ -505,10 +503,10 @@ expression `F` to a common denominator :math:`N/D = 0` where `N` and `D` are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve :math:`N = 0`. -Note that ``field`` also generates non-zero conditions for all the +Note that ``field`` also generates nonzero conditions for all the denominators it encounters in the reduction. In our example, it generates the condition :math:`x \neq 0`. These conditions appear as one subgoal -which is a conjunction if there are several denominators. Non-zero +which is a conjunction if there are several denominators. Nonzero conditions are always polynomial expressions. For example when reducing the expression :math:`1/(1 + 1/x)`, two side conditions are generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since @@ -616,7 +614,7 @@ carrier set, an equality, and field operations: satisfies the field axioms. Semi-fields (fields without + inverse) are also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of -fields and semi-fields is: +fields and semifields is: .. coqtop:: in @@ -670,7 +668,7 @@ specific modifier: completeness :n:`@term` allows the field tactic to prove automatically - that the image of non-zero coefficients are mapped to non-zero + that the image of nonzero coefficients are mapped to nonzero elements of the field. :n:`@term` is a proof of ``forall x y, [x] == [y] -> x ?=! y = true``, @@ -684,7 +682,7 @@ History of ring First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big -for |Coq|’s type-checker. Let us see why: +for |Coq|’s type checker. Let us see why: .. coqtop:: all @@ -707,7 +705,7 @@ interleaving of computation and reasoning (see :ref:`discussion_reflection`). He some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. Proofs terms generated by ring are quite small, they are linear in the -number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking +number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking those terms requires some time because it makes a large use of the conversion rule, but memory requirements are much smaller. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b7946c6451..369dae0ead 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,12 +1,10 @@ -.. include:: ../replaces.rst - .. _typeclasses: Type Classes ============ This chapter presents a quick reference of the commands related to type -classes. For an actual introduction to type classes, there is a +classes. For an actual introduction to typeclasses, there is a description of the system :cite:`sozeau08` and the literature on type classes in Haskell which also applies. @@ -76,7 +74,7 @@ for dealing with obligations. Binding classes --------------- -Once a type class is declared, one can use it in class binders: +Once a typeclass is declared, one can use it in class binders: .. coqtop:: all @@ -92,7 +90,7 @@ found, an error is raised: Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). -The algorithm used to solve constraints is a variant of the eauto +The algorithm used to solve constraints is a variant of the :tacn:`eauto` tactic that does proof search with a set of lemmas (the instances). It will use local hypotheses as well as declared lemmas in the ``typeclass_instances`` database. Hence the example can also be @@ -103,13 +101,13 @@ written: Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). However, the generalizing binders should be used instead as they have -particular support for type classes: +particular support for typeclasses: -+ They automatically set the maximally implicit status for type class ++ They automatically set the maximally implicit status for typeclass arguments, making derived functions as easy to use as class methods. In the example above, ``A`` and ``eqa`` should be set maximally implicit. + They support implicit quantification on partially applied type - classes (:ref:`implicit-generalization`). Any argument not given as part of a type class + classes (:ref:`implicit-generalization`). Any argument not given as part of a typeclass binder will be automatically generalized. + They also support implicit quantification on :ref:`superclasses`. @@ -148,7 +146,7 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we provide a new +To ease the parametrization of developments by typeclasses, we provide a new way to introduce variables into section contexts, compatible with the implicit argument mechanism. The new command works similarly to the :cmd:`Variables` vernacular, except it accepts any binding context as argument. For example: @@ -271,7 +269,7 @@ Summary of the commands .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } - The :cmd:`Class` command is used to declare a type class with parameters + The :cmd:`Class` command is used to declare a typeclass with parameters ``binders`` and fields the declared record fields. Variants: @@ -302,7 +300,7 @@ Variants: .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } -The :cmd:`Instance` command is used to declare a type class instance named +The :cmd:`Instance` command is used to declare a typeclass instance named ``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and fields ``b1`` to ``bi``, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode. @@ -310,7 +308,7 @@ the class. Missing fields must be filled in interactive proof mode. An arbitrary context of ``binders`` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for -auto hints. If the priority is not specified, it defaults to the number +:tacn:`auto` hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term @@ -329,7 +327,7 @@ of non-dependent binders of the instance. .. cmdv:: Program Instance :name: Program Instance - Switches the type-checking to Program (chapter :ref:`programs`) and + Switches the type checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. .. cmdv:: Declare Instance @@ -342,12 +340,12 @@ of non-dependent binders of the instance. Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a -few other commands related to type classes. +few other commands related to typeclasses. .. cmd:: Existing Instance {+ @ident} [| priority] This command adds an arbitrary list of constants whose type ends with - an applied type class to the instance database with an optional + an applied typeclass to the instance database with an optional priority. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it @@ -367,11 +365,11 @@ few other commands related to type classes. + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is available among dependent subgoals, and shelving goals is supported. - typeclasses eauto is a multi-goal tactic. It analyses the dependencies + ``typeclasses eauto`` is a multi-goal tactic. It analyses the dependencies between subgoals to avoid backtracking on subgoals that are entirely independent. - + When called with no arguments, typeclasses eauto uses + + When called with no arguments, ``typeclasses eauto`` uses the ``typeclass_instances`` database by default (instead of core). Dependent subgoals are automatically shelved, and shelved goals can remain after resolution ends (following the behavior of Coq 8.5). @@ -379,13 +377,13 @@ few other commands related to type classes. .. note:: As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully mimicks what happens during typeclass resolution when it is called - during refinement/type-inference, except that *only* declared class + during refinement/type inference, except that *only* declared class subgoals are considered at the start of resolution during type inference, while ``all`` can select non-class subgoals as well. It might move to ``all:typeclasses eauto`` in future versions when the refinement engine will be able to backtrack. - + When called with specific databases (e.g. with), typeclasses eauto + + When called with specific databases (e.g. with), ``typeclasses eauto`` allows shelved goals to remain at any point during search and treat typeclass goals like any other. @@ -403,10 +401,10 @@ few other commands related to type classes. .. warning:: The semantics for the limit :n:`@num` - is different than for auto. By default, if no limit is given the - search is unbounded. Contrary to auto, introduction steps (intro) are + is different than for auto. By default, if no limit is given, the + search is unbounded. Contrary to :tacn:`auto`, introduction steps are counted, which might result in larger limits being necessary when - searching with typeclasses eauto than auto. + searching with ``typeclasses eauto`` than with :tacn:`auto`. .. cmdv:: typeclasses eauto with {+ @ident} @@ -417,11 +415,11 @@ few other commands related to type classes. .. tacn:: autoapply @term with @ident :name: autoapply - The tactic autoapply applies a term using the transparency information + The tactic ``autoapply`` applies a term using the transparency information of the hint database ident, and does *no* typeclass resolution. This can be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint database ``typeclass_instances``) to allow backtracking on the typeclass - subgoals created by the lemma application, rather than doing type class + subgoals created by the lemma application, rather than doing typeclass resolution locally at the hint application time. .. _TypeclassesTransparent: @@ -431,7 +429,7 @@ Typeclasses Transparent, Typclasses Opaque .. cmd:: Typeclasses Transparent {+ @ident} - This command defines makes the identifiers transparent during type class + This command makes the identifiers transparent during typeclass resolution. .. cmd:: Typeclasses Opaque {+ @ident} @@ -458,7 +456,7 @@ This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. Options ~~~~~~~ -.. opt:: Typeclasses Dependency Order +.. flag:: Typeclasses Dependency Order This option (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend @@ -467,7 +465,7 @@ Options quite different performance behaviors of proof search. -.. opt:: Typeclasses Filtered Unification +.. flag:: Typeclasses Filtered Unification This option, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a @@ -481,27 +479,29 @@ Options where there is a hole in that place. -.. opt:: Typeclasses Limit Intros +.. flag:: Typeclasses Limit Intros This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction. - *Warning:* this can be expensive as it requires rebuilding hint - clauses dynamically, and does not benefit from the invertibility - status of the product introduction rule, resulting in potentially more - expensive proof-search (i.e. more useless backtracking). + .. warning:: + + This can be expensive as it requires rebuilding hint + clauses dynamically, and does not benefit from the invertibility + status of the product introduction rule, resulting in potentially more + expensive proof-search (i.e. more useless backtracking). -.. opt:: Typeclass Resolution For Conversion +.. flag:: Typeclass Resolution For Conversion This option (on by default) controls the use of typeclass resolution - when a unification problem cannot be solved during elaboration/type- + when a unification problem cannot be solved during elaboration/type inference. With this option on, when a unification fails, typeclass resolution is tried before launching unification once again. -.. opt:: Typeclasses Strict Resolution +.. flag:: Typeclasses Strict Resolution Typeclass declarations introduced when this option is set have a stricter resolution behavior (the option is off by default). When @@ -511,28 +511,33 @@ Options instantiated. -.. opt:: Typeclasses Unique Solutions +.. flag:: Typeclasses Unique Solutions When a typeclass resolution is launched we ensure that it has a single solution or fail. This ensures that the resolution is canonical, but can make proof search much more expensive. -.. opt:: Typeclasses Unique Instances +.. flag:: Typeclasses Unique Instances Typeclass declarations introduced when this option is set have a more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -.. opt:: Typeclasses Debug {? Verbosity @num} +.. flag:: Typeclasses Debug + + Controls whether typeclass resolution steps are shown during search. Setting this flag + also sets :opt:`Typeclasses Debug Verbosity` to 1. + +.. opt:: Typeclasses Debug Verbosity @num + :name: Typeclasses Debug Verbosity - These options allow to see the resolution steps of typeclasses that are - performed during search. The ``Debug`` option is synonymous to ``Debug - Verbosity 1``, and ``Debug Verbosity 2`` provides more information - (tried tactics, shelving of goals, etc…). + Determines how much information is shown for typeclass resolution steps during search. + 1 is the default level. 2 shows additional information such as tried tactics and shelving + of goals. Setting this option also sets :flag:`Typeclasses Debug`. -.. opt:: Refine Instance Mode +.. flag:: Refine Instance Mode This option allows to switch the behavior of instance declarations made through the Instance command. @@ -548,7 +553,7 @@ Typeclasses eauto `:=` .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth - This command allows more global customization of the type class + This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index f245fab5ca..41afe3c312 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _polymorphicuniverses: Polymorphic Universes @@ -36,7 +34,7 @@ error: Fail Definition selfid := identity (@identity). Indeed, the global level ``Top.1`` would have to be strictly smaller than -itself for this self-application to typecheck, as the type of +itself for this self-application to type check, as the type of :g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself :g:`Type@{Top.1+1}`. @@ -59,7 +57,7 @@ so: Definition selfpid := pidentity (@pidentity). Of course, the two instances of :g:`pidentity` in this definition are -different. This can be seen when the :opt:`Printing Universes` option is on: +different. This can be seen when the :flag:`Printing Universes` flag is on: .. coqtop:: none @@ -79,7 +77,7 @@ levels. When printing :g:`pidentity`, we can see the universes it binds in the annotation :g:`@{Top.2}`. Additionally, when -:opt:`Printing Universes` is on we print the "universe context" of +:flag:`Printing Universes` is on we print the "universe context" of :g:`pidentity` consisting of the bound universes and the constraints they must verify (for :g:`pidentity` there are no constraints). @@ -129,14 +127,14 @@ Polymorphic, Monomorphic As shown in the examples, polymorphic definitions and inductives can be declared using the ``Polymorphic`` prefix. -.. opt:: Universe Polymorphism +.. flag:: Universe Polymorphism Once enabled, this option will implicitly prepend ``Polymorphic`` to any definition of the user. .. cmd:: Monomorphic @definition - When the :opt:`Universe Polymorphism` option is set, to make a definition + When the :flag:`Universe Polymorphism` option is set, to make a definition producing global universe constraints, one can use the ``Monomorphic`` prefix. Many other commands support the ``Polymorphic`` flag, including: @@ -169,7 +167,7 @@ declared cumulative using the :g:`Cumulative` prefix. Declares the inductive as cumulative -Alternatively, there is an option :opt:`Polymorphic Inductive +Alternatively, there is a flag :flag:`Polymorphic Inductive Cumulativity` which when set, makes all subsequent *polymorphic* inductive definitions cumulative. When set, inductive types and the like can be enforced to be non-cumulative using the :g:`NonCumulative` @@ -179,7 +177,7 @@ prefix. Declares the inductive as non-cumulative -.. opt:: Polymorphic Inductive Cumulativity +.. flag:: Polymorphic Inductive Cumulativity When this option is on, it sets all following polymorphic inductive types as cumulative (it is off by default). @@ -229,7 +227,7 @@ Cumulative inductive types, coninductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`. +Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`. That is, this option, when set, makes all subsequent *polymorphic* inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) but has no effect on *monomorphic* inductive declarations. @@ -277,18 +275,18 @@ An example of a proof using cumulativity Cumulativity Weak Constraints ----------------------------- -.. opt:: Cumulativity Weak Constraints +.. flag:: Cumulativity Weak Constraints -This option, on by default, causes "weak" constraints to be produced -when comparing universes in an irrelevant position. Processing weak -constraints is delayed until minimization time. A weak constraint -between `u` and `v` when neither is smaller than the other and -one is flexible causes them to be unified. Otherwise the constraint is -silently discarded. + When set, which is the default, causes "weak" constraints to be produced + when comparing universes in an irrelevant position. Processing weak + constraints is delayed until minimization time. A weak constraint + between `u` and `v` when neither is smaller than the other and + one is flexible causes them to be unified. Otherwise the constraint is + silently discarded. -This heuristic is experimental and may change in future versions. -Disabling weak constraints is more predictable but may produce -arbitrary numbers of universes. + This heuristic is experimental and may change in future versions. + Disabling weak constraints is more predictable but may produce + arbitrary numbers of universes. Global and local universes @@ -354,9 +352,9 @@ This minimization process is applied only to fresh universe variables. It simply adds an equation between the variable and its lower bound if it is an atomic universe (i.e. not an algebraic max() universe). -.. opt:: Universe Minimization ToSet +.. flag:: Universe Minimization ToSet - Turning this option off (it is on by default) disallows minimization + Turning this flag off (it is on by default) disallows minimization to the sort :g:`Set` and only collapses floating universes between themselves. @@ -436,7 +434,7 @@ underscore or by omitting the annotation to a polymorphic definition. Check le@{k _}. Check le. -.. opt:: Strict Universe Declaration. +.. flag:: Strict Universe Declaration Turning this option off allows one to freely use identifiers for universes without declaring them first, with the |