From my comment in Elaboration.Wire:
There is something fishy with this |tellEntry| and the invariant of "when
applied on a definition, this definition must be the current entry".
In reality, there are two function, one defined on Parameters and called only
on Parameters (in @ProofState.Edition.Navigation@) (call it
|tellParameterEntry|) and one defined on Definitions and only called by itself
and |tellCurrentEntry| in a safe wrapper enforcing this invariant (call it
|tellDefinitionEntry|)
If we do the split, on one hand, the invariant will always be enforced. On the
other hand, we get two functions with a partial pattern-matching. At least,
with two explicitly named functions, one can hardly ignore that one is for
Parameters and the other for Definitions.
It's up to debate.
Original issue reported on code.google.com by pedag...@gmail.com on 26 Aug 2010 at 5:14
Original issue reported on code.google.com by
pedag...@gmail.comon 26 Aug 2010 at 5:14