		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-internal-line

Signature
(stv-expand-internal-line line usersyms mod) → (mv new-line usersyms)
Arguments: line — Guard (true-listp line).; mod — Guard (good-esim-modulep mod).
Returns: new-line — Type (true-listp new-line).

Definitions and Theorems

Function: stv-expand-internal-line

(defun
 stv-expand-internal-line
 (line usersyms mod)
 (declare (xargs :guard (and (true-listp line)
                             (good-esim-modulep mod))))
 (let
  ((__function__ 'stv-expand-internal-line))
  (declare (ignorable __function__))
  (b*
   (((cons name entries) line)
    ((unless (and (consp name) (true-listp name)))
     (raise
      "Expected :internal line names to be already expanded to ~
                non-empty lists of E paths, but found ~x0."
      name)
     (mv nil usersyms))
    ((mv okp new-name)
     (fast-canonicalize-paths name mod))
    ((unless okp)
     (raise "Failed to canonicalize all the paths for ~x0."
            name)
     (mv nil usersyms))
    ((mv new-entries usersyms)
     (stv-expand-output-entries new-name (len new-name)
                                0 entries usersyms))
    (new-line (cons new-name new-entries)))
   (mv new-line usersyms))))

Theorem: true-listp-of-stv-expand-internal-line.new-line

(defthm true-listp-of-stv-expand-internal-line.new-line
        (b* (((mv ?new-line ?usersyms)
              (stv-expand-internal-line line usersyms mod)))
            (true-listp new-line))
        :rule-classes :type-prescription)