commit: dd1303b64ca6aa98ae620e10b4ddde26db2afc25

[log]
author: Kim Morrison <kim@tqft.net>

Wed Mar 25 12:52:20 2026 +1100
committer: Kim Morrison <kim@tqft.net>

Wed Mar 25 12:52:20 2026 +1100
tree: e22b1f81a51da9094809e3ac314681739cb7f806
parent: 57f13c89f253b0642073ea029c43643df2eae2bd [diff]

fix: update Reparen golden file for inferInstanceAs docstring change

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

tests/elab/Reparen.lean.out.expected[diff]

1 file changed

tree: e22b1f81a51da9094809e3ac314681739cb7f806

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.