Filtering...

conjoin-equalities

books/std/system/conjoin-equalities

Included Books

define constructors conjoin
other
(in-package "ACL2")
include-book
(include-book "std/util/define" :dir :system)
include-book
(include-book "xdoc/constructors" :dir :system)
local
(local (include-book "conjoin"))
other
(define conjoin-equalities
  ((lefts pseudo-term-listp) (rights pseudo-term-listp))
  :guard (= (len lefts) (len rights))
  :returns (term pseudo-termp :hyp :guard)
  :parents (std/system/term-transformations)
  :short "Build a conjunction of equalities with the given
          left-hand and right-hand sides."
  (conjoin (conjoin-equalities-aux lefts rights))
  :prepwork ((define conjoin-equalities-aux
     ((lefts pseudo-term-listp) (rights pseudo-term-listp))
     :guard (= (len lefts) (len rights))
     :returns (equalities pseudo-term-listp :hyp :guard)
     (if (endp lefts)
       nil
       (cons `(equal ,(CAR LEFTS) ,(CAR RIGHTS))
         (conjoin-equalities-aux (cdr lefts) (cdr rights)))))))