commit: bf73a26d6a16c24bd9e0252283120e897e929667

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

Thu Jul 18 11:51:47 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jul 18 11:51:47 2024 -0700
tree: 4ed123d498d1b6beda2e367415c596c76784c72d
parent: a94805ff71f7576ee014aafc76b29e29b066bd80 [diff]

chore: `Simp.Config.implicitDefEqProofs := true` by default

Motivation: unblock PR #4595
`Simp.Config.implicitDefEqProofs := false` is currently creating too
many issues in Mathlib.

src/Init/MetaTypes.lean[diff]

1 file changed

tree: 4ed123d498d1b6beda2e367415c596c76784c72d

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