commit: 5cf36e81de04711cedd6d67bb3580c6546a22860

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

Tue Feb 25 15:06:42 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Feb 25 15:06:42 2025 -0800
tree: 2327a4acf496d629cf2f0b07babbdadc02879ddd
parent: b2bc1e1ecafdcdd09e7d7299cadf0b838ce7940d [diff]

feat: add `diseq` APIs to grind

This PR implements functions for constructing disequality proofs in `grind`.

src/Init/Grind/Lemmas.lean[diff]
src/Lean/Meta/Tactic/Grind.lean[diff]
src/Lean/Meta/Tactic/Grind/Diseq.lean[Added - diff]
src/Lean/Meta/Tactic/Grind/Types.lean[diff]
tests/lean/run/grind_diseq_api.lean[Added - diff]

5 files changed

tree: 2327a4acf496d629cf2f0b07babbdadc02879ddd

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