ink

def tacticReduceGoal : Lean.ParserDescr

A tactic to reduce the main goal, up to definitional equality.

Equations

• tacticReduceGoal = Lean.ParserDescr.node `tacticReduceGoal 1024 (Lean.ParserDescr.nonReservedSymbol "reduceGoal" false)