89686fcd02
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. |
||
|---|---|---|
| .. | ||
| Combinators | ||
| Consumers | ||
| Internal | ||
| Lemmas | ||
| Basic.lean | ||
| Combinators.lean | ||
| Consumers.lean | ||
| Internal.lean | ||
| Lemmas.lean | ||
| PostconditionMonad.lean | ||
| ToIterator.lean | ||