letin id ≝ sterm
Prev
Chapter 6. Tactics
Next
letin
id
≝
sterm
letin x ≝ t
Pre-conditions:
None.
Action:
It adds to the context of the current sequent to prove a new definition
x ≝ t
.
New sequents to prove:
None.