Sebastian Ullrich

For recursive functions, especially ones that are not trivially structurally recursive, we want to automatically generate induction rules that reflect the function's recursion structure so that proofs over the function...

(as created by `mklink` or cmake using Developer Mode)

RFC: reorganizing docs

9

There have been multiple discussions about the structure of our documentation recently. There is also a practical issue of the chapter sidebar becoming too long to comfortably navigate the mdBook...

Originally from `module.cpp` (RIP) ---- - Persistent `set_option`. We want to be able to store the option settings in .olean files. The main issue is conflict between imported modules. That...

We store the Lean wrappers of stdin/stdout/stderr in thread-local variables to support redirection as in `withStdin/...`. New threads spawned within these functions should inherit these variables. Note that if a...

This is another unexpected RC operation I noticed while debugging the recent lsan false positive. If their RC is 1, neither the task closure nor its captured values should be...

Signature pretty printer

11

In hover text etc., we should not naively print the signature as a term to the right of the colon `:` but move parameters to the left of it, ensuring...

Code lense on slow declarations

3

Just testing the waters here: would a code lense showing the processing time for declarations that took more time than `profiler.threshold` be more valuable to mathlib maintainers and authors than...