In a refinement error such as Expected: Positive(buffered) and Found: ∀buffered … Nat(buffered), the ∀buffered binder can be clicked to highlight its source. It looks like ordinary text: the existing dotted underline rule applies to .clickable, but the binder’s button does not have that class. Its tooltip shows the type rather than saying what a click does.
Give source-linked binders a persistent visual cue, such as a dotted underline or link icon, and an action label such as “Go to source.” Make the cue visible before hover and ensure clicking still reveals and highlights the source variable. The occurrences inside the predicates should either have the same source action or remain visually distinct from the clickable binder.
In a refinement error such as
Expected: Positive(buffered)andFound: ∀buffered … Nat(buffered), the∀bufferedbinder can be clicked to highlight its source. It looks like ordinary text: the existing dotted underline rule applies to.clickable, but the binder’s button does not have that class. Its tooltip shows the type rather than saying what a click does.Give source-linked binders a persistent visual cue, such as a dotted underline or link icon, and an action label such as “Go to source.” Make the cue visible before hover and ensure clicking still reveals and highlights the source variable. The occurrences inside the predicates should either have the same source action or remain visually distinct from the clickable binder.