JovanGerb

This is the same as my DiscrTree PR in Std, but I've decided to move it over to Mathlib now. Additionally, I have added the `rw??` tactic which uses this...

feat: DiscrTree

27

I've made a new version of Lean's `DiscrTree` called `RefinedDiscrTree` with a lot of new features. It is able to index lambda's, forall's, and their bound variables. It also gives...

Lean pr testing 4152

4

Testing some aggressive instance caching. --- [](https://gitpod.io/from-referrer/)

chore: remove unnecessary outParam

2

I spotted an `outParam` in an instance argument of a class. The purpose of `outParam` is to fill in the value during type class search. However, since this is an...

Lean pr testing 4206

2

The bug fix lean4#4206 causes some change in the behaviour of `congr`, `convert` and friends. So some proofs need to be fixed, usually by providing more arguments. --- [![Open in...

Lean pr testing 4272

4

testing more aggressive caching --- [](https://gitpod.io/from-referrer/)

Lean pr testing 4276

2

--- [](https://gitpod.io/from-referrer/)

chore: clean up TC inference implementation

1

### This PR optimizes the type class search algorithm - We don't want trace messages to slow down type class search when trace is not enabled, so I made sure...

perf: cache intermediate type class results and non-results

1

Cache intermediate type class successes and failures. A cleaned up version of #4152, (on that branch I was experimenting with some other stuff) Note: in some tests, the numbers in...

perf: use `hasExprMvar` in type class search

2

I'm wondering if this change has a significant effect on Mathlib, because there might be lots of universe metavariables flying around there that we don't care about. --- Closes #0000...