From 30cbf95e6a717e71fb8bda6b15a7253aed36115a Mon Sep 17 00:00:00 2001 From: Matthew Butterick Date: Thu, 4 May 2023 22:05:32 -0700 Subject: [PATCH] =?UTF-8?q?doc=20fix:=C2=A0=3F=20is=20used=20for=20quantif?= =?UTF-8?q?ication?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- brag/brag/brag.scrbl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/brag/brag/brag.scrbl b/brag/brag/brag.scrbl index 2babb1d..47ee7e5 100755 --- a/brag/brag/brag.scrbl +++ b/brag/brag/brag.scrbl @@ -689,8 +689,8 @@ continues till the end of the line. A @deftech{multiline comment} begins with @litchar{(*} and ends with @litchar{*)}. An @deftech{identifier} is a sequence of letters, numbers, or -characters in the set @racket["-.!$%&/<=>?^_~@"]. It must not contain -@litchar{*}, @litchar{+}, or @litchar|{{}| and @litchar|{}}|, as those characters are used to denote quantification. +characters in the set @racket["-.!$%&/<=>^_~@"]. It must not contain +@litchar{*}, @litchar{+}, @litchar{?}, or @litchar|{{}| and @litchar|{}}|, as those characters are used to denote quantification. A @deftech{pattern} is one of the following: @itemize[