commit: fe7b96d8a0cf85e1ea81791ac9d673f84c9e866d

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Thu May 09 14:52:09 2024 +1000
committer: GitHub <noreply@github.com>

Thu May 09 04:52:09 2024 +0000
tree: c7d3e1f58de4fe1c811166985f0ed699b005df46
parent: ec872834655e55835e010347e9adacc85d7307f9 [diff]

fix: generate deprecation warnings for dot notation (#3969)

Fixes #3270 by moving the deprecation check from
`Lean.Elab.Term.mkConsts` to `Lean.Elab.Term.mkConst`, so
`Lean.Elab.Term.mkBaseProjections`, `.elabAppLValsAux`, `.elabAppFn`,
and `.elabForIn` also hit the check. Not all of these really need to hit
the check, so I'll run `!bench` to see if it's a problem.

6 files changed

tree: c7d3e1f58de4fe1c811166985f0ed699b005df46

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