		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-safe-nonascii

Abstract a safe-nonascii to a Leo character.

Signature
(abs-safe-nonascii tree) → char
Arguments: tree — Guard (abnf::treep tree).
Returns: char — Type (char-resultp char).

Definitions and Theorems

Function: abs-safe-nonascii

(defun abs-safe-nonascii (tree)
  (declare (xargs :guard (abnf::treep tree)))
  (let ((__function__ 'abs-safe-nonascii))
    (declare (ignorable __function__))
    (b* (((okf nat)
          (abnf::check-tree-nonleaf-num-range-4
               tree "safe-nonascii" 128 8233
               8239 8293 8304 55295 57344 1114111)))
      (char nat))))

Theorem: char-resultp-of-abs-safe-nonascii

(defthm char-resultp-of-abs-safe-nonascii
  (b* ((char (abs-safe-nonascii tree)))
    (char-resultp char))
  :rule-classes :rewrite)