lean4-htt/src/Init/Data/Range
Paul Reichert e86e978f26
feat: ToStream instance for ranges (#9058)
This PR provides a `ToStream` instance for slices so that they can be
used in `for i in xs, j in ys do` notation.
2025-06-28 09:38:37 +00:00
..
Polymorphic feat: ToStream instance for ranges (#9058) 2025-06-28 09:38:37 +00:00
Basic.lean chore: cleanup after renaming get_elem_tactic_trivial 2025-06-06 13:10:18 +10:00
Lemmas.lean feat: do not export def bodies by default (#8221) 2025-05-15 12:16:54 +00:00
Polymorphic.lean feat: ToStream instance for ranges (#9058) 2025-06-28 09:38:37 +00:00