• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
              • Dynamic-semantics
                • Execution
                • Values
                • Dynamic-environments
                  • Call-dinfo
                  • Denv
                  • Update-var/const-dinfo-in-scope-list
                  • Update-var/const-dinfo-in-scope
                  • Var/const-dinfo
                  • Update-var/const-dinfo
                  • Add-var/const-dinfo-to-scope
                  • Add-var/const-dinfo
                  • Var/const-dinfo-option
                  • Get-var/const-dinfo-from-scope-list
                  • Denv-option
                  • Get-var/const-dinfo-from-scope
                  • Vcscope-dinfo-option
                  • Vcscope-dinfo-list-option
                  • Vcscope-dinfo
                  • Screens
                  • Get-var/const-dinfo
                  • Vcscope-dinfo-option-result
                  • Vcscope-dinfo-list-result
                  • Vcscope-dinfo-result
                  • Dynamic-struct-environments
                    • Struct-dinfo-option
                    • Add-struct-dinfo
                    • Struct-dinfo
                      • Struct-dinfo-fix
                      • Struct-dinfo-equiv
                      • Struct-dinfo->components
                      • Make-struct-dinfo
                      • Change-struct-dinfo
                      • Struct-dinfop
                    • Struct-denv-option
                    • Get-struct-dinfo
                    • Struct-denv
                    • Init-struct-denv
                  • Dynamic-function-environments
                  • Denv-result
                  • Init-denv
                  • Vcscope-dinfo-list
                  • Call-dinfo-list
                • Arithmetic-operations
                • Curve-parameterization
                • Shift-operations
                • Errors
                • Value-expressions
                • Locations
                • Input-execution
                • Edwards-bls12-generator
                • Equality-operations
                • Logical-operations
                • Program-execution
                • Ordering-operations
                • Bitwise-operations
                • Literal-evaluation
                • Type-maps-for-struct-components
                • Output-execution
                • Tuple-operations
                • Struct-operations
              • Compilation
              • Static-semantics
              • Concrete-syntax
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Dynamic-struct-environments

Struct-dinfo

Fixtype of dynamic information about struct types.

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

Fields
components — type-map

Currently this only consists of information about the components, organized as a type map from component names to their types. The finite map structure is adequate because components have unique names.

This dynamic information for struct types may be extended with information about associated constants and functions.

Subtopics

Struct-dinfo-fix
Fixing function for struct-dinfo structures.
Struct-dinfo-equiv
Basic equivalence relation for struct-dinfo structures.
Struct-dinfo->components
Get the components field from a struct-dinfo.
Make-struct-dinfo
Basic constructor macro for struct-dinfo structures.
Change-struct-dinfo
Modifying constructor for struct-dinfo structures.
Struct-dinfop
Recognizer for struct-dinfo structures.