Joachim Breitner

http://www.joachim-breitner.de/ [email protected]

Lean FRO Freiburg, Germany

Results 908 comments of


                                            Joachim Breitner

`simp` uses `congr` lemmas that are not visible

Probably a missing `exportEntry` function that prevents these entries from entering the public environment in the first place, somewhere near https://github.com/leanprover/lean4/blob/057b70b443d99c08be8b0f193cfa0690b42d0185/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean#L49 or - if possible - in SimpleScopedEnvExtension directly in...

Add ?limit= parameter

This would fix #40, but only in a rather superficial way: The hits are still generated, just not returned to the client. I wonder how useful that is. I’d suggest...

Failed to generate equality theorems

Still the case with Lean 4.18.0-nightly-2025-02-11.

Failed to generate equality theorems

The error message is similar to #9846, so when fixing one of the two, check the other!

Failed to generate equality theorems

Ah, there is a simple workaround in this case: Explicitly include the index in the pattern matching: ``` def plus (t : Term Γ a) : Term Γ a :=...

perf: experiment: reduce primitive recursive functions directly

!bench

perf: experiment: reduce primitive recursive functions directly

!bench

perf: experiment: reduce primitive recursive functions directly

!bench

perf: experiment: reduce primitive recursive functions directly

!bench

perf: experiment: reduce primitive recursive functions directly

!bench

‹
1
2
...
82
83
84
85
86
87
88
89
90
91
›