lean4-htt/src/Init/Data/BitVec
Sebastian Ullrich f4a0259344
chore: cleanups uncovered by Shake (#10572)
* Wrap proof subterms in `by exact` so dependencies can be demoted to
private `import`s
* Remove trivial instance re-definitions that may cause name collisions
on import changes
* Remove unused `open`s that may fail on import removals
2025-09-26 14:38:30 +00:00
..
Basic.lean chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00
BasicAux.lean chore: move String.utf8EncodeChar to the prelude (#10264) 2025-09-07 12:42:53 +00:00
Bitblast.lean feat: add fast circuit for unsigned multiplication overflow detection fastUmulOverflow_eq and surrounding definitions (#7858) 2025-08-26 13:21:23 +00:00
Bootstrap.lean chore: use [grind =] (#10337) 2025-09-11 03:21:37 +00:00
Decidable.lean chore: cleanups uncovered by Shake (#10572) 2025-09-26 14:38:30 +00:00
Folds.lean chore: avoid confusing public import all combination (#10051) 2025-08-22 12:04:42 +00:00
Lemmas.lean chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00