• 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
              • Swcase-list->value-list
              • Hex-digit-list->chars
              • Fundef-list->name-list
              • Literal
              • Path
                • Path-fix
                • Path-equiv
                • Make-path
                • Pathp
                • Change-path
                • Path->get
              • 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

Path

Fixtype of paths.

This is a product type introduced by fty::defprod.

Fields
get — identifier-list

A path is a non-empty sequence of identifiers, separated by dots. Here we define a path as a list of identifiers, wrapped in a one-field product type. In the future we may add an invariant that the list is not empty.

Representing paths as a wrapped list of identifiers, as opposed to just a list of identifiers, lets us make a finer distinction between lists of identifiers representing paths (when wrapped), and just lists of identifiers that may be used for other purposes. In other words, the wrapping conveys that it is a path, and that the identifiers in the list are separated by dots (if written in concrete syntax).

Subtopics

Path-fix
Fixing function for path structures.
Path-equiv
Basic equivalence relation for path structures.
Make-path
Basic constructor macro for path structures.
Pathp
Recognizer for path structures.
Change-path
Modifying constructor for path structures.
Path->get
Get the get field from a path.