		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-boolean

Given a :nonleaf tree with rulename "boolean", return the appropriate literal AST node.

Signature
(cst2ast-boolean tree) → ast-node?
Arguments: tree — Guard (abnf::treep tree).
Returns: ast-node? — Type (literal-optionp ast-node?).

Definitions and Theorems

Function: cst2ast-boolean

(defun cst2ast-boolean (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'cst2ast-boolean))
  (declare (ignorable __function__))
  (b*
   ((fringe (abnf::tree->string tree))
    ((unless (acl2::unsigned-byte-listp 8 fringe))
     (prog2$
      (er
         hard? 'top-level
         "unexpected type of leafterm nats when parsing identifier")
      nil))
    (fringe-string (acl2::nats=>string fringe)))
   (cond ((equal fringe-string "true")
          (make-literal-boolean :get t))
         ((equal fringe-string "false")
          (make-literal-boolean :get nil))
         (t nil)))))

Theorem: literal-optionp-of-cst2ast-boolean

(defthm literal-optionp-of-cst2ast-boolean
  (b* ((ast-node? (cst2ast-boolean tree)))
    (literal-optionp ast-node?))
  :rule-classes :rewrite)