		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Command

Fixtype of commands.

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

Member Tags → Types

:increment → command-increment
:decrement → command-decrement
:instruction → command-instruction

There are currently three kinds of commands: increments, decrements, and instructions. Note that, as in the grammar, finalization commands are separate.

Subtopics

Command-fix: Fixing function for command structures.
Command-case: Case macro for the different kinds of command structures.
Command-equiv: Basic equivalence relation for command structures.
Commandp: Recognizer for command structures.
Command-increment
Command-decrement
Command-instruction
Command-kind: Get the kind (tag) of a command structure.