rfindler/395-2013 — pull request #8 by maxsnew (2013-12-19 22:27:43+00:00)
Title: Naive Make Array 1 and Beginning of Naive Make Array 2

Implementation with and without runtime complexity proof of the first version of make_array.

I've also tried to define unravel and I think I have the right type, but it looks like Program can't handle non-inductive datatypes.