Jannis Limperg
Jannis Limperg
I was recently surprised by the lack of `splitAtR`, `takeR` and `dropR` in `Data.Sequence` when `takeWhileR` and `dropWhileR` are available. Taking this question to [Stack Overflow](http://stackoverflow.com/q/30966910/2948250), a simple implementation of...
This commit adds a low-priority meta instance which concludes `has_to_string α` from `has_to_format α`. The instance has to be meta since `format` is meta. This means that for most types,...
Just leaving this here as a note to myself (or to anyone else who wants to do this of course). I think this would be very helpful. I'm thinking of...
The MetaM chapter already contains some notes about matching expressions up to computation, using `whnf`. But arguably the more convenient approach is to use `isDefEq` with a pattern expression containing...
Another note to self: mention these functions somewhere in the MetaM chapter. There's not much to discuss, but this functionality is obviously important, so people should be able to discover...
Many basic functions have changed recently, e.g. `getMVarDecl` to `MVarId.getDecl`. The old versions are deprecated, so we (I) should update the book accordingly. See leanprover/lean4#1346.
The mechanism used for delayed mvar assignments has changed in a recent nightly. We have a brief section on this in the MetaM chapter, so we should check whether the...
The induction' and cases' tactics would previously not generalise the goal correctly when called with a complex term (i.e. not just a local constant) as major premise. E.g. the call...
In the medium term, we want to remove Aesop's dependency on Std so that Aesop can be used in Std. This requires two things: - Remove dependencies on Std where...
It sometimes happens that an Aesop rule has a premise that will always be true in practice, but Aesop can't always prove it. In such cases, it would be nice...