commit: 5ac0662886f731170124abb29c113a0595a6a17d

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

Fri May 10 14:19:20 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Fri May 10 14:38:42 2024 -0700
tree: f5feddcf9a8739d993e1643b512436be014f063b
parent: fe7b96d8a0cf85e1ea81791ac9d673f84c9e866d [diff]

fix: add `checkSystem` and `withIncRecDepth` to `withAutoBoundImplicit`

Fix stack overflow crash.

Closes #4117

The fix can be improved: we could try to avoid creating hundreds of
auto implicits before failing.

src/Lean/Elab/Term.lean[diff]
tests/lean/4117.lean[Added - diff]
tests/lean/4117.lean.expected.out[Added - diff]
tests/lean/run/simpDiag.lean[diff]

4 files changed

tree: f5feddcf9a8739d993e1643b512436be014f063b

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 (documentation source: doc/make/index.md).