Given the current values of the options pp.showLetValues
and pp.showLetValues.threshold
,
determines whether the local let declaration's value should be omitted.
tactic
is whether the goal is for a tactic metavariable. In that case, uses the maximum ofpp.showLetValues.tactic.threshold
andpp.showLetValues.threshold
for the threshold. In tactics, we usually want to see let values. In contrast, for the "expected type" view we usually do not.