Infer an optional parameter

In this file we define a tactic infer_param that closes a goal with default value by using this default value.

ink

def Mathlib.Tactic.inferOptParam : Lean.ParserDescr

Close a goal of the form optParam α a or autoParam α stx by using a.

Equations

• Mathlib.Tactic.inferOptParam = Lean.ParserDescr.node `Mathlib.Tactic.inferOptParam 1024 (Lean.ParserDescr.nonReservedSymbol "infer_param" false)