		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Element-wfp

An element is well-formed iff its constituents are well-formed.

Signature
(element-wfp element) → yes/no
Arguments: element — Guard (elementp element).
Returns: yes/no — Type (booleanp yes/no).

This condition is structural.

Function: element-wfp

(defun element-wfp (element)
  (declare (xargs :guard (elementp element)))
  (element-case element
                :rulename (rulename-wfp element.get)
                :group (alternation-wfp element.get)
                :option (alternation-wfp element.get)
                :char-val (char-val-wfp element.get)
                :num-val (num-val-wfp element.get)
                :prose-val (prose-val-wfp element.get)))