max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/DocString
History
David Thrane Christiansen ceb86b1293
fix: details in Markdown rendering of Verso docstrings (#11151) 
This PR fixes some details in the Markdown renderings of Verso
docstrings, and adds tests to keep them correct. Also adds tests for
Verso docstring metadata.
2025-11-13 05:19:30 +00:00
..
Add.lean chore: rename String.endPos -> String.rawEndPos (#10853) 2025-10-21 11:25:30 +00:00
Extension.lean chore: more reorganization of strings (#10928) 2025-10-23 11:56:11 +00:00
Formatter.lean refactor: rename String.split to String.splitToList (#10822) 2025-10-18 12:12:54 +00:00
Links.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Markdown.lean fix: details in Markdown rendering of Verso docstrings (#11151) 2025-11-13 05:19:30 +00:00
Parser.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Syntax.lean feat: improvements to Verso docstrings (#10479) 2025-09-20 22:05:57 +00:00
Types.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00