• 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• R-and-i-data-types

R-and-i-strings

Recursion and Induction: Strings

Strings in our subset of ACL2 are written as sequences of ASCII characters between successive string quotes. For example, here is a string: "Hello, World!". For the purposes of this document, we will treat strings as atomic objects, though it is actually possible to construct and deconstruct them in terms of lists of character objects.

(Maybe explore <<strings>>?)

Next: Symbols (or Table of Contents)