JovanGerb
JovanGerb
My understanding is that in `exact?`, a relatively small amount of the computation time goes to searching in the `DiscrTree`, and most of the computation time is used for checking...
I should say that I've only compared the runtimes for building the `DiscrTree`, and not lookup, since that is the part that takes a lot of time. But when running...
For testing performance, I use Lean's heartbeats. Is that the generally accepted way of performance benchmarking?
I replaced the `Key.fvar` key with `Key.opaque`, which I think is a better name for it. This is used for indexing existentially quantified variables in the library so it is...
@Kha Thanks for the comments. I'll reply to them in order - I agree that calling `isDefEq` is possibly problematic. It seemed to me that in practice the `isDefEq` calls...
How should I go about unit testing/benchmarking? For `StateListT` I previously just replaced it in the code by an alternative to see the change, but that isn't exactly a unit...
That is also possible. I don't know if making changes there can break lot's of other things though, because class inference and `simp` calls could get slightly different results after...
> What is the state of this PR? I don't think the PR will merge very soon, since we need to first have a tactic that uses this DiscrTree and...
Here is a more minimal example that I ran into: ``` def oops (i : ∀ α, List α) : List β := i β ``` When hovering over the...
!bench