Epilogue

In a fit of anal retentiveness, I’ve spent this morning tidying up yesterday’s developments. In particular, I’ve separated out DeBruijn.lhs as a more generic bunch of utilities. Correspondingly, Scope has become a functor (I’ve also added a constructor for vacuous scopes, as these give rise to optimized execution for λ and cute print forms for ∀ and ∃). For any idiom which counts how many binders you’re under, the operator ‘shiftyMap’ pushes functions inside scopes, doing the right thing. Yesterday’s nu operation has been slightly refactored to make it less value specific. You’ll also be delighted to find that I’ve added a few more comments…

I’ve just created Term.lhs. I’ll be filling it up with glue very shortly.