		Search-engine friendly clone of the ACL2 documentation.

Validator-states

Timer

Fixtype of timer states.

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

Member Tags → Types

:running → timer-running
:expired → timer-expired

Our model does not represent real time, but it represents the state of timers, which may be either running or expired. Each validator has such a timer: see validator-state.

Subtopics

Timer-case: Case macro for the different kinds of timer structures.
Timer-fix: Fixing function for timer structures.
Timer-equiv: Basic equivalence relation for timer structures.
Timerp: Recognizer for timer structures.
Timer-running
Timer-expired
Timer-kind: Get the kind (tag) of a timer structure.