Those are other things you can prove — I actually watched an idris talk where they included the complexity cost in the function and it refuses to run commands o

Those are other things you can prove — I actually watched an idris talk where they included the complexity cost in the function and it refuses to run commands over a certain complexity.