Needed to do a bit of hacking at the weekend, so I just sorted out the naming mechanism to allow and generate the x^n notation. Try typechecking lam X : * => lam X : X => X and lam X : * => lam X : X => X^1.
Next mission, a very simple interactive editor for proof states, given by (Cursor (Key UId Reference)) for now, but we’ll go tree-structured later. In the first instance, this should just have holes and lets, with refinement and undo as the basic operations. This requires the ability to propagate an update. Before long, though, we’ll want to have parametrised things, and a hierarchical structure. We should be able to knock up a serviceable toy in fairly short order.