Engineering Pride

[MonoidMusician]

Checklist of things I want to clean up in the code that aren't going to be visible to users, just devs:

1. (style) Use consistent names for variables across the codebase, e.g. we should decide to always write Pi (nm, a, b) instead of Pi (name, tm1, tm2) or whatever
2. (docs) Related: document what each of those constructors look like in syntax,
3. (docs) Document what effects each module uses and how they interact, e.g. how Eff.Locals feeds all the other environments (semantics, quoting, and pretty-printing)
4. (docs) How to add stuff to the syntax (tokens, grammar, elaboration, and data/syntax/semantics, if applicable)
5. (code) Remove duplication between rules/Hom.ml and rules/Prog.hml
6. (code) Remove duplication of common constructions, like calculating the underlying type of HomLam (currently in the conversion checker, elaborator, quoter, and do_hom_elim), and D.Neu (tp, { hd = D.Borrow lvl; spine = Emp }))
7. (code) Remove extraneous Debug.print statements

[solomon-b]

@MonoidMusician where would you say we are at on this issue?

[MonoidMusician]

I'm going to keep adding things as they come up, I don't think we're going to close it any time soon.