		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Plexeme-hashp

Check if a lexeme is a hash #.

Signature
(plexeme-hashp lexeme) → yes/no
Arguments: lexeme — Guard (plexemep lexeme).
Returns: yes/no — Type (booleanp yes/no).

That is, check if the lexeme is the punctuator #, or also if the lexeme is the digraph %: [C17:6.4.6/3].

Definitions and Theorems

Function: plexeme-hashp

(defun plexeme-hashp (lexeme)
  (declare (xargs :guard (plexemep lexeme)))
  (and (plexeme-case lexeme :punctuator)
       (b* ((string (plexeme-punctuator->punctuator lexeme)))
         (or (equal string "#")
             (equal string "%:")))))

Theorem: booleanp-of-plexeme-hashp

(defthm booleanp-of-plexeme-hashp
  (b* ((yes/no (plexeme-hashp lexeme)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: plexeme-hashp-of-plexeme-fix-lexeme

(defthm plexeme-hashp-of-plexeme-fix-lexeme
  (equal (plexeme-hashp (plexeme-fix lexeme))
         (plexeme-hashp lexeme)))

Theorem: plexeme-hashp-plexeme-equiv-congruence-on-lexeme

(defthm plexeme-hashp-plexeme-equiv-congruence-on-lexeme
  (implies (plexeme-equiv lexeme lexeme-equiv)
           (equal (plexeme-hashp lexeme)
                  (plexeme-hashp lexeme-equiv)))
  :rule-classes :congruence)