• Top

• Expression

Expressionp

Recognizer for expression structures.

Signature

(expressionp x) → *

Definitions and Theorems

Theorem: consp-when-expressionp

(defthm consp-when-expressionp
  (implies (expressionp x) (consp x))
  :rule-classes :compound-recognizer)