		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-check-noncanonical-paths

Checks that the listed paths all exist in the module

Signature
(stv-check-noncanonical-paths paths mod) → *

Definitions and Theorems

Function: stv-check-noncanonical-paths

(defun stv-check-noncanonical-paths (paths mod)
  (declare (xargs :guard t))
  (let ((__function__ 'stv-check-noncanonical-paths))
    (declare (ignorable __function__))
    (b* (((when (atom paths)) nil)
         (path (car paths))
         (submod (follow-esim-path path mod))
         (wirename (if (atom path)
                       path
                     (cdr (last path)))))
      (if (and wirename (symbolp wirename))
          (or (member-of-pat-flatten wirename (gpl :i submod))
              (find-in-occs-field :o wirename (gpl :occs submod))
              (raise "Path ~x0 does not exist" path))
        (raise "~x0 is not a valid wirename" wirename))
      (stv-check-noncanonical-paths (cdr paths)
                                    mod))))