search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

chore: remove nonterminal simps in UnionFind #868

Closed semorrison closed 2 months ago

semorrison commented 2 months ago

In today's attempt to adapt to changes in Lean https://github.com/leanprover/lean4/pull/4595 I ran into a broken proof in UnionFind, and discovered lots more non-terminal simps making it unnecessarily complicated to fix, so I've removed them all here, too.

semorrison commented 2 months ago

(I've merged this into lean-pr-testing-4595 already.)