commit: 3b6e65dcae21db4c46076c7a92dccbe195abc929

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

Sun Mar 01 14:28:02 2026 -0800
committer: Kim Morrison <kim@tqft.net>

Wed Mar 04 23:38:31 2026 +0000
tree: fb685ff62a68d5c7d84c602008fe5cc3b9a5820e
parent: f3752861c934c277630cc0dc5a812bbcc8b6f3a3 [diff]

fix: mark `Id.run` as `[implicit_reducible]`

This PR marks `Id.run` as `[implicit_reducible]` to ensure that
`Id.instMonadLiftTOfPure` and `instMonadLiftT Id` are definitionally
equal when using `.implicitReducible` transparency setting.

2 files changed

tree: fb685ff62a68d5c7d84c602008fe5cc3b9a5820e

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.