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.
Mathlib.Tactic.InferParam
In this file we define a tactic infer_param
that closes a goal with default value by using
this default value.