diff options
| author | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
| commit | bdc5db891aa2a060387da758d8910a82cea21da1 (patch) | |
| tree | 8122c3a46ee68b7b5f0f3c263d8516a40e08347c /doc/sphinx/language | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Add missing ";" in record grammar
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4cdfba146a..39b154de8d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -13,7 +13,7 @@ Inductive types .. prodn:: inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } - | {? @ident } %{ {*; @record_field } %} + | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } This command defines one or more diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index cd44d06e67..b2099b8636 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term - term_record ::= %{%| {* @field_def } %|%} + term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term |