Siddharth
Siddharth
Done, I've made the requested changes. The PR is still in draft mode as it is stacked on top of https://github.com/leanprover/lean4/pull/3480.
awaiting-review
Superceded by https://github.com/leanprover/lean4/commit/23a202b6bec6348301c65a3260d52f561d3b55fb
awaiting-review
They're no longer `simp` lemmas.
awaiting-review
Then I am somewhat unsure as to why this fixes a link issue I have.
I stumbled on the fact that `Checkpoint` is not used today and was confused as well. If it _can_ be used, what is a good use-case for it? I wanted...
@simonpj Indeed, `fuel` makes sense :) I wasn't sure what `Checkpoint` was doing. I presumed it was to be able to speculate on optimisations, but I couldn't find any such...
@mlite where is the performance optimised version described?