same-lengthp

(in-package "ACL2")

(defsection same-lengthp
  :parents (len)
  :short "Efficiently checks if two lists have the same length."
  :long "<p>In the logic this is just @('(equal (len x) (len y))').  For faster
execution, we walk down both lists together so that we can terminate early.</p>

<p>We leave @('same-lengthp') enabled, and reason about @('len') instead.</p>"
  (defun same-lengthp
    (x y)
    (declare (xargs :guard t))
    (mbe :logic (equal (len x) (len y))
      :exec (if (consp x)
        (and (consp y) (same-lengthp (cdr x) (cdr y)))
        (not (consp y))))))