Markus Himmel b28daa6d60 chore: rename String.endPos -> String.rawEndPos (#10853) ... This PR renames `String.endPos` to `String.rawEndPos`, as in a future release the name `String.endPos` will be taken by the function that is currently called `String.endValidPos`.		2025-10-21 11:25:30 +00:00
..
Tactic	chore: remove redundant imports in core (#10750)	2025-10-16 20:27:46 +00:00
Term	chore: cleanup and better docs for #10479 (#10504)	2025-09-23 09:02:07 +00:00
Attr.lean	chore: remove redundant imports in core (#10750)	2025-10-16 20:27:46 +00:00
Basic.lean	chore: rename String.endPos -> String.rawEndPos (#10853)	2025-10-21 11:25:30 +00:00
Command.lean	feat: expose optionValue parser (#10839)	2025-10-19 22:57:47 +00:00
Do.lean	chore: rename Stream to Std.Stream (#10645)	2025-10-02 15:25:56 +00:00
Extension.lean	chore: rename String.endPos -> String.rawEndPos (#10853)	2025-10-21 11:25:30 +00:00
Extra.lean	chore: remove redundant imports in core (#10750)	2025-10-16 20:27:46 +00:00
Level.lean	refactor: remove some unnecessary meta imports (#9542)	2025-07-25 15:14:02 +00:00
Module.lean	chore: remove redundant imports in core (#10750)	2025-10-16 20:27:46 +00:00
StrInterpolation.lean	chore: rename String.Pos to String.Pos.Raw (#10624)	2025-10-01 07:45:24 +00:00
Syntax.lean	feat: enable notationItem in "mixfix" notation commands (#10378)	2025-09-14 18:54:36 +00:00
Tactic.lean	refactor: module-ize Lean (#9330)	2025-07-25 12:02:51 +00:00
Term.lean	chore: rename String.endPos -> String.rawEndPos (#10853)	2025-10-21 11:25:30 +00:00
Types.lean	chore: rename String.endPos -> String.rawEndPos (#10853)	2025-10-21 11:25:30 +00:00