lean4-htt/src/Std
Vlad Tsyrklevich 7bd12c71c8
feat: add or/and/xor lemmas for BitVec/bv_normalize (#6872)
This PR adds lemmas for xor injectivity and when and/or/xor equal
allOnes or zero. Then I plumb support for the new lemmas through to
bv_normalize.
2025-01-31 13:27:43 +00:00
..
Data perf: improve elaboration performance of Std.Data.DHashMap.Internal.RawLemmas (#6814) 2025-01-28 11:04:42 +00:00
Internal feat: implement basic async IO with timers (#6505) 2025-01-13 18:11:04 +00:00
Net feat: Std.Net.Addr (#6563) 2025-01-09 09:33:03 +00:00
Sat perf: fast path for multiplication with constants in bv_decide (#6739) 2025-01-22 10:32:47 +00:00
Sync refactor: move IO.Channel and IO.Mutex to Std.Sync (#6282) 2024-12-03 09:36:50 +00:00
Tactic feat: add or/and/xor lemmas for BitVec/bv_normalize (#6872) 2025-01-31 13:27:43 +00:00
Time fix: negative timestamps and PlainDateTimes before 1970 (#6668) 2025-01-20 07:52:13 +00:00
Data.lean fix: unorphan modules in Std.Data (#4679) 2024-07-08 07:57:56 +00:00
Internal.lean feat: implement basic async IO with timers (#6505) 2025-01-13 18:11:04 +00:00
Net.lean feat: Std.Net.Addr (#6563) 2025-01-09 09:33:03 +00:00
Sat.lean feat: Std.Sat.AIG (#4953) 2024-08-12 14:58:38 +00:00
Sync.lean refactor: move IO.Channel and IO.Mutex to Std.Sync (#6282) 2024-12-03 09:36:50 +00:00
Tactic.lean chore: fix spelling mistakes in src/Std/ (#5431) 2024-09-23 20:39:34 +00:00
Time.lean feat: add date and time functionality (#4904) 2024-11-14 14:04:19 +00:00