		Search-engine friendly clone of the ACL2 documentation.

Simple-escape

Simple-escape-kind

Get the kind (tag) of a simple-escape structure.

Signature
(simple-escape-kind x) → kind
Arguments: x — Guard (simple-escapep x).

Definitions and Theorems

Function: simple-escape-kind$inline

(defun simple-escape-kind$inline (x)
  (declare (xargs :guard (simple-escapep x)))
  (let ((__function__ 'simple-escape-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :squote))
                       :squote)
                      ((eq (car x) :dquote) :dquote)
                      ((eq (car x) :qmark) :qmark)
                      ((eq (car x) :bslash) :bslash)
                      ((eq (car x) :a) :a)
                      ((eq (car x) :b) :b)
                      ((eq (car x) :f) :f)
                      ((eq (car x) :n) :n)
                      ((eq (car x) :r) :r)
                      ((eq (car x) :t) :t)
                      ((eq (car x) :v) :v)
                      (t :percent))
         :exec (car x))))

Theorem: simple-escape-kind-possibilities

(defthm simple-escape-kind-possibilities
  (or (equal (simple-escape-kind x) :squote)
      (equal (simple-escape-kind x) :dquote)
      (equal (simple-escape-kind x) :qmark)
      (equal (simple-escape-kind x) :bslash)
      (equal (simple-escape-kind x) :a)
      (equal (simple-escape-kind x) :b)
      (equal (simple-escape-kind x) :f)
      (equal (simple-escape-kind x) :n)
      (equal (simple-escape-kind x) :r)
      (equal (simple-escape-kind x) :t)
      (equal (simple-escape-kind x) :v)
      (equal (simple-escape-kind x) :percent))
  :rule-classes
  ((:forward-chaining :trigger-terms ((simple-escape-kind x)))))