Documentation

Mathlib.Tactic.Constructor

The fconstructor and econstructor tactics #

The fconstructor and econstructor tactics are variants of the constructor tactic in Lean core, except that

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.

    Equations
    Instances For