commit: 39aab4433667c4d68a285fb06945997a5d32ae3f

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

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

Tue Mar 03 03:00:57 2026 +0000
tree: fb409b38bfb9e28bbac34261688efab04c76bcd5
parent: 8f30efba2d1a5415190f0778ae586f9373bd8836 [diff]

fix: use explicit `ReaderT.run` to avoid accidental recursion

`self.run` where `self : MonitorM α` resolves to `MonitorM.run`
(a recursive call) instead of `ReaderT.run`, because `MonitorM`
is an abbrev and the locally-defined `MonitorM.run` takes priority
in dot notation.

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

src/lake/Lake/Build/Run.lean[diff]

1 file changed

tree: fb409b38bfb9e28bbac34261688efab04c76bcd5

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.