		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 by the validator, but not received from the network yet. See validator-state and the definition 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.
Address+pos->address: Get the address field from a address+pos.
Change-address+pos: Modifying constructor for address+pos structures.
Address+pos->pos: Get the pos field from a address+pos.
Address+pos-p: Recognizer for address+pos structures.