		Search-engine friendly clone of the ACL2 documentation.

Tfunction-lambda

Make-tfunction-lambda

Basic constructor macro for tfunction-lambda structures.

Syntax

(make-tfunction-lambda [:parameters <parameters>] 
                       [:body <body>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-tfunction-lambda

(defmacro make-tfunction-lambda (&rest args)
  (std::make-aggregate 'tfunction-lambda
                       args '((:parameters) (:body))
                       'make-tfunction-lambda
                       nil))

Function: tfunction-lambda

(defun tfunction-lambda (parameters body)
  (declare (xargs :guard (and (symbol-value-listp parameters)
                              (ttermp body))))
  (declare (xargs :guard t))
  (let ((__function__ 'tfunction-lambda))
    (declare (ignorable __function__))
    (b* ((parameters (mbe :logic (symbol-value-list-fix parameters)
                          :exec parameters))
         (body (mbe :logic (tterm-fix body)
                    :exec body)))
      (cons :lambda (list parameters body)))))