• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
          • Character-listp
          • Characterp
          • Coerce
          • Standard-char-p
            • Standard-char-p+
            • Digit-char-p
            • Code-char
            • Char-code
            • Char-downcase
            • Char
            • Char-upcase
            • Explode-nonnegative-integer
            • Explode-atom
            • Alpha-char-p
            • Upper-case-p
            • Lower-case-p
            • Char-equal
            • Digit-to-char
            • Char<
            • Char>=
            • Make-character-list
            • Char>
            • Char<=
            • Standard-char-listp
            • Character-alistp
            • Standard-char-p+
              • Chars-upcase-gen
              • Chars-downcase-gen
              • Char-upcase-gen
              • Char-downcase-gen
            • Time$
            • Loop$-primer
            • Fast-alists
            • Defmacro
            • Defconst
            • Evaluation
            • Guard
            • Equality-variants
            • Compilation
            • Hons
            • ACL2-built-ins
            • Developers-guide
            • System-attachments
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Irrelevant-formals
            • Efficiency
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Redefining-programs
            • Lists
            • Invariant-risk
            • Errors
            • Defabbrev
            • Conses
            • Alists
            • Set-register-invariant-risk
            • Strings
            • Program-wrapper
            • Get-internal-time
            • Basics
            • Packages
            • Defmacro-untouchable
            • Primitive
            • <<
            • Revert-world
            • Set-duplicate-keys-action
            • Unmemoize
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Defopen
            • Sleep
          • Start-here
          • Real
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Testing-utilities
        • Math
      • Standard-char-p
      • Characters
      • ACL2-built-ins

      Standard-char-p+

      Recognizer for standard characters whose guard is t

      Logically standard-char-p+ is the same as standard-char-p. However, standard-char-p+ has a guard of t, while standard-char-p is guarded by characterp.

      Function: standard-char-p+

      (defun standard-char-p+ (x)
             (declare (xargs :guard t))
             (and (characterp x)
                  (standard-char-p x)))