commit: fe184b41b010673645fbbd73dfc0411f71361b35

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

Wed Jul 16 20:54:48 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Jul 16 20:59:01 2025 -0700
tree: 7d92bef01d64eea4acb2942b435e1e2321bd10a4
parent: d6675225243ba5205bcd46eced5926b027a39869 [diff]

perf: `isArrowProposition`

This PR increases the number of cases where `isArrowProposition`
returns a result other than `.undef`. This function is used
to implement the `isProof` predicate, which is invoked on
every subterm visited by `simp`.

src/Lean/Meta/InferType.lean[diff]

1 file changed

tree: 7d92bef01d64eea4acb2942b435e1e2321bd10a4

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.