• 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-symbols

Recursion and Induction: Symbols

Unlike many languages, Lisp provides symbols as primitive data objects. Some example symbols are t, nil, LOAD, STORE, ICONST_0, prime-factors, ++, and file77. For the purposes of this document, we will treat symbols as atomic objects, though it is actually possible to construct and deconstruct them in terms of strings.

For the purposes of this document, a symbol is a sequence of alphabetic characters, digits, and/or certain signs (specifically, +, -, *, /, =, <, >, ?, !, $, &, and _ (underscore)) that cannot be read as a number. Case is unimportant. Symbols are parsed to have the greatest length possible under the rules above. Thus, xy is one symbol, not two symbols (x and y) written without intervening whitespace!

Note that t and T are different ways to write the same symbol, as are nil, Nil, and NIL. T and nil are called the Boolean symbols. T is frequently used to denote true and nil is used to denote false. For reasons that will become apparent, nil is also used as the empty list.

(Maybe explore <<symbols>>?)

Next: Pairs (or Table of Contents)