commit: 6c17ad8954ccbd1211829ffa39397d635e92aeff

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Tue Jun 03 11:49:36 2025 +1000
committer: GitHub <noreply@github.com>

Tue Jun 03 01:49:36 2025 +0000
tree: c772520ee701c01e2aff6530c99f9744ab5e5723
parent: 3452a8a2e5744b9efb4ed1a4877e2bc0b169e210 [diff]

chore: add failing grind test (#8599)

`@[grind local]` currently doesn't work as expected on theorems in
namespaces.

tests/lean/grind/grind_local_namespace.lean[Added - diff]

1 file changed

tree: c772520ee701c01e2aff6530c99f9744ab5e5723

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.