letin
Prev Chapter 7. Tactics Next

letin

letin x ≝ t

Synopsis:

letin id ≝ sterm

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.

Prev Up Next
lapply Home normalize