		Search-engine friendly clone of the ACL2 documentation.

Validator-states

Address+pos

Fixtype of pairs consisting of addresses and positive integers.

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

Fields

address — address
pos — posp

These pairs serve to record, in a validator state, which certificates have been endorsed but not received from the network yet. See the definition of validator states and of state transitions for details about the exact use of these pairs.

Subtopics

Address+pos-fix: Fixing function for address+pos structures.
Address+pos-equiv: Basic equivalence relation for address+pos structures.
Make-address+pos: Basic constructor macro for address+pos structures.
Change-address+pos: Modifying constructor for address+pos structures.
Address+pos->address: Get the address field from a address+pos.
Address+pos->pos: Get the pos field from a address+pos.
Address+posp: Recognizer for address+pos structures.