commit: 106448a9af10dde5c697619a5e67896dd14dcfec

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

Sun Sep 20 19:46:59 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Sep 20 19:46:59 2026 +0000
tree: f776cebfc87b789146f54fdee2e4abfcfbc52461
parent: 2bdf77b753736bbe41269a41fe3bbaff93973cf1 [diff]

perf: skip local instance check for the new argument in `MatcherApp.addArg`

`updateAlts` introduced the new alternative argument with `forallBoundedTelescope`, which checks whether its type is a class. The argument is only abstracted, so the check is skipped.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

2 files changed

tree: f776cebfc87b789146f54fdee2e4abfcfbc52461

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.