LET is a top-level command.
Bind a variable to a term.
The command format for LET is:

 <n>LET   P5   P4   H3   D2     D1      A      x      C     P5-HYPS    P4-HYPS    H3-HYPS    D2-HYPS    D1-HYPS 

The arguments have the following meaning:
P5 : Plan Line
P4 : New Plan Line
H3 : Line where variable is chosen
D2 : Auxiliary existential line
D1 : Auxiliary line with reflexivity
A : Term
x : Variable
C :
P5-HYPS : Hypotheses
P4-HYPS : Hypotheses
H3-HYPS : Hypotheses
D2-HYPS : Hypotheses
D1-HYPS : Hypotheses

ETPS documentation homepage


LET is an inference rule.
Its priority is NIL

ETPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage