commit: 126b1d56ecf246e8fb6b7d883419f6758c65e3c3

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

Tue Mar 03 00:30:52 2026 +0000
committer: Kim Morrison <kim@tqft.net>

Tue Mar 03 00:30:52 2026 +0000
tree: 022281840126c98a04b1314f1ff14f061d2ec525
parent: 145a12104887190a20b016f81c73810b25da3e91 [diff]

chore: add HACK banner to isNonTrivialRegular transparency check

This PR adds a HACK comment to the transparency restriction in
`isNonTrivialRegular` so it's not forgotten. Per Sebastian's request
on Zulip.

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

src/Lean/Meta/ExprDefEq.lean[diff]

1 file changed

tree: 022281840126c98a04b1314f1ff14f061d2ec525

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.