Changelog

leanprover/lean4 · · 2 commits

Lean docstrings now handle macro-generated text

Verso docstrings can now be elaborated from raw text when source positions are missing, fixing parameter references in more cases.

david-christiansen Garmelon

Fix Verso parameter references in more docstring forms (david-christiansen45e668d)

Lean’s Verso docstring elaboration now handles unbracketed binders, _ parameters, and macro-generated declarations more reliably. The change adds fallback parsing/elaboration paths for plain text and position-stripped docstrings, so parameter references resolve correctly even when source positions or interactive metadata are unavailable.

Other misc changes

  • CI workflow references updated for a downstream action rename (Garmelon6b941e7).