commit: bcf63093e6b07729b4887ae36c29d2bdc863489a

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

Wed Nov 26 04:41:27 2025 +0100
committer: Kim Morrison <kim@tqft.net>

Wed Nov 26 04:41:27 2025 +0100
tree: 004d81cbb637acf6e9174414d683a7c565b2539c
parent: 1d8fa1faf5e41bce0cb67aab16d82e36ec2d4793 [diff]

fix: update test to use public isGrindAnnotatedModule API

The test was accessing the private grindAnnotatedExt extension directly.
Updated to use the new public isGrindAnnotatedModule function instead.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

tests/lean/run/grind_annotated.lean[diff]

1 file changed

tree: 004d81cbb637acf6e9174414d683a7c565b2539c

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.