|
|
|---|
|
|
|
|---|
Forms you type at the top-level, but...
...the word ``command'' usually refers to a top-level form whose evaluation produces a new logical world.
Typical commands are: (defun foo (x) (cons x x)) (defthm consp-foo (consp (foo x))) (defrec pair (hd . tl) nil)
The first two forms are examples of commands that are in fact primitive
events. See events.
Both events and commands leave landmarks on the world that enable us to determine how the given world was created from the previous one. Most of your interactions will occur at the command level, i.e., you type commands, you print previous commands, and you undo back through commands. Commands are denoted by command descriptors. See command-descriptor.