• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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-add-last

Add a member at the end of a list of member types.

Signature

(member-type-add-last name type members) → new-members

Arguments

name — Guard (identp name).

type — Guard (typep type).

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

Returns

new-members — Type (member-type-list-optionp new-members).

We check that a member with the same name is not already in the list, to maintain the well-formedness of the list.

Definitions and Theorems

Function: member-type-add-last

(defun member-type-add-last (name type members)
  (declare (xargs :guard (and (identp name)
                              (typep type)
                              (member-type-listp members))))
  (let ((__function__ 'member-type-add-last))
    (declare (ignorable __function__))
    (b* ((found (member-type-lookup name members))
         ((when found)
          (member-type-list-option-none)))
      (member-type-list-option-some
           (rcons (make-member-type :name name :type type)
                  members)))))

Theorem: member-type-list-optionp-of-member-type-add-last

(defthm member-type-list-optionp-of-member-type-add-last
  (b* ((new-members (member-type-add-last name type members)))
    (member-type-list-optionp new-members))
  :rule-classes :rewrite)

Theorem: member-type-add-last-of-ident-fix-name

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

Theorem: member-type-add-last-ident-equiv-congruence-on-name

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

Theorem: member-type-add-last-of-type-fix-type

(defthm member-type-add-last-of-type-fix-type
  (equal (member-type-add-last name (type-fix type)
                               members)
         (member-type-add-last name type members)))

Theorem: member-type-add-last-type-equiv-congruence-on-type

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

Theorem: member-type-add-last-of-member-type-list-fix-members

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

Theorem: member-type-add-last-member-type-list-equiv-congruence-on-members

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