Skip to content

refactor(Semantics/Degree): delete reducible duplicate names#567

Merged
github-actions[bot] merged 1 commit into
mainfrom
degree-delete-reducible
Jun 19, 2026
Merged

refactor(Semantics/Degree): delete reducible duplicate names#567
github-actions[bot] merged 1 commit into
mainfrom
degree-delete-reducible

Conversation

@hawkrobe

Copy link
Copy Markdown
Owner

Smallest-surface consolidation: delete named operations that are exactly a Comparison/posExt form (no aliasing, no bridges), consumers use the primitive directly.

  • matrixPredicate deleted (it was posExt); its two trivial Iff.rfl bridges deleted; isMaxDeg_posExt/posExt_downwardClosed restated on posExt.
  • positiveSem deleted (it was Comparison.ge.over); meetsThreshold_eq_positiveSemmeetsThreshold_eq_threshold (↔ θ ≤ cr a φ).
  • eqAt/compAt deleted; inlined at their granularity use sites.

@github-actions github-actions Bot enabled auto-merge (squash) June 19, 2026 23:29
@github-actions github-actions Bot merged commit f5b7e47 into main Jun 19, 2026
2 checks passed
@hawkrobe hawkrobe deleted the degree-delete-reducible branch June 19, 2026 23:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant