		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Strin-get-file

Simple wrapper that fixes the filename number to a string.

Signature
(strin-get-file x) → str
Arguments: x — Guard (strin-p x).
Returns: str — Type (stringp str).

This just lets us always assume that sin-file is a string. We typically leave this disabled, because there's not much reason to want to expose the implementation.

Definitions and Theorems

Function: strin-get-file$inline

(defun strin-get-file$inline (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-get-file))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((file (strin->file x)))
           (if (stringp file) file ""))
         :exec (strin->file x))))

Theorem: stringp-of-strin-get-file

(defthm stringp-of-strin-get-file
  (b* ((str (strin-get-file$inline x)))
    (stringp str))
  :rule-classes :type-prescription)