• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
              • Escape
                • Escape-case
                • Escape-fix
                • Escapep
                • Escape-equiv
                • Escape-x
                • Escape-u
                • Escape-kind
                • Escape-single-quote
                • Escape-line-feed
                • Escape-letter-t
                • Escape-letter-r
                • Escape-letter-n
                • Escape-double-quote
                • Escape-carriage-return
                • Escape-backslash
              • Swcase-list->value-list
              • Hex-digit-list->chars
              • Fundef-list->name-list
              • Literal
              • Path
              • Hex-string-rest-element
              • Plain-string
              • String-element
              • Hex-string-content-option
              • Hex-string-content
              • Identifier
              • Funcall-option
              • Expression-option
              • Statement-option
              • Literal-option
              • Identifier-option
              • Hex-string
              • Hex-quad
              • Hex-digit
              • Hex-pair
              • Data-value
              • Data-item
              • Statements-to-fundefs
              • String-element-list-result
              • Identifier-identifier-map-result
              • Swcase-result
              • String-element-result
              • Statement-result
              • Literal-result
              • Identifier-set-result
              • Identifier-result
              • Identifier-list-result
              • Fundef-result
              • Funcall-result
              • Expression-result
              • Escape-result
              • Path-result
              • Block-result
              • Objects
              • Statements/blocks/cases/fundefs
              • Identifier-list
              • Identifier-set
              • Identifier-identifier-map
              • Identifier-identifier-alist
              • Hex-string-rest-element-list
              • String-element-list
              • Path-list
              • Hex-digit-list
              • Literal-list
              • Fundef-list
              • Expressions/funcalls
              • Abstract-syntax-induction-schemas
            • Dynamic-semantics
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Abstract-syntax

Escape

Fixtype of escapes.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:single-quote → escape-single-quote
:double-quote → escape-double-quote
:backslash → escape-backslash
:letter-n → escape-letter-n
:letter-r → escape-letter-r
:letter-t → escape-letter-t
:line-feed → escape-line-feed
:carriage-return → escape-carriage-return
:x → escape-x
:u → escape-u

These are the escapes used in string literals. They are all preceded by backslash, which we do not need to represent explicitly in abstract syntax. There are simple escapes consisting of a single character just after the backslash, as well as escapes consisting of x (not explicitly represented) followed by a pair of hex digits, and Unicode escapes consisting of u (not explicitly represented) followed by a quadruple of hex digits. Thus in this abstract syntax of escapes we capture all the information from the concrete syntax.

Subtopics

Escape-case
Case macro for the different kinds of escape structures.
Escape-fix
Fixing function for escape structures.
Escapep
Recognizer for escape structures.
Escape-equiv
Basic equivalence relation for escape structures.
Escape-x
Escape-u
Escape-kind
Get the kind (tag) of a escape structure.
Escape-single-quote
Escape-line-feed
Escape-letter-t
Escape-letter-r
Escape-letter-n
Escape-double-quote
Escape-carriage-return
Escape-backslash