From b1670dc46cd6a6661d414a1d65baf17cdd635fec Mon Sep 17 00:00:00 2001 From: Seth Tisue Date: Tue, 21 Nov 2023 13:24:39 -0800 Subject: [PATCH] reference doc: fix incorrect syntax production --- docs/_docs/reference/contextual/givens.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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