lean4-htt/src/Std
Tobias Grosser c5b82e0b16
feat: BitVec.[toFin|getMsbD]_setWidth and [getMsbD|msb]_signExtend (#6338)
This PR adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.

Also correct renamed the misnamed theorem for
`signExtend_eq_setWidth_of_msb_false`.

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>
2024-12-10 01:17:20 +00:00
..
Data chore: cleanup of Array lemmas (#6337) 2024-12-08 22:03:23 +00:00
Internal feat: add date and time functionality (#4904) 2024-11-14 14:04:19 +00:00
Sat feat: change Array.set to take a Nat and a tactic provided bound (#5988) 2024-11-11 07:53:24 +00:00
Sync refactor: move IO.Channel and IO.Mutex to Std.Sync (#6282) 2024-12-03 09:36:50 +00:00
Tactic feat: BitVec.[toFin|getMsbD]_setWidth and [getMsbD|msb]_signExtend (#6338) 2024-12-10 01:17:20 +00:00
Time chore: remove unused imports (#6305) 2024-12-04 12:46:08 +00:00
Data.lean fix: unorphan modules in Std.Data (#4679) 2024-07-08 07:57:56 +00:00
Internal.lean chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115) 2024-08-21 15:26:17 +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