Robert Peszek (2) [Avatar] Offline
#1
Quoting 10.2.2:
"You now have an implementation of myReverse that runs in linear time,
because it traverses the list once to build the SnocList view and then traverses
the SnocList view once to build the reversed list."

It looks to me that in Idris example (`snocListHelp`)
we have a linear cost proof at each step causing overall quadratic cost.
Few timing experiments with my code seem to confirm that.

Is there some mechanism to exclude runtime proof cost?
I want to clarify my understanding of this,
does the book mean linear excluding proofs, or Idris can somehow replace the proofs
with something like believe-me at runtime?

I could not find answer for this, sorry if I missed it.