diff options
| author | Théo Zimmermann | 2020-04-28 10:20:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-28 10:20:37 +0200 |
| commit | 25c7e0cb30a7e196a293df9620bc4b801eaafa27 (patch) | |
| tree | 50d801f404aa55208e97a736f64e77edf08f2cda /doc/sphinx/addendum | |
| parent | d15b99d93b67f37a0c572950868713b2a7a2b1a4 (diff) | |
| parent | a7f56cb5799bc830285f4acf96678486a5929172 (diff) | |
Merge PR #11718: Convert syntax extensions chapter to prodn
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index cfaa681d20..a6dc15da55 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,6 +37,8 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. +Formally, the syntax of classes is defined as: + .. insertprodn class class .. prodn:: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index bd4c276571..903aa266e2 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -241,7 +241,7 @@ binders. For example: Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). -The ``!`` modifier switches the way a binder is parsed back to the regular +The ``!`` modifier switches the way a binder is parsed back to the usual interpretation of Coq. In particular, it uses the implicit arguments mechanism if available, as shown in the example. @@ -323,7 +323,7 @@ Summary of the commands .. cmdv:: Existing Class @ident - This variant declares a class a posteriori from a constant or + This variant declares a class from a previously declared constant or inductive definition. No methods or instances are defined. .. warn:: @ident is already declared as a typeclass @@ -394,7 +394,7 @@ few other commands related to typeclasses. :name: typeclasses eauto This proof search tactic implements the resolution engine that is run - implicitly during type-checking. This tactic uses a different resolution + implicitly during type checking. This tactic uses a different resolution engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the following: |