• 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
          • Atc
          • Language
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
              • Pointer
              • Member-types-of-member-values
              • Member-value-list->value-list
              • Member-value-list->name-list
              • Expr-value
              • Type-list-of-value-list
              • Type-of-value
              • Value-option
              • Init-value
                • Init-value-case
                • Init-value-fix
                • Init-value-equiv
                • Init-valuep
                • Init-value-single
                • Init-value-list
                • Init-value-kind
              • Value-result
              • Type-of-value-option
              • Value-list-result
              • Member-value-list-result
              • Init-value-result
              • Expr-value-result
              • Value-option-result
              • Signed/unsigned-byte-p-of-integer-values
              • Member-type-of-member-value
              • Bounds-of-integer-values
              • Value-promoted-arithmeticp
              • Init-type-of-init-value
              • Value-unsigned-integerp
              • Value-signed-integerp
              • Value-integerp
              • Value-arithmeticp
              • Value-scalarp
              • Value-realp
              • Values/membervalues
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • 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
  • Values

Init-value

Fixtype of initializer values.

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

Member Tags → Types
:single → init-value-single
:list → init-value-list

We introduce a notion of values for initializers. An initializer value has the same structure as an initializer, but expressions are replaced with (their) values.

As our model of initializers is extended, out model of initializer values will be extended accordingly.

Subtopics

Init-value-case
Case macro for the different kinds of init-value structures.
Init-value-fix
Fixing function for init-value structures.
Init-value-equiv
Basic equivalence relation for init-value structures.
Init-valuep
Recognizer for init-value structures.
Init-value-single
Init-value-list
Init-value-kind
Get the kind (tag) of a init-value structure.