lean4-htt/src/Std
Henrik Böving 88f17dee71
perf: tune the behavior of and flattening in bv_decide (#11781)
This PR improves the performance of and flattening in `bv_decide`.

The two main insights of this PR are:
1. When embedded constraint substitution is disabled it makes no sense
to have and flattening on in
   the first place, given that we do not profit from it in any way.
2. The new fvars produced by and flattening can also be inserted into
the rewriting caches of the
preprocessing pipeline if the fvar they were derived from is already in
the cache. This
drastically decreases the amount of work we have to do in the second
rewriting pass after running
   and flattening.
2025-12-23 13:08:31 +00:00
..
Data refactor: remove IteratorCollect (#11706) 2025-12-17 23:02:33 +00:00
Do refactor: move Std.Range to Std.Legacy.Range (#11438) 2025-12-18 02:07:33 +00:00
Internal feat: introduce CancellationContext type for cancellation with context propagation (#11499) 2025-12-15 21:20:11 +00:00
Net refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Sat feat: dedicated fix operator for well-founded recursion on Nat (#7965) 2025-12-01 12:51:55 +00:00
Sync feat: introduce CancellationContext type for cancellation with context propagation (#11499) 2025-12-15 21:20:11 +00:00
Tactic perf: tune the behavior of and flattening in bv_decide (#11781) 2025-12-23 13:08:31 +00:00
Time doc: correct typos in documentation and comments (#11465) 2025-12-02 06:38:05 +00:00
Data.lean feat: add decidable equality to DHashMap/HashMap/HashSet and their extensional variants (#11421) 2025-12-12 09:55:55 +00:00
Do.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Internal.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Net.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Sat.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Sync.lean feat: introduce CancellationContext type for cancellation with context propagation (#11499) 2025-12-15 21:20:11 +00:00
Tactic.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Time.lean doc: correct typos in documentation and comments (#11465) 2025-12-02 06:38:05 +00:00