commit: 72e552875870310d9dbdc807700be8292150b982

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

Mon Jun 10 15:01:03 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Jun 10 15:01:03 2024 -0700
tree: c1b5a7465bfc64d465f1e194960b00182a918673
parent: fb01c650c25b9eb3b1effa46c9912378dce6c9ef [diff]

fix: improve `typeOccursCheck`

This commit addresses a Mathlib failure.

src/Lean/Meta/ExprDefEq.lean[diff]
tests/lean/run/typeOccursCheckIssue.lean[Added - diff]

2 files changed

tree: c1b5a7465bfc64d465f1e194960b00182a918673

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