commit: e8d6e2242ba2ccf9ecaba2abbbd725f7e220b313

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

Sun Mar 16 09:42:16 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Mar 16 09:42:16 2025 -0700
tree: 02d4fefe74540273f99ff010acb598601e04be08
parent: 6f16a535f83838cc6ff196abb33b70799482aa0a [diff]

feat: exfalso in `grind`

This PR ensures that `grind` can be used as a more powerful `contradiction` tactic, sparing the user from having to type `exfalso; grind` or `intros; exfalso; grind`.

5 files changed

tree: 02d4fefe74540273f99ff010acb598601e04be08

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