commit: 9c8cb61b5ca174cd47c40fb786c84e91a24e3303

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Thu Aug 21 14:50:41 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Aug 21 14:50:41 2025 -0700
tree: e26aa2c729eecdbe82da226ae97b2ce29a6b92fb
parent: ca4322ff09910aa33c4f7d99aee36a7252219797 [diff]

chore: add `module` keyword to `grind` tests

This PR also fixes missing `@[expose]` in grind support definitions.

236 files changed

tree: e26aa2c729eecdbe82da226ae97b2ce29a6b92fb

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.