Commit 2026-02-09 08:58 201ee8da

View on Github →

chore(style): remove duplicate instance hypotheses (#35002) This PR removes simple duplicate instance hypotheses which appear in the local context. This is a stylistic change; this PR does not modify the types of definitions. The deletions and variable movements here are restricted to simple cases; fixes that require more restructuring are split off into other PRs. This is motivated by the upcoming overlapping instances linter, which fires on duplicate instances in the local context (even if these do not appear in the resulting definition's type). See also this Zulip thread for discussion on removing duplicate instances.

Estimated changes