• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
        • R-and-i-pairs
        • R-and-i-data-types-exercises
        • R-and-i-symbols
        • R-and-i-identity
        • R-and-i-numbers
        • R-and-i-characters
        • R-and-i-strings
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• R-and-i-data-types

R-and-i-characters

Recursion and Induction: Characters

We will not use character objects in this document. In case you come across such an object in your exploration of ACL2, some characters are #\a, #\A, #\Newline and #\Space. It is actually possible in ACL2 to “construct” and “deconstruct” characters in terms of naturals. For example, one can construct #\A from 65, the ASCII code for uppercase `A'.

(Maybe explore <<characters>>?)

Next: Strings (or Table of Contents)