		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Strin-get-line

Wrapper for strin->line that fixes the line number to a posp.

Signature
(strin-get-line x) → col
Arguments: x — Guard (strin-p x).
Returns: col — Type (posp col).

This just lets us always assume that sin-line is a posp. We typically just leave this disabled, because who wants to reason about line numbers?

Definitions and Theorems

Function: strin-get-line$inline

(defun strin-get-line$inline (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-get-line))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((line (strin->line x)))
           (if (posp line) line 1))
         :exec (strin->line x))))

Theorem: posp-of-strin-get-line

(defthm posp-of-strin-get-line
  (b* ((col (strin-get-line$inline x)))
    (posp col))
  :rule-classes :type-prescription)