From 8053f2119db44562df90395e1a694dd1c90299df 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 [Cherry-picked b1670dc46cd6a6661d414a1d65baf17cdd635fec] --- 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