search

namme-anetten / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Demo: correct semantics of 'next', 'prev' tactics #89

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
During the demo, this sequence of commands is fairly common:

 > let test : Set
 > root
 > next

After 'root', we expect to be deep *down* in the ProofState, so we would think 
that 'prev' is the thing to do. For some reason, it's 'next'.

A better fix would be to have proper "programming problem" navigation commands, 
with a 'qed' command that would check that the problem is solved.

Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 10:51

GoogleCodeExporter commented 9 years ago 
Adjusting the semantics of 'prev' and 'next' is likely to be more trouble than 
it's worth. I suggest we implement 'qed' to move out to the development 
containing the original let-definition, which is generally where you want to 
end up. This should be cheap, and later we can always make it actually check 
the problem is completely solved.

Original comment by adamgundry on 9 Sep 2010 at 9:40