Documentation

Mathlib.Tactic.Constructor

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