# 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.

source
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)

Instances For