lean4-htt/src/Std
Paul Reichert 89686fcd02
refactor: replace PRange shape α with Rcc α and eight other types (#10319)
This PR "monomorphizes" the structure `Std.PRange shape α`, replacing it
with nine distinct structures `Std.Rcc`, `Std.Rco`, `Std.Rci` etc., one
for each possible shape of a range's bounds. This change was necessary
because the shape polymorphism is detrimental to attempts of automation.

**BREAKING CHANGE:** While range/slice notation itself is unchanged,
this essentially breaks the entire remaining (polymorphic) range and
slice API except for the dot-notation(`toList`, `iter`, ...). It is not
possible to deprecate old declarations that were formulated in a
shape-polymorphic way that is not available anymore.
2025-10-02 06:45:11 +00:00
..
Data refactor: replace PRange shape α with Rcc α and eight other types (#10319) 2025-10-02 06:45:11 +00:00
Do refactor: replace PRange shape α with Rcc α and eight other types (#10319) 2025-10-02 06:45:11 +00:00
Internal chore: rename String.Pos to String.Pos.Raw (#10624) 2025-10-01 07:45:24 +00:00
Net refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Sat perf: shorten critical build path around String.Basic (#10614) 2025-09-29 19:45:21 +00:00
Sync perf: shorten critical build path around String.Basic (#10614) 2025-09-29 19:45:21 +00:00
Tactic perf: shorten critical build path around String.Basic (#10614) 2025-09-29 19:45:21 +00:00
Time perf: shorten critical build path around String.Basic (#10614) 2025-09-29 19:45:21 +00:00
Data.lean feat: add useful functions in Parsec, add error variant and Std.Data.ByteSlice (#9599) 2025-09-11 14:53:41 +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 feat: add Std.Notify type (#10368) 2025-09-24 03:35:08 +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