You may have noticed that Term.lhs is a little shorter. I just shifted everything not strictly necessary for the syntax and operational semantics into other files, viz.
- TermTools.lhs
with yer abstractor and yer instantiator // and yer discharger |- and yer quantifier-stripper -| and a’that. Most especially, the β-behaviour of typed terms (which must only be used in a type-correct way). See here. This is what the typechecker will call to assemble values with which it’s happy. See here. - Normal.lhs now has the weak-head and full normalization algs. The latter will be tweaked to use typed β next time I commit.
You’ll also have noticed that I’m up to something, down the bottom of the file, with some form of Code. More on that in a bit.