• 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
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
              • Grammar
              • Files
              • Grammar-character-p
              • Keywords
              • Grammar-character-listp
              • File-paths
                • Filepath-option
                • Filepath
                  • Filepath-fix
                  • Filepath-equiv
                  • Filepathp
                  • Make-filepath
                  • Filepath->unwrap
                  • Change-filepath
                • Filepath-set
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • 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
  • File-paths

Filepath

Fixtype of file paths.

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

Fields
unwrap — ACL2::any-p

For now we formalize a file path as anything, which we wrap to keep things more abstract and separate. In the future we may refine this type with more structure. But note that, for instance, we could already use strings with slashes and such as file paths.

Subtopics

Filepath-fix
Fixing function for filepath structures.
Filepath-equiv
Basic equivalence relation for filepath structures.
Filepathp
Recognizer for filepath structures.
Make-filepath
Basic constructor macro for filepath structures.
Filepath->unwrap
Get the unwrap field from a filepath.
Change-filepath
Modifying constructor for filepath structures.