• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
        • Atc
        • Syntax-for-tools
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • 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
            • 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-integer-listp
            • Type-nonchar-integerp
            • Type-integer-listp
            • Type-arithmetic-listp
            • Integer-type-xdoc-string
            • Integer-type-minbits
            • Type-unsigned-integerp
            • Type-signed-integerp
            • Integer-type-bits
            • Type-integerp
            • Type-arithmeticp
            • Type-scalarp
            • Type-realp
            • Type-list
            • *nonchar-integer-types*
            • Member-type-list
            • Type-set
            • Type-option-set
            • Symbol-type-alist
            • Type-option-list
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Implementation-environments
          • 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
        • Pack
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Types

Member-type-lookup

Look up a member by name in a list of member types.

Signature

(member-type-lookup name members) → type

Arguments

name — Guard (identp name).

members — Guard (member-type-listp members).

Returns

type — Type (type-optionp type).

We search from the beginning and stop at the first hit; since the names are unique in well-formed lists, the exact search strategy makes no difference We return the type of the member if the search is successful. We return nil if the search is unsuccessful.

Definitions and Theorems

Function: member-type-lookup

(defun member-type-lookup (name members)
  (declare (xargs :guard (and (identp name)
                              (member-type-listp members))))
  (let ((__function__ 'member-type-lookup))
    (declare (ignorable __function__))
    (b* (((when (endp members)) nil)
         ((when (equal (ident-fix name)
                       (member-type->name (car members))))
          (member-type->type (car members))))
      (member-type-lookup name (cdr members)))))

Theorem: type-optionp-of-member-type-lookup

(defthm type-optionp-of-member-type-lookup
  (b* ((type (member-type-lookup name members)))
    (type-optionp type))
  :rule-classes :rewrite)

Theorem: member-type-lookup-of-ident-fix-name

(defthm member-type-lookup-of-ident-fix-name
  (equal (member-type-lookup (ident-fix name)
                             members)
         (member-type-lookup name members)))

Theorem: member-type-lookup-ident-equiv-congruence-on-name

(defthm member-type-lookup-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (member-type-lookup name members)
                  (member-type-lookup name-equiv members)))
  :rule-classes :congruence)

Theorem: member-type-lookup-of-member-type-list-fix-members

(defthm member-type-lookup-of-member-type-list-fix-members
  (equal (member-type-lookup name (member-type-list-fix members))
         (member-type-lookup name members)))

Theorem: member-type-lookup-member-type-list-equiv-congruence-on-members

(defthm
    member-type-lookup-member-type-list-equiv-congruence-on-members
  (implies (member-type-list-equiv members members-equiv)
           (equal (member-type-lookup name members)
                  (member-type-lookup name members-equiv)))
  :rule-classes :congruence)