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.
I’ve hacked up some of the boring bits. In Ecce.lhs (thus far undocumented), there’s a basic interactive thingy which displays the state and lets you navigate, add new declarations and definitions, evaluate stuff and quit. But no proof tactics yet…
I’ve finally got round to adding the ability to fill holes, please test