commit: 9698a4a883b5c44ef732e6dcadbdaed9f95859b9

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

Thu Jan 02 17:20:08 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jan 02 17:57:15 2025 -0800
tree: dfe97518c45c6d2f3a6453bf8bbd9b3600ad6648
parent: df9ed20385dec2f616533e6d61956b5e53ed3da2 [diff]

perf: avoid unnecessary assert/intro pairs in `grind`

This PR enhances the assertion of new facts in `grind` by avoiding the creation of unnecessary metavariables.

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

1 file changed

tree: dfe97518c45c6d2f3a6453bf8bbd9b3600ad6648

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).