commit: 5c354050523bcffd30201fb30e0568004552b423

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

Sun Nov 09 23:01:45 2025 +0100
committer: Kim Morrison <kim@tqft.net>

Mon Nov 10 00:14:04 2025 +0100
tree: d5351ce9cebbe29c64491758b45a11a52112a223
parent: 80409a9ceb803bdfa695687de3aca2008c5aaf6d [diff]

chore: add failing test for diamond structure docstrings

tests/pkg/structure_docstrings/StructureDocstrings.lean[Added - diff]
tests/pkg/structure_docstrings/StructureDocstrings/A.lean[Added - diff]
tests/pkg/structure_docstrings/StructureDocstrings/B.lean[Added - diff]
tests/pkg/structure_docstrings/lakefile.toml[Added - diff]
tests/pkg/structure_docstrings/lean-toolchain[Added - diff]
tests/pkg/structure_docstrings/test.sh[Added - diff]

6 files changed

tree: d5351ce9cebbe29c64491758b45a11a52112a223

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.