diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 73 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 201 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 108 |
4 files changed, 269 insertions, 118 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index e05df65c63..ef183174d7 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -36,21 +36,29 @@ Sorts ~~~~~~~~~~~ All sorts have a type and there is an infinite well-founded typing -hierarchy of sorts whose base sorts are :math:`\Prop` and :math:`\Set`. +hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` +and :math:`\Set`. The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a logical proposition then it denotes the class of terms representing proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is provable. An object of type :math:`\Prop` is called a proposition. +The sort :math:`\SProp` is like :math:`\Prop` but the propositions in +:math:`\SProp` are known to have irrelevant proofs (all proofs are +equal). Objects of type :math:`\SProp` are called strict propositions. +:math:`\SProp` is rejected except when using the compiler option +``-allow-sprop``. See :ref:`sprop` for information about using +:math:`\SProp`. + The sort :math:`\Set` intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and function types over these data types. -:math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. +:math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of -|Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` +|Cic| has infinitely many sorts. There are, in addition to the base sorts, a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as @@ -63,7 +71,7 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - \Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and :math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`. @@ -113,7 +121,7 @@ language of the *Calculus of Inductive Constructions* is built from the following rules. -#. the sorts :math:`\Set`, :math:`\Prop`, :math:`\Type(i)` are terms. +#. the sorts :math:`\SProp`, :math:`\Prop`, :math:`\Set`, :math:`\Type(i)` are terms. #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms. #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then @@ -293,6 +301,12 @@ following rules. --------------- \WF{E;~c:=t:T}{} +.. inference:: Ax-SProp + + \WFE{\Gamma} + ---------------------- + \WTEG{\SProp}{\Type(1)} + .. inference:: Ax-Prop \WFE{\Gamma} @@ -325,6 +339,14 @@ following rules. ---------------------------------------------------------- \WTEG{c}{T} +.. inference:: Prod-SProp + + \WTEG{T}{s} + s \in {\Sort} + \WTE{\Gamma::(x:T)}{U}{\SProp} + ----------------------------- + \WTEG{\forall~x:T,U}{\SProp} + .. inference:: Prod-Prop \WTEG{T}{s} @@ -336,14 +358,15 @@ following rules. .. inference:: Prod-Set \WTEG{T}{s} - s \in \{\Prop, \Set\} + s \in \{\SProp, \Prop, \Set\} \WTE{\Gamma::(x:T)}{U}{\Set} ---------------------------- \WTEG{∀ x:T,~U}{\Set} .. inference:: Prod-Type - \WTEG{T}{\Type(i)} + \WTEG{T}{s} + s \in \{\SProp, \Type{i}\} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- \WTEG{∀ x:T,~U}{\Type(i)} @@ -524,6 +547,14 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. +.. _proof-irrelevance: + +Proof Irrelevance +~~~~~~~~~~~~~~~~~ + +It is legal to identify any two terms whose common type is a strict +proposition :math:`A : \SProp`. Terms in a strict propositions are +therefore called *irrelevant*. .. _convertibility: @@ -540,7 +571,7 @@ We say that two terms :math:`t_1` and :math:`t_2` are global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and -:math:`u_2` are identical, or they are convertible up to η-expansion, +:math:`u_2` are identical up to irrelevant subterms, or they are convertible up to η-expansion, i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is recursively convertible to :math:`u_1'`, or, symmetrically, :math:`u_2` is :math:`λx:T.~u_2'` @@ -612,6 +643,7 @@ a *subtyping* relation inductively defined by: #. for any :math:`i`, :math:`E[Γ] ⊢ \Set ≤_{βδιζη} \Type(i)`, #. :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Set`, hence, by transitivity, :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)`, for any :math:`i` + (note: :math:`\SProp` is not related by cumulativity to any other term) #. if :math:`E[Γ] ⊢ T =_{βδιζη} U` and :math:`E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'` then :math:`E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′`. @@ -980,9 +1012,9 @@ provided that the following side conditions hold: One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sort :math:`\Prop` but may fail to define inductive type on sort :math:`\Set` and -generate constraints between universes for inductive types in -the Type hierarchy. +sorts :math:`\SProp` and :math:`\Prop` but may fail to define +inductive type on sort :math:`\Set` and generate constraints +between universes for inductive types in the Type hierarchy. .. example:: @@ -1339,14 +1371,15 @@ There is no restriction on the sort of the predicate to be eliminated. The case of Inductive definitions of sort :math:`\Prop` is a bit more complicated, because of our interpretation of this sort. The only -harmless allowed elimination, is the one when predicate :math:`P` is also of -sort :math:`\Prop`. +harmless allowed eliminations, are the ones when predicate :math:`P` +is also of sort :math:`\Prop` or is of the morally smaller sort +:math:`\SProp`. .. inference:: Prop - ~ - --------------- - [I:\Prop|I→\Prop] + s ∈ \{\SProp,\Prop\} + -------------------- + [I:\Prop|I→s] :math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in @@ -1434,6 +1467,14 @@ type. An empty definition has no constructors, in that case also, elimination on any sort is allowed. +.. _Eliminaton-for-SProp: + +Inductive types in :math:`\SProp` must have no constructors (i.e. be +empty) to be eliminated to produce relevant values. + +Note that thanks to proof irrelevance elimination functions can be +produced for other types, for instance the elimination for a unit type +is the identity. .. _Type-of-branches: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c1eab8a970..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 25f983ac1e..18cafd1f21 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -754,10 +754,46 @@ used by ``Function``. A more precise description is given below. Section mechanism ----------------- -The sectioning mechanism can be used to to organize a proof in -structured sections. Then local declarations become available (see -Section :ref:`gallina-definitions`). +Sections create local contexts which can be shared across multiple definitions. +.. example:: + + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. + + .. coqtop:: all + + Section s1. + + Inside a section, local parameters can be introduced using :cmd:`Variable`, + :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for + the first two). + + .. coqtop:: all + + Variables x y : nat. + + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. + + .. coqtop:: in + + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. + + .. coqtop:: all + + Print x'. + Print x''. + + End s1. + + Print x'. + Print x''. + + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. .. cmd:: Section @ident @@ -768,43 +804,80 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident This command closes the section named :token:`ident`. After closing of the - section, the local declarations (variables and local definitions) get + section, the local declarations (variables and local definitions, see :cmd:`Variable`) get *discharged*, meaning that they stop being visible and that all global objects defined in the section are generalized with respect to the variables and local definitions they each depended on in the section. - .. example:: + .. exn:: This is not the last opened section. + :undocumented: - .. coqtop:: all +.. note:: + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which + appear inside a section are canceled when the section is closed. + +.. cmd:: Variable @ident : @type - Section s1. + This command links :token:`type` to the name :token:`ident` in the context of + the current section. When the current section is closed, name :token:`ident` + will be unknown and every object using this variable will be explicitly + parameterized (the variable is *discharged*). - Variables x y : nat. + .. exn:: @ident already exists. + :name: @ident already exists. (Variable) + :undocumented: - Let y' := y. + .. cmdv:: Variable {+ @ident } : @type - Definition x' := S x. + Links :token:`type` to each :token:`ident`. - Definition x'' := x' + y'. + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Print x'. + Declare one or more variables with various types. - End s1. + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } + :name: Variables; Hypothesis; Hypotheses - Print x'. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. - Print x''. +.. cmd:: Let @ident := @term - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` is accessible + only within the current section. When the section is closed, all persistent + definitions and theorems within it and depending on :token:`ident` + will be prefixed by the let-in definition :n:`let @ident := @term in`. - .. exn:: This is not the last opened section. + .. exn:: @ident already exists. + :name: @ident already exists. (Let) :undocumented: -.. note:: - Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which - appear inside a section are canceled when the section is closed. + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: + + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: + +.. cmd:: Context @binders + + Declare variables in the context of the current section, like :cmd:`Variable`, + but also allowing implicit variables, :ref:`implicit-generalization`, and + let-binders. + + .. coqdoc:: + + Context {A : Type} (a b : A). + Context `{EqDec A}. + Context (b' := b). + +.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. Module system ------------- @@ -1575,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | @ident } +.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1592,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1621,7 +1694,7 @@ Declaring Implicit Arguments .. coqtop:: reset all - Inductive list (A:Type) : Type := + Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. @@ -1629,13 +1702,15 @@ Declaring Implicit Arguments Arguments cons [A] _ _. - Arguments nil [A]. + Arguments nil {A}. Check (cons 3 nil). - Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end. + Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := + match l with nil => nil | cons a t => cons (f a) (map A B f t) end. - Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end. + Fixpoint length (A : Type) (l : list A) : nat := + match l with nil => 0 | cons _ m => S (length A m) end. Arguments map [A B] f l. @@ -1651,6 +1726,13 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). +.. warn:: Argument number @num is a trailing implicit so must be maximal. + + For instance in + + .. coqtop:: all warn + + Arguments prod _ [_]. Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1704,19 +1786,15 @@ of constants. For instance, the variable ``p`` below has type ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z`` appear strictly in the body of the type, they are implicit. -.. coqtop:: reset none - - Set Warnings "-local-declaration". - .. coqtop:: all - Variable X : Type. + Parameter X : Type. Definition Relation := X -> X -> Prop. Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z. - Variables (R : Relation) (p : Transitivity R). + Parameters (R : Relation) (p : Transitivity R). Arguments p : default implicits. @@ -1724,7 +1802,7 @@ appear strictly in the body of the type, they are implicit. Print Implicit p. - Variables (a b c : X) (r1 : R a b) (r2 : R b c). + Parameters (a b c : X) (r1 : R a b) (r2 : R b c). Check (p r1 r2). @@ -2023,7 +2101,7 @@ or :g:`m` to the type :g:`nat` of natural numbers). This is useful for declaring the implicit type of a single variable. -.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) } +.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) } Adds blocks of implicit types with different specifications. @@ -2260,3 +2338,52 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9ab3f905e6..8a5e9d87f8 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -94,8 +94,8 @@ Keywords employed otherwise:: _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod Prop return - Set then Type using where with + forall fun if IF in let match mod return + SProp Prop Set Type then using where with Special tokens The following sequences of characters are special tokens:: @@ -159,7 +159,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` - sort : Prop | Set | Type + sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` cofix_bodies : `cofix_body` @@ -218,13 +218,17 @@ numbers (see :ref:`datatypes`). .. index:: single: Set (sort) + single: SProp single: Prop single: Type Sorts ----- -There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. +There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. + +- :g:`SProp` is the universe of *definitionally irrelevant + propositions* (also called *strict propositions*). - :g:`Prop` is the universe of *logical propositions*. The logical propositions themselves are typing the proofs. We denote propositions by :production:`form`. @@ -235,7 +239,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Type` is the type of :g:`Prop` and :g:`Set` +- :g:`Type` is the type of sorts. More on sorts can be found in Section :ref:`sorts`. @@ -626,33 +630,21 @@ has type :token:`type`. These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. -.. cmd:: Variable @ident : @type - - This command links :token:`type` to the name :token:`ident` in the context of - the current section (see Section :ref:`section-mechanism` for a description of - the section mechanism). When the current section is closed, name :token:`ident` - will be unknown and every object using this variable will be explicitly - parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out - of any section is equivalent to using :cmd:`Local Parameter`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Variable) - :undocumented: + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } + :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) - .. cmdv:: Variable {+ @ident } : @term + Outside of any section, these variants are synonyms of + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + For their meaning inside a section, see :cmd:`Variable` in + :ref:`section-mechanism`. - Links :token:`type` to each :token:`ident`. + .. warn:: @ident is declared as a local axiom [local-declaration,scope] - .. cmdv:: Variable {+ ( {+ @ident } : @term ) } - - Adds blocks of variables with different specifications. - - .. cmdv:: Variables {+ ( {+ @ident } : @term) } - Hypothesis {+ ( {+ @ident } : @term) } - Hypotheses {+ ( {+ @ident } : @term) } - :name: Variables; Hypothesis; Hypotheses - - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. + Warning generated when using :cmd:`Variable` instead of + :cmd:`Local Parameter`. .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and @@ -661,6 +653,8 @@ has type :token:`type`. :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases (corresponding to the declaration of an abstract mathematical entity). +.. seealso:: Section :ref:`section-mechanism`. + .. _gallina-definitions: Definitions @@ -700,10 +694,10 @@ Section :ref:`typing-rules`. .. exn:: The term @term has type @type while it is expected to have type @type'. :undocumented: - .. cmdv:: Definition @ident @binders {? : @term } := @term + .. cmdv:: Definition @ident @binders {? : @type } := @term This is equivalent to - :n:`Definition @ident : forall @binders, @term := fun @binders => @term`. + :n:`Definition @ident : forall @binders, @type := fun @binders => @term`. .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term :name: Local Definition @@ -717,32 +711,18 @@ Section :ref:`typing-rules`. This is equivalent to :cmd:`Definition`. -.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + .. cmdv:: Let @ident := @term + :name: Let (outside a section) -.. cmd:: Let @ident := @term + Outside of any section, this variant is a synonym of + :n:`Local Definition @ident := @term`. + For its meaning inside a section, see :cmd:`Let` in + :ref:`section-mechanism`. - This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` disappears when the - current section is eventually closed, and all persistent objects (such - as theorems) defined within the section and depending on :token:`ident` are - prefixed by the let-in definition :n:`let @ident := @term in`. - Using the :cmd:`Let` command out of any section is equivalent to using - :cmd:`Local Definition`. + .. warn:: @ident is declared as a local definition [local-declaration,scope] - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: - - .. cmdv:: Let @ident {? @binders } {? : @type } := @term - :undocumented: - - .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} - :name: Let Fixpoint - :undocumented: - - .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} - :name: Let CoFixpoint - :undocumented: + Warning generated when using :cmd:`Let` instead of + :cmd:`Local Definition`. .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, :cmd:`Transparent`, and tactic :tacn:`unfold`. @@ -767,9 +747,9 @@ Simple inductive types are the names of its constructors and :token:`type` their respective types. Depending on the universe where the inductive type :token:`ident` lives (e.g. its type :token:`sort`), Coq provides a number of destructors. - Destructors are named :token:`ident`\ ``_ind``, :token:`ident`\ ``_rec`` - or :token:`ident`\ ``_rect`` which respectively correspond to elimination - principles on :g:`Prop`, :g:`Set` and :g:`Type`. + Destructors are named :token:`ident`\ ``_sind``,:token:`ident`\ ``_ind``, + :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively + correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. The type of the destructors expresses structural induction/recursion principles over objects of type :token:`ident`. The constant :token:`ident`\ ``_ind`` is always provided, @@ -873,8 +853,8 @@ which is a type whose conclusion is a sort. successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the structural induction principle we got for :g:`nat`. -Parametrized inductive types -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Parameterized inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} @@ -950,7 +930,7 @@ Parametrized inductive types because the conclusion of the type of constructors should be :g:`listw A` in both cases. - + A parametrized inductive definition can be defined using annotations + + A parameterized inductive definition can be defined using annotations instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination. @@ -1010,7 +990,7 @@ Mutually defined inductive types .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } - In this variant, the inductive definitions are parametrized + In this variant, the inductive definitions are parameterized with :token:`binders`. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types. @@ -1023,7 +1003,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1046,7 +1026,7 @@ Mutually defined inductive types Check forest_rec. - Assume we want to parametrize our mutual inductive definitions with the + Assume we want to parameterize our mutual inductive definitions with the two type variables :g:`A` and :g:`B`, the declaration should be done the following way: @@ -1533,7 +1513,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. |