bool: type. t : bool. f: bool.
lemma : bool -> type.
%mode lemma +B.
thm : type.
%mode thm.
- : thm <- (lemma Z -> lemma t) <- (lemma Z -> lemma f).
Then output-freeness should save us from ever having to make outputs effectively inputs and using unification on them.
So this would mean doing more than patterns during unification, so one would have to handle postponing equations, but one side would always be ground, so no mucking about with computing intersection and restriction in deBruijn form.
A successful compilation of some clause should line up, I think, with a constructive witness that the clause is well-moded. If the inputs are ground, then one should be able to create a functional expression of what ground terms the outputs are instantiated with.
In other news I went to D's and it was above-average fun. And watched S03E03 of Lost. "We killed a polar bear".
