Kyle Miller b863ca9ae9 chore: post-#7100 cleanup (#7196) ... This PR does some stage0 cleanup after #7100, and enables a warning when the old `structure S extends P : Type` syntax is used. It also updates the library to put resulting types in the new correct place (`structure S : Type extends P`). The `structure` elaborator also has some additional docstrings, and `StructFieldKind.fromParent` is renamed to `StructFieldKind.fromSubobject`.		2025-02-23 22:46:22 +00:00
..
Classes	chore: post-#7100 cleanup (#7196)	2025-02-23 22:46:22 +00:00
Data	feat: verify fold/for variants for Hashmaps (#7137)	2025-02-21 16:08:33 +00:00
Internal	chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162)	2025-02-20 12:05:09 +00:00
Net	feat: Std.Net.Addr (#6563)	2025-01-09 09:33:03 +00:00
Sat	chore: cleanup duplicate theorems (#7113)	2025-02-18 01:46:12 +00:00
Sync	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
Tactic	chore: use as[i] instead of as.get i	2025-02-19 08:48:33 +11:00
Time	chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162)	2025-02-20 12:05:09 +00:00
Classes.lean	feat: tree map data structures and operations (#6914)	2025-02-11 14:47:47 +00:00
Data.lean	feat: tree map data structures and operations (#6914)	2025-02-11 14:47:47 +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