diff --git a/_02_.Writing-programs.sz b/_02_.Writing-programs.sz
index c0ed80e..5885198 100644
--- a/_02_.Writing-programs.sz
+++ b/_02_.Writing-programs.sz
@@ -1353,14 +1353,15 @@ The hash macro 'card' failed at bad.bjo:3: a suit is clubs, diamonds, hearts or
 
 Notice the @code{re-export} in @code{cardmacros.bjo}: because the macro expansion emits constructor symbols like @code{Card} and @code{Queen}, those types must be resolvable in the module invoking the macro. Re-exporting them ensures that importing @code{cardmacros.bjo} alone brings the required types into scope. Importing @code{deck.bjo} alongside it remains recommended so that the corresponding @code{->str} implementations are also present.
 
-@subsubsection{Literals that elaborate into your unions}
+@subsubsection{Literals read by a grammar}
 
-Many embedded domain-specific languages do not require macros at all. In contexts where the type checker expects a specific union type, quoted lists can elaborate directly into union cases. Union cases specify their literal keyword tag using @code{#:tag}:
+Many embedded domain-specific languages do not need macros. A grammar says how a quoted literal of a type is written, and declares the type. Where the type checker expects the type, a quoted literal becomes its constructors:
 
 @codeblock[#:lang "bjolang"]|{
-(type (: Action (Union (: Play int #:tag play)
-                       (: Say string #:tag say)
-                       (: Pass #:tag pass))))
+(def/grammar Action
+  (:or (: Play (play int))
+       (: Say (say string))
+       (: Pass 'pass)))
 
 (: script (List Action))
 (def script '((play 3) (say "your turn") pass (play 1)))
@@ -1370,14 +1371,14 @@ Many embedded domain-specific languages do not require macros at all. In context
 (def (: more (List Action)) '((play ,n) pass))
 }|
 
-Because elaboration is handled by the type checker rather than a syntactic macro, misspelled tags or invalid argument counts produce standard type errors:
+@code{Action} is an ordinary union, and @code{match} takes its cases. The type checker reads the literal, so a misspelled keyword or a wrong number of items is a compile error that says what can come at that place:
 
 @codeblock[#:lang "text"]|{
-Type Error at elab2.bjo:5: `sya` is not a tag of the union elab2/Action and no case of it
-carries a list, so this literal cannot be one. Its tags are play, say or pass.
+Type Error at elab2.bjo:5: Action: expected (play ...), (say ...) or `pass`; found (sya ...).
+Type Error at elab2.bjo:5: (play ...): expected the end of the list; found the number 2.
 }|
 
-This elaboration mechanism only applies in positions where the type checker already knows that a specific union type is expected (which is why @code{script} and @code{more} include explicit type signatures). Standard library modules like @code{(std run)} and @code{(std fmt)} use this exact technique for command pipelines and text layouts.
+A grammar reads a literal only where the type checker already expects one of its types, which is why @code{script} and @code{more} have signatures. A grammar can also have several productions, items in any order with @code{:each}, optional items, repeats with @code{...} and @code{...+}, parameters, and atoms that a function checks when the literal is compiled. @code{(std run)}, @code{(std fmt)} and @code{(std url)} use grammars for pipelines, layouts and URLs. The language reference describes every form: see @code{Docs/Syntax.org} and @code{Docs/Grammar-design.org} in the Bjolang repository.
 
 @subsubsection{Computing a value once}
 
diff --git a/_03.Standard-library.sz b/_03.Standard-library.sz
index 6408c0c..eed722e 100644
--- a/_03.Standard-library.sz
+++ b/_03.Standard-library.sz
@@ -31,7 +31,7 @@ For more details, see @link["modules/std/http.html"]{@code{(std http)}}.
 
 @subsection{std/url}
 
-URLs by RFC 3986. A URL is written as a quoted literal, as @code{(std run)} writes a pipeline: @code{(link '(url https "example.com" (path "users" ,name) (query (page 2) (tag ,tag)) (fragment "top")))}, or @code{'(path "users" ,id "edit")} for a path on this site. Each value is encoded for the part that it is in, so a @code{/} in a computed segment does not make a second segment, and a @code{&} in a computed value does not make a second parameter. The compiler checks the parts of a literal where it is written. @code{parse-url} reads a URL or a relative reference strictly, and refuses text that is not one with the column where it goes wrong. A @code{Url} keeps each part as it was written, so @code{url->string} gives back the same text. @code{url-resolve} reads a link where a page is. @code{url-segments} and @code{url-params} decode the path and the query, and there is one percent-encoder for each part of a URL.
+URLs by RFC 3986. A URL is written as a quoted literal, as @code{(std run)} writes a pipeline: @code{(link '(url https "example.com" (path "users" ,name) (query (page 2) (tag ,tag)) (fragment "top")))}, or @code{'(path "users" ,id "edit")} for a path on this site. Each value is encoded for the part that it is in, so a @code{/} in a computed segment does not make a second segment, and a @code{&} in a computed value does not make a second parameter. A grammar reads the literal, so the compiler checks its parts where it is written: a misspelled part, a part given twice, a port out of range or a host that is no host is a compile error. A computed scheme, host or port is made with @code{scheme}, @code{host} or @code{port}, which return a @code{Result}, so @code{make-url} does not fail. @code{parse-url} reads a URL or a relative reference strictly, and refuses text that is not one with the column where it goes wrong. A @code{Url} keeps each part as it was written, so @code{url->string} gives back the same text. @code{url-resolve} reads a link where a page is. @code{url-segments} and @code{url-params} decode the path and the query, and there is one percent-encoder for each part of a URL.
 For more details, see @link["modules/std/url.html"]{@code{(std url)}}.
 
 @subsection{std/run}