leanprover / verso

Lean documentation authoring tool
Apache License 2.0
125 stars 14 forks source link

feat: working example definition link targets #222

Closed david-christiansen closed 3 weeks ago

david-christiansen commented 3 weeks ago

Code samples can now detect defined names and generate links to them, just as there were previously links to docstrings from code samples. This will help make the Markdown docstrings render usefully in the manual genre.