brutally unbreak build
add definition of big_oh
a first cut at a Racket-based version of this
language that generates the Coq code with built-in
step counting

still not right, tho