Matita Home
reduce <pattern>
Prev
Chapter 6. Tactics
Next
reduce <pattern>
reduce patt
Pre-conditions:
None.
Action:
It replaces all the terms matched by
patt
with their βδιζ-normal form.
New sequents to prove:
None.