		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-let

Execute a :let command.

Signature
(defisar-let let-args bindings ctx state) → (mv erp new-bindings state)
Arguments: bindings — Guard (symbol-alistp bindings).
Returns: new-bindings — Type (symbol-alistp new-bindings), given (symbol-alistp bindings).

A :let command takes exactly one argument, which must be a list of a variable symbol and a term. The variable symbol must not be already bound. We do no check he term here: we implicitly check it when the bound variable is used.

Definitions and Theorems

Function: defisar-let

(defun defisar-let (let-args bindings ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbol-alistp bindings)))
  (let ((__function__ 'defisar-let))
    (declare (ignorable __function__))
    (b* (((unless (tuplep 1 let-args))
          (er-soft+ ctx
                    t nil "Malformed :LET arguments ~x0."
                    let-args))
         (let-var+term (car let-args))
         ((unless (tuplep 2 let-var+term))
          (er-soft+ ctx t nil "Malformed :LET argument ~x0."
                    let-var+term))
         (let-var (first let-var+term))
         (let-term (second let-var+term))
         ((unless (symbolp let-var))
          (er-soft+ ctx t
                    nil "The variable ~x0 must be a symbol."
                    let-var))
         ((when (consp (assoc-eq let-var bindings)))
          (er-soft+ ctx t
                    nil "Duplicate variable ~x0." let-var)))
      (value (acons let-var let-term bindings)))))

Theorem: symbol-alistp-of-defisar-let.new-bindings

(defthm symbol-alistp-of-defisar-let.new-bindings
  (implies (symbol-alistp bindings)
           (b* (((mv ?erp ?new-bindings acl2::?state)
                 (defisar-let let-args bindings ctx state)))
             (symbol-alistp new-bindings)))
  :rule-classes :rewrite)