The fconstructor
and econstructor
tactics #
The fconstructor
and econstructor
tactics are variants of the constructor
tactic in Lean core,
except that
fconstructor
does not reorder goalseconstructor
adds only non-dependent premises as new goals.
fconstructor
is like constructor
(it calls apply
using the first matching constructor of an inductive datatype)
except that it does not reorder goals.
Equations
Instances For
econstructor
is like constructor
(it calls apply
using the first matching constructor of an inductive datatype)
except only non-dependent premises are added as new goals.