		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-formals

Generate Java code to build a deeply embedded formals parameter list of an ACL2 named function or lambda expression.

Signature
(atj-gen-deep-formals formals) → expr
Arguments: formals — Guard (symbol-listp formals).
Returns: expr — Type (jexprp expr).

The generated code builds an array of the formals as symbols.

Definitions and Theorems

Function: atj-gen-deep-formals

(defun atj-gen-deep-formals (formals)
  (declare (xargs :guard (symbol-listp formals)))
  (let ((__function__ 'atj-gen-deep-formals))
    (declare (ignorable __function__))
    (jexpr-newarray-init *aij-type-symbol*
                         (atj-gen-symbols formals t nil))))

Theorem: jexprp-of-atj-gen-deep-formals

(defthm jexprp-of-atj-gen-deep-formals
  (b* ((expr (atj-gen-deep-formals formals)))
    (jexprp expr))
  :rule-classes :rewrite)