Paul Reichert 1448493489 feat: improvements to Min/Max-related classes (#10024) ... This PR adds useful declarations to the `LawfulOrderMin/Max` and `LawfulOrderLeftLeaningMin/Max` API. In particular, it introduces `.leftLeaningOfLE` factories for `Min` and `Max`. It also renames `LawfulOrderMin/Max.of_le` to .of_le_min_iff` and `.of_max_le_iff` and introduces a second variant with different arguments.		2025-08-22 07:08:00 +00:00
..
Data	feat: improvements to Min/Max-related classes (#10024)	2025-08-22 07:08:00 +00:00
Do	fix: remove local Triple notation from SpecLemmas.lean to fix stage2 (#9967)	2025-08-18 16:41:26 +00:00
Internal	fix: background function and forIn (#9560)	2025-08-15 02:39:57 +00:00
Net	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Sat	feat: high-level order typeclasses (#9729)	2025-08-11 14:55:17 +00:00
Sync	chore: miscellaneous documentation typos (#10009)	2025-08-20 21:39:03 +00:00
Tactic	feat: change extended syntax for mvcgen invariants ... with ... (#9989)	2025-08-19 14:51:19 +00:00
Time	feat: integrate high-level order typeclasses with BEq and Ord (#9908)	2025-08-19 07:54:53 +00:00
Data.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Do.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Internal.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Net.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Sat.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Sync.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Tactic.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00
Time.lean	refactor: module-ize Std.Time (#9100)	2025-07-16 09:57:53 +00:00