lean4-htt/src/Init/Data/String
David Thrane Christiansen 82932ec86a
feat: add stop position to parser (#10057)
This PR adds a stop position field to parser input contexts, allowing
the parser to be instructed to stop parsing prior to the end of a file.

This is step 1, prior to a stage0 update, to make run-time data
structures sufficiently compatible to avoid segfaults. After the update,
the actual code to stop parsing can be merged.
2025-08-22 17:04:04 +00:00
..
Basic.lean feat: add stop position to parser (#10057) 2025-08-22 17:04:04 +00:00
Extra.lean chore: avoid confusing public import all combination (#10051) 2025-08-22 12:04:42 +00:00
Lemmas.lean feat: high-level order typeclasses (#9729) 2025-08-11 14:55:17 +00:00