Yesterday’s stuff

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.

Leave a Reply