using meta-interpreters to debug nominal quines
getting stack trace for quine reduction: lein run -m tapl.quines_nom_red_small_debug.clj
fix small step reducer so that cons only takes quoted exps -- not functions b/c rep is diff in clojure
opt
simple use of proof meta-interpreter for STLC
one more deriv ex
generating proof trees typesetted in TeX
minor: make cases disjoint
first steps towards a proof debugger
add a flag for ok derivation or not
first stab at showing derivation trees for debugging
colors
move out private defs from let, for easier repl fu
a bit more debugging support
better output
a few more output tweaks
fix debugging restriction and better printing
use snapshot core.logic and bump logically
a WORKING substitution-based quine generator

working my way up from mini:
- explicit quoting to distinguish between functions and things that
  can appear quoted
- functions evaluates to themselves, and are restored to be first class
- so, app case explicitly says it's not one of the previous cases
- lists are restored to be of any arity

things to notice:
- quines are equal up to alpha-renaming
- code is ugly
started utils