diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 109 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 26 |
2 files changed, 83 insertions, 52 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ba766c8c3d..c48964d66c 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions. Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term @@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any :token:`module_binding`. The output module type is verified against each :token:`module_type`. -.. cmdv:: Module [ Import | Export ] +.. cmdv:: Module {| Import | Export } Behaves like :cmd:`Module`, but automatically imports or exports the module. @@ -1648,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1665,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @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 } | @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 } | @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 @@ -2131,24 +2131,71 @@ Implicit generalization .. index:: `{ } .. index:: `( ) +.. index:: `{! } +.. index:: `(! ) Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are -quantified explicitly. Implicit generalization is done inside binders -starting with a \` and terms delimited by \`{ } and \`( ), always -introducing maximally inserted implicit arguments for the generalized -variables. Inside implicit generalization delimiters, free variables -in the current context are automatically quantified using a product or -a lambda abstraction to generate a closed term. In the following -statement for example, the variables n and m are automatically -generalized and become explicit arguments of the lemma as we are using -\`( ): +quantified explicitly. -.. coqtop:: all +It is activated for a binder by prefixing a \`, and for terms by +surrounding it with \`{ } or \`( ). + +Terms surrounded by \`{ } introduce their free variables as maximally +inserted implicit arguments, and terms surrounded by \`( ) introduce +them as explicit arguments. + +Generalizing binders always introduce their free variables as +maximally inserted implicit arguments. The binder itself introduces +its argument as usual. + +In the following statement, ``A`` and ``y`` are automatically +generalized, ``A`` is implicit and ``x``, ``y`` and the anonymous +equality argument are explicit. + +.. coqtop:: all reset Generalizable All Variables. - Lemma nat_comm : `(n = n + 0). + Definition sym `(x:A) : `(x = y -> y = x) := fun _ p => eq_sym p. + + Print sym. + +Dually to normal binders, the name is optional but the type is required: + +.. coqtop:: all + + Check (forall `{x = y :> A}, y = x). + +When generalizing a binder whose type is a typeclass, its own class +arguments are omitted from the syntax and are generalized using +automatic names, without instance search. Other arguments are also +generalized unless provided. This produces a fully general statement. +this behaviour may be disabled by prefixing the type with a ``!`` or +by forcing the typeclass name to be an explicit application using +``@`` (however the later ignores implicit argument information). + +.. coqtop:: all + + Class Op (A:Type) := op : A -> A -> A. + + Class Commutative (A:Type) `(Op A) := commutative : forall x y, op x y = op y x. + Instance nat_op : Op nat := plus. + + Set Printing Implicit. + Check (forall `{Commutative }, True). + Check (forall `{Commutative nat}, True). + Fail Check (forall `{Commutative nat _}, True). + Fail Check (forall `{!Commutative nat}, True). + Arguments Commutative _ {_}. + Check (forall `{!Commutative nat}, True). + Check (forall `{@Commutative nat plus}, True). + +Multiple binders can be merged using ``,`` as a separator: + +.. coqtop:: all + + Check (forall `{Commutative A, Hnat : !Commutative nat}, True). One can control the set of generalizable identifiers with the ``Generalizable`` vernacular command to avoid unexpected @@ -2167,7 +2214,7 @@ that specify which variables should be generalizable. Disable implicit generalization entirely. This is the default behavior. -.. cmd:: Generalizable (Variable | Variables) {+ @ident } +.. cmd:: Generalizable {| Variable | Variables } {+ @ident } Allow generalization of the given identifiers only. Calling this command multiple times adds to the allowed identifiers. @@ -2176,22 +2223,6 @@ that specify which variables should be generalizable. Allows exporting the choice of generalizable variables. -One can also use implicit generalization for binders, in which case -the generalized variables are added as binders and set maximally -implicit. - -.. coqtop:: all - - Definition id `(x : A) : A := x. - - Print id. - -The generalizing binders \`{ } and \`( ) work similarly to their -explicit counterparts, only binding the generalized variables -implicitly, as maximally-inserted arguments. In these binders, the -binding name for the bound object is optional, whereas the type is -mandatory, dually to regular binders. - .. _Coercions: Coercions diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5a1af9f9fa..8acbcbec8f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -616,34 +616,34 @@ has type :token:`type`. Adds several parameters with specification :token:`type`. - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } Adds blocks of parameters with different specifications. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } :name: Local Parameter Such parameters are never made accessible through their unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } :name: Parameters; Axiom; Axioms; Conjecture; Conjectures - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } + .. 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) Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. |