• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • C
          • Syntax-for-tools
          • Atc
          • Transformation-tools
          • Language
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Types
              • Type
              • Type-name-list-to-type-list
              • Tyname-to-type
              • Member-type-list->name-list
              • Type-completep
              • Member-type
              • Member-type-add-first
              • Member-type-add-last
              • Init-type
                • Init-type-fix
                • Init-type-case
                • Init-type-equiv
                • Init-typep
                • Init-type-single
                • Init-type-list
                • Init-type-kind
              • Type-option
              • Member-type-lookup
              • Tyspecseq-to-type
              • Member-type-list-option
              • Type-promoted-arithmeticp
              • Type-list-result
              • Member-type-list-result
              • Integer-type-bits-nulfun
              • Init-type-result
              • Type-result
              • Type-nonchar-integerp
              • Type-nonchar-integer-listp
              • Type-arithmetic-listp
              • Type-integer-listp
              • Integer-type-xdoc-string
              • Type-unsigned-integerp
              • Type-signed-integerp
              • Integer-type-minbits
              • Integer-type-bits
              • Type-scalarp
              • Type-integerp
              • Type-arithmeticp
              • Type-realp
              • Type-list
              • *nonchar-integer-types*
              • Member-type-list
              • Ident-type-map
              • Type-set
              • Type-option-set
              • Symbol-type-alist
              • Type-option-list
            • Integer-formats-definitions
            • Computation-states
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Types

Init-type

Fixtype of initializer types.

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

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

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

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

Subtopics

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