<diamond-command> ::= <> <character>* <box-command> ::=  <character>*
<> induction step  induction step
LP checks <>'s and 's when it executes commands from a .lp file and the box-checking setting is on. Whenever it generates a <> or a , LP checks that the next nonblank line in the .lp file contains a corresponding <> or  command. The special LP prompts <>? and ? indicate that LP expects a confirming <> or  in the .lp file. LP prints an error message if the confirming <> or  is missing, or if an unexpected <> or  appears in the .lp file.
Regardless of whether box-checking is on or off, LP does not copy <> and  commands from its input to the history or to a script file. Instead, it puts into the history and script file the <> and  commands that it produces as it creates and discharges subgoals. Thus, the history and the script file will be annotated in a way that correctly reflects the actual progress of the proof.
See also the qed command.