		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Empty-strin

Create an empty strin-p structure.

Signature
(empty-strin) → *

This is very unlikely to be useful to you. It exists only because we need an abstract strin-p corresponding to the initial sin$c.

We just leave this enabled.

Definitions and Theorems

Function: empty-strin

(defun empty-strin nil
  (declare (xargs :guard t))
  (let ((__function__ 'empty-strin))
    (declare (ignorable __function__))
    (make-strin :chars nil
                :file ""
                :line 1
                :col 0)))