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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.getGoalPrefix mvarDecl = if (Lean.isLHSGoal? mvarDecl.type).isSome = true then "| " else "⊢ "
Instances For
Equations
- One or more equations did not get rendered due to their size.