operators and arities

[ivoysey]

reformulate things in terms of 312-style-ish operators and arities. this should mean that case is easier to state, movements to children can be done with Fin (arity oper) rather than ad hoc hoping to pick the right indices, and a bunch of rules can be combined. at the least, the ap and plus rules would get combined

do this for types, too---as evidenced by thinking about adding sums, the same problems exist there. and really, that's why 312 uses the same ABT functor for types as well as terms.

[ivoysey]

this might also let us restate the action semantics that makes fewer proof cases? like instead of zip1, zip2 etc, index them by fin4 or whatever.

[ivoysey]

from the old todo:

- abstract over movments somehow. moving between arguments is a little hard
  coded; what if everything had a list of arguments instead of specific
  forms? is that the slippery slope to writing a full ABT library, or the
  one to lvars?

[cyrus-]

we should probably leave this (and #4 and #5) as future work, no need to do this for the POPL artifact

[ivoysey]

yeah, i think i agree.

[ivoysey]

migrating this to the issue tracker repo.