[POPLmark] Twelf questions

[Rob Simmons]

If you want an example of such a disjunctive conclusion, one is 
discussed at the Twelf Wiki (which I created as a side project during my 
senior undergraduate independent work, and which Frank Pfenning gave me 
web space for) :

http://fp.logosphere.cs.cmu.edu/twelf/?n=Answers.Factoring

The website has a number of examples, and it will hopefully become more 
useful with more contributions. twelf-list has been used for the sorts 
of questions you're talking about - a few months ago I thought it might 
interesting to experiment with doing this sort of thing with a Wiki, 
where it could be better preserved and better organized.

Rob

P.S. I'm currently working on doing a Wiki write-up based on the second 
longer question and Karl's response.

>> First, a short one.  I understand how to state and prove lemmas that
>> have a conjunction in the conclusion, using two positions with output
>> mode.  But how does one state a lemma with a disjunctive conclusion?
>>  
>>
> You do it much the same way you return a disjunctive result in ML; 
> define a new type with two cases and return a result of that type.