Currently, we implement cases using the recursor. This means every time we want to do a cases operation we have to walk the entire datastructure just to throw away the result at the end.
This is fine for proving, but might not be good for computation.
It might be possible to use Fix.dest, which effectively unfolds a fixpoint type once,
but it turns out that Fix.dest is implemented using Fix.drec, so this would not avoid the full recursion.
In future it might be worth fixing this by adding the correct theorems to dest and removing its dependence on rec.
Currently, we implement
casesusing the recursor. This means every time we want to do a cases operation we have to walk the entire datastructure just to throw away the result at the end.This is fine for proving, but might not be good for computation.
It might be possible to use
Fix.dest, which effectively unfolds a fixpoint type once,but it turns out that
Fix.destis implemented usingFix.drec, so this would not avoid the full recursion.In future it might be worth fixing this by adding the correct theorems to
destand removing its dependence on rec.