		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-symbol-2part

Check if a symbol consists of two parts separated by dash.

Signature
(atc-check-symbol-2part sym) → (mv yes/no part1 part2)
Arguments: sym — Guard (symbolp sym).
Returns: yes/no — Type (booleanp yes/no).; part1 — Type (symbolp part1).; part2 — Type (symbolp part2).

If the symbol has the form <part1>-<part2>, with <part1> and <part2> non-empty and without dashes, we return an indication of success and the two parts. Otherwise, we return an indication of failure and nil as the parts. The two returned symbols, when the function is successful, are interned in the same package as the input symbol.

Definitions and Theorems

Function: atc-check-symbol-2part

(defun atc-check-symbol-2part (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((__function__ 'atc-check-symbol-2part))
    (declare (ignorable __function__))
    (b* ((parts (str::strtok! (symbol-name sym)
                              (list #\-)))
         ((unless (= (len parts) 2))
          (mv nil nil nil))
         (part1 (intern-in-package-of-symbol (first parts)
                                             sym))
         (part2 (intern-in-package-of-symbol (second parts)
                                             sym)))
      (mv t part1 part2))))

Theorem: booleanp-of-atc-check-symbol-2part.yes/no

(defthm booleanp-of-atc-check-symbol-2part.yes/no
  (b* (((mv ?yes/no ?part1 ?part2)
        (atc-check-symbol-2part sym)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-2part.part1

(defthm symbolp-of-atc-check-symbol-2part.part1
  (b* (((mv ?yes/no ?part1 ?part2)
        (atc-check-symbol-2part sym)))
    (symbolp part1))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-2part.part2

(defthm symbolp-of-atc-check-symbol-2part.part2
  (b* (((mv ?yes/no ?part1 ?part2)
        (atc-check-symbol-2part sym)))
    (symbolp part2))
  :rule-classes :rewrite)