search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

refactor: do not try rfl in mkEqnTypes in WF.mkEqns #4047

Closed nomeata closed 2 weeks ago

nomeata commented 2 weeks ago

when dealing with well-founded recursive definitions, tryURefl isn't going to be that useful and possibly slow. So disable that code path when doing well-founded recursion.

(This is a variant of #4025 where I tried using with_reducible to limit the impact of slow unfolding, but if we can get away with disabling it complete, then even better.)

nomeata commented 2 weeks ago

!bench

nomeata commented 2 weeks ago

Mathlib perf results: http://speed.lean-fro.org/mathlib4/compare/d263df69-867e-4d8e-b1b0-3f3ff0c077c9/to/029cb476-33f2-4227-84be-3ad9be09f0b8 Not significant changes.

leanprover-bot commented 2 weeks ago

Here are the benchmark results for commit 4606f1a1a13bd0a2f920b64549dcf044f32f79d9. There were no significant changes against commit 83c139f7504706624eb3dcb3d78000d4fc6f4d13.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):