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.

def Mathlib.Tactic.inferOptParam : Lean.ParserDescr

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