commit: 5142a76abb7e65483ea182ab69b9049a50c40535

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

Mon Jul 14 12:47:51 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Jul 14 12:50:01 2025 -0700
tree: 6af949fba8829a60c63bc92a057c77997d93748f
parent: cfb13b16890276eeb916998436f2760bca032e31 [diff]

perf: minimize use of `inferType` at `markNestedSubsingleton` in `grind`

This PR minimizes the number of times `inferType` has to be used in
the `grind` preprocessing step: `markNestedSubsingleton`.

src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean[diff]

1 file changed

tree: 6af949fba8829a60c63bc92a057c77997d93748f

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.