Leonardo de Moura

feat: add `simp` configuration option `Simp.Config.instances`

5

Depends on #3124 Mathlib adaptation PR is at https://github.com/leanprover-community/mathlib4/pull/9572

fix: `rw` argument elaboration

21

- `rw [id]` is now elaborated as `rw [@id]` - Add `Rewrite.Config.newGoals` field for specifying how new `rw` goals are ordered. We use the same approach used in the `apply`...

fix: type class issues with `maxSynthPendingDepth := 1`

1

Summary: - Take `synthPendingDepth` into account when caching TC results - Add `maxSynthPendingDepth` option with default := 2. - Add support for tracking `synthPending` failures when using `set_option diagnostics true`...

fix: take `synthPendingDepth` into account when caching TC results

1

@semorrison This is for debugging purposes only. It contains only the TC cache fix. If #4119 does not fix the performance issues in Mathlib. We can use this one to...

fix: type class issues

2

Summary: - Take `synthPendingDepth` into account when caching TC results - Add `maxSynthPendingDepth` option with default := 2. - Add support for tracking `synthPending` failures when using `set_option diagnostics true`...

fix: do not include internal `match` equational theorems at simp trace

1

closes #4251

feat: make `<num>#<term>` bitvector literal notation global

3

The bitvector literal notation (e.g., `0x1#4`) is currently scoped, but it is used when pretty-printing. This has led to confusion among users who find that the notation does not work...

feat: `Simp.Config.implicitDefEqProofs`

2

This PR implements `Simp.Config.implicitDefEqsProofs`. When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated with an `rfl`-theorem. Rewriting rules are provided by users by annotating...

perf: use pointer equality at kernel `inferType` and `whnf` caches (WIP)

5

Motivation: when type checking big terms, we may get hash collisions for big terms that are structurally different, but very similar. In this kind of situation we may spend we...