|
|
|---|
|
|
|
|---|
ABNF grammar of Leo.
We use our verified ABNF grammar parser to parse the ABNF grammar of Leo into a representation in ACL2.
The grammar consists of two sub-grammars: the lexical grammar and the syntactic grammar. We put them together, in one ACL2 constant for the whole grammar.