Dobule pipes in language not rendered about redex HOT 4 CLOSED

Opening this Issue revealed a fundamental misunderstanding of Racket's syntax when it comes to pipes (|). It turns out that my expectations were wrong—Redex's typesetting was right.

See the corrected snippet, with escapes on every | within the identifier:

#lang racket
(require redex)

(define-language pipe
  [operator ::= \| \|\| \|\|\|])

(module+ test
  (test-equal (redex-match? pipe operator (term \|)) #t)
  (test-equal (redex-match? pipe operator (term \|\|)) #t)
  (test-equal (redex-match? pipe operator (term \|\|\|)) #t))

(render-language pipe)

Now the typeset version is what I wanted:

If someone wants to explain what || means and how typesetting worked on my wrong example, I'd be thankful.

from redex.

Glad you got this sorted out!

from redex.

In Racket, || is the empty identifier.

Because identifiers are scoped symbols, and any string can be turned to a symbol -- even "⇒" or "λ" or "hello world" -- and we need something to delimit symbols containing whitespace. The delimiter happens to be |:

> (string->symbol "hello world")
'|hello world|

I guess | is the delimiter because it's close to the other delimiters on many keyboards and looks kind of like braces.

For the official explanation, search for "|" in the docs: link

from redex.

@bennn: Thank you for the explanation. I understand what is going on, now.

I didn't know I could search for punctuation on Racket documentation. In all other search engines that I used, it doesn't work, so I just never thought of trying.

Racket keeps impressing me! 👍

from redex.