Mario Carneiro
Mario Carneiro
I think the most helpful test for this and other kernel `perf:` PRs is `lean4checker --fresh Mathlib` wallclock / instruction count / other perf metrics. Unfortunately I don't think we...
Yes, it would also work without `--fresh`, although this will add multithreading and contention stuff so it may make the benchmarks more noisy. We could also consider testing only selected...
@leodemoura I'll do my best, but as indicated above I don't even have evidence that the optimization does anything at all. That is, even in the best case when the...
I have managed to confirm that on master, the last two examples trigger the fast path, and on this PR the first two trigger the fast path, which is as...
I think this should be disabled by default, or only enabled in CI. For people using vscode with the "remove trailing whitespace on save" option, it will only ever be...
We don't really have a place to put scripts like this. Ideally we could put it somewhere such that lake would make it available to downstream packages.
I'm not a fan, this turns things that would be recursive on lists into well founded recursions.
`IsChain1`? `IsChainSucc`?
This PR fixes part of the issue (it prevents ```lean inductive Foo : Prop where | mk (x : Nat) (h : x = x) : Foo example (h :...
This seems unlikely to work, especially if you consider that you can also call `f3 (1 + 1) 2`, at which point it's not clear what name `x` is supposed...