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

source
def tacticFconstructor :
Lean.ParserDescr

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
      source
      def tacticEconstructor :
      Lean.ParserDescr

      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