commit: be5db4c3ecb5c0ae172cfc0a834e386b947801d5

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

Tue Nov 19 12:04:13 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Nov 19 12:04:13 2024 -0800
tree: 4680b8ef35f82768d463d4df9d0ead996bca0ce3
parent: 4600bb16fcded0356d20ae232e7f8580c56a5955 [diff]

fix: `isDefEq` when `zetaDelta := false`

This PR fixes a bug at `isDefEq` when `zetaDelta := false`.
See new test for a small example that exposes the issue.

3 files changed

tree: 4680b8ef35f82768d463d4df9d0ead996bca0ce3

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