diff --git a/docs/_docs/reference/contextual/givens.md b/docs/_docs/reference/contextual/givens.md index f1333bf8811f..bf018278c9fc 100644 --- a/docs/_docs/reference/contextual/givens.md +++ b/docs/_docs/reference/contextual/givens.md @@ -181,7 +181,7 @@ GivenDef ::= [GivenSig] StructuralInstance | [GivenSig] AnnotType ‘=’ Expr | [GivenSig] AnnotType GivenSig ::= [id] [DefTypeParamClause] {UsingParamClause} ‘:’ -StructuralInstance ::= ConstrApp {‘with’ ConstrApp} ‘with’ TemplateBody +StructuralInstance ::= ConstrApp {‘with’ ConstrApp} [‘with’ TemplateBody] ``` A given instance starts with the reserved word `given` and an optional _signature_. The signature