|
|
|---|
|
|
|
|---|
Validation of the concrete syntax rules.
We show that the concrete syntax rules are well-formed.
Additonal properties, such as closure, do not hold just for the concrete syntax rules: they must be completed with (some of) the core rules. See concrete-syntax-validation.
As done for core-rules-validation, we put the validation of the concrete syntax rules in a separate file so that their definition does not depend on grammar operations.
Theorem:
(defthm rulelist-wfp-of-*concrete-syntax-rules* (rulelist-wfp *concrete-syntax-rules*))