		Search-engine friendly clone of the ACL2 documentation.

Number-subtrees

(number-subtrees x) returns the number of distinct subtrees of X, in the sense of equal

In the logic, number-subtrees is defined as the length of cons-subtrees.

Under the hood, we first hons-copy X to obtain a normed version, then count the number of unique conses in X using an EQ hash table.

Function: number-subtrees

(defun number-subtrees (x)
  (declare (xargs :guard t))
  (len (cons-subtrees x 'number-subtrees)))