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 goals
• econstructor adds only non-dependent premises as new goals.

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

• tacticFconstructor = Lean.ParserDescr.node `tacticFconstructor 1024 (Lean.ParserDescr.nonReservedSymbol "fconstructor" false)

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

• tacticEconstructor = Lean.ParserDescr.node `tacticEconstructor 1024 (Lean.ParserDescr.nonReservedSymbol "econstructor" false)