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, on a goal which is an inductive type, solves it by applying the first matching constructor, creating new goals for all arguments to the constructor in the same order. This is like constructor except the goals are not reordered.

Equations

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

def tacticEconstructor : Lean.ParserDescr

econstructor, on a goal which is an inductive type, solves it by applying the first matching constructor, creating new goals for non-dependent arguments to the constructor in the same order. This is like constructor except only non-dependent arguments are shown as new goals.

Equations

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