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

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

Closed leodemoura closed 6 days ago

leodemoura commented 6 days ago

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

leanprover-community-bot commented 6 days ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6129 has successfully built against this PR. (2024-11-19 21:31:04) View Log