ink

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)

ink

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)