Paul Reichert comments

Results 26 comments of


                                            Paul Reichert

refactor: migrate all usages of old slice notation

!bench

refactor: migrate all usages of old slice notation

!bench

refactor: migrate all usages of old slice notation

!bench

refactor: migrate all usages of old slice notation

!bench

Dynamically filter tests to run

These filters decide based on the the test description (which also provides the testId after being hashed), as far as I understand it. Is it also possible to use other...

Dynamically filter tests to run

Hmm, I see. So there is also no "initial ordering" preserved?

Dynamically filter tests to run

Thank you for your quick response. It's also about Stryker: To verify that tests cover all functionality, small changes to the source code are inserted into the code. The tests...

Usage of realizable constant `foo.eq_1` in privately imported module makes it private

Just checked and it's not specific to instances, I just forgot to minimize that part. I updated the MWE to illustrate this and to demonstrate that in `Basic.lean`, `x` has...

`simp`, `omega` in `module` cause type mismatch in kernel

That indeed solves the MWE, but it turns out that in the actual situation I had, I need to expose lots of defs. not so minimal working example ```lean module...

Regression in nightly: type mismatch (4.25.0-nightly-2025-10-10)

This seems to be related to the fact that #10319 adds a new get-elem tactic that relies on `omega`. I modified the example, forcing the usage of `omega` in the...