kaonn
kaonn
I think the way the eq type is being used currently suggests that it should be a negative type whose computations are the Agda equality between the relevant terms. Eq...
No really sure what this pr does, but let's just leave it for now.
I think the error is contained to the various `split` functions, so it shouldn't take so long to typecheck.
my bad, I removed the other files that are irrelevant for split. It really doesn't depend on any of the brutal proofs in `merge` or `insert`.
I'm drawn to incur or charge since that's how I usually verbalize step.