diff options
| author | coqbot-app[bot] | 2020-11-25 07:51:39 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-25 07:51:39 +0000 |
| commit | 6377fbe0a76a92b2a685ac9efa033487304234d0 (patch) | |
| tree | 0bec2ea0157f63c6ec2b6bbedf52f98ca8b36241 /doc/sphinx/addendum/type-classes.rst | |
| parent | 99931473e6a662fa21575dc1e99a6084a3c850d1 (diff) | |
| parent | b1846e859091e24db1210be53f9193aa3aedb4d9 (diff) | |
Merge PR #13343: Update syntax in auto.rst chapter
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'doc/sphinx/addendum/type-classes.rst')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 98445fca1a..4143d836c4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -335,12 +335,6 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info one_pattern - - .. prodn:: - hint_info ::= %| {? @natural } {? @one_pattern } - one_pattern ::= @one_term - Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of @@ -503,7 +497,7 @@ Typeclasses Transparent, Typeclasses Opaque It is useful when some constants prevent some unifications and make resolution fail. It is also useful to declare constants which - should never be unfolded during proof-search, like fixpoints or + should never be unfolded during proof search, like fixpoints or anything which does not look like an abbreviation. This can additionally speed up proof search as the typeclass map can be indexed by such rigid constants (see @@ -555,7 +549,7 @@ Settings 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). + expensive proof search (i.e. more useless backtracking). .. flag:: Typeclass Resolution For Conversion |