commit: 71568b2cf3e8fe4cdd0c4802ee41b001b5bf64a7

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

Wed Apr 08 10:58:23 2026 +1000
committer: Kim Morrison <kim@tqft.net>

Wed Apr 08 10:58:23 2026 +1000
tree: 9da78bd827d56ff9fb699037f6ce6d1e89bd200c
parent: 6eb6a364b12c7a0ca710aa5ac9fa9a38f765c618 [diff]

fix: skip implicit_reducible for Prop-valued delta-derived instances

Address review feedback: skip setting `@[implicit_reducible]` on
Prop-valued instances (theorems), matching the behavior of the
handwritten `instance` command in `MutualDef.lean`.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

3 files changed

tree: 9da78bd827d56ff9fb699037f6ce6d1e89bd200c

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.