Hi
I'm sure in the future Epigram will support plenty of sophisticated
chain reactions (triggered by local undos), as envisaged in "the
deletion of information can have highly non-local effects".
But for now, i'd like to recommend a conservative 'proof tactic' with
an undo when giving a proof which requires a lemma, e.g.
rev (rev l) = l
as in http://www.cs.nott.ac.uk/~txa/g5bcfr/l5.epi
When you've come to the point, where you need to prove the lemma, name
it and it's parameters where you need it. Then give its signature
(further up the script) and elaborate to see if it's wellformed. Now
elaborate the shed with the 'call' to the lemma to see if you're aiming
right. But undo the last step before you go and implement the lemma.
That might look unwieldy as Epigram checks for you that what you're
coming up with fits the theoretical gap you're trying to fill, so you
don't have to use your own eyes and compare context and signature. But i
find elaborating the use of a lemma last helps to complete the bigger
picture, especially when the proof of the lemma takes longer than
spotting where it's needed.
Have a nice weekend,
Sebastian
