		Search-engine friendly clone of the ACL2 documentation.

Lhs-override

Make-lhs-override

Basic constructor macro for lhs-override structures.

Syntax

(make-lhs-override [:lhs <lhs>] 
                   [:test <test>] 
                   [:val <val>])

This is the usual way to construct lhs-override structures. It simply conses together a structure with the specified fields.

This macro generates a new lhs-override structure from scratch. See also change-lhs-override, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-lhs-override

(defmacro make-lhs-override (&rest args)
  (std::make-aggregate 'lhs-override
                       args '((:lhs) (:test) (:val))
                       'make-lhs-override
                       nil))

Function: lhs-override

(defun lhs-override (lhs test val)
  (declare (xargs :guard (and (lhs-p lhs)
                              (svex-p test)
                              (svex-p val))))
  (declare (xargs :guard t))
  (let ((__function__ 'lhs-override))
    (declare (ignorable __function__))
    (b* ((lhs (mbe :logic (lhs-fix lhs) :exec lhs))
         (test (mbe :logic (svex-fix test) :exec test))
         (val (mbe :logic (svex-fix val) :exec val)))
      (std::prod-cons lhs (std::prod-cons test val)))))