		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Ambiguity (and unambiguity) in ABNF grammars.

This part of the ABNF formalization is work in progress. More definitions and theorems should be added.

Concatenation-alternation-disjointp: Notion of disjoint concatenation-alternation pairs.
Concatenation-unambiguousp: Notion of unambiguous concatenations.
Repetition-unambiguousp: Notion of unambiguous repetitions.
Alternation-unambiguousp: Notion of unambiguous alternations.
Alternation-unambiguousp-of-cons-when-disjointp: If an umambiguous concatenation is disjoint from an unambiguous alternation, then adding the concatenation maintains the alternation unambiguous.
Element-unambiguousp: Notion of unambiguous elements.
Rules-ambiguousp: Notion of ambiguous lists of rules.
Prose-val-ambiguous: Prose value notations are always ambiguous.
Num-val-unambiguous: Numeric value notations are never ambiguous.
Char-val-unambiguous: Character value notations are never ambiguous.
Element-prose-val-ambiguous: Prose value elements are always ambiguous.
Element-num-val-unambiguous: Numeric value elements are never ambiguous.
Element-char-val-unambiguous: Character value elements are never ambiguous.