diff --git a/structures_and_records.md b/structures_and_records.md index b3a0c1c5..664d6a84 100644 --- a/structures_and_records.md +++ b/structures_and_records.md @@ -178,9 +178,9 @@ fields were defined. Lean therefore provides the following alternative notations for defining elements of a structure type. ``` - { ( := )* : structure-type } + { ( := ,)* : structure-type } or - { ( := )* } + { ( := ,)* } ``` The suffix ``: structure-type`` can be omitted whenever the name of