		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-imatrix

Retrieve the matrix of a function introduced via defun-sk, in untranslated form.

Signature
(defun-sk-imatrix fn wrld) → imatrix
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: imatrix — An untranslated term.

The i that starts imatrix in the name of this function conveys that the result is based on the defun-sk form that introduced fn.

Use defun-sk-matrix to retrieve the matrix in translated form.

Definitions and Theorems

Function: defun-sk-imatrix

(defun defun-sk-imatrix (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defun-sk-namep fn wrld))))
  (let ((__function__ 'defun-sk-imatrix))
    (declare (ignorable __function__))
    (third (defun-sk-body fn wrld))))