Alex Keizer

If I understand correctly, reencoding always happens when you apply a filter. So each interval (or chunk of 32 intervals in my version) is encoded separately. The final concatenation indeed...

Hmm, after looking at the ffmpeg documentation some more I found this: ``` -ss position (input/output) When used as an input option (before -i), seeks in this input file to...

We still want to focus the main goal, before applying `a`, so that `b` only works on those goals introduced by `a`. ``` example {x y : Nat} : y...

In any case, I probably won't have time to actually dig into this until my current project is finished (after which my need for it will be much less). For...

There is some precedent for this in the `induction` tactic, which does allow custom recursors with `induction ... using myRecursor`. I'd propose we mirror that syntax for pattern matching as...

Personally, I would say it's already an improvement to be able to customize only the top-level match, without nesting. We could set a limitation that a single `match` statement can...

That's a nice idea! But, we should be careful to not make totality checking too complicated. We could say that when tagging an eliminator with the `@[eliminator]` attribute, the user...

Good point! At first, I wondered if duplicating the constructors would lead to having to duplicate theorems as well, but since we're talking about term-mode `match` these constructors should only...

#14 has reduced the noise in tests, but there are still quite some noisy lines in the framework itself

In a sense, the tombstoning introduced in this PR is not so much about making names inaccessible, as it is about making sure that uses of a shadowing variable don't...