commit: ac6ea18cc6802c94a4e2a9eef903d11d3182e82d

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

Sat Dec 14 15:57:19 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Dec 14 15:59:56 2024 -0800
tree: 01c599ed8a68458f1e36bdc42ca674b2d4ad062e
parent: b721c0f54041f6a6adc618c07851a7e0414bd1e4 [diff]

fix: type incorrect term produced by `contradiction`

This PR fixes a type error in the proof generated by the `contradiction` tactic.

closes #4851

src/Lean/Meta/Tactic/Contradiction.lean[diff]
tests/lean/run/4851.lean[Added - diff]

2 files changed

tree: 01c599ed8a68458f1e36bdc42ca674b2d4ad062e

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