Sebastian Ullrich

icon company Lean FRO icon location Munich, Germany

Results 427 comments of Sebastian Ullrich

feat: `debug.proofAsSorry`

It doesn't look like we'll need this

test: `big_omega` benchmark

@bollu Do you agree to this test being added to the repo?

test: `big_omega` benchmark

!bench

fix: `instantiateMVars` slowdown in the language server

!bench

show ctest system-out as details

Oops, I intended to open a PR to my own fork... I don't know if you want such a specific change upstream

show ctest system-out as details

(I think it's broken anyway)

fix: do not ban `..` with a `.` on the next line

Why is this a draft?

fix: do not ban `..` with a `.` on the next line

Thanks. Please add a module docstring to the test describing its purpose as mentioned in testing.md

perf: `infer_app` with `infer_only := false` (WIP)

Either of these might or might not be noise, the instruction count suggests that there is probably no impact overall. We should try again on top of https://github.com/leanprover-community/mathlib4/pull/8224

RFC: Make `IO` universe polymorphic

How would you ever make use of a higher-universe `IO` if `main` etc. remain in `IO.{0}`?