Roger,

On 17 Aug 2010, at 10:46, Roger Bishop Jones wrote:

> Here is a sequence of actions with ProofPower which is 
> causing me puzzlement.
> 
> :) set_merge_pcs ["unalg", "'latt2"];
> 
> val it = () : unit
> 
> :) add_%exists%_cd_thms [MkLat_recursion_lemma] "'latt2";
> 
> val it = () : unit
> 
> :) set_merge_pcs ["unalg", "'latt2"];
> Exception Fail * Element cannot be found in list [find.1004] 
> * raised
> 

This is clearly a bug - if there is something wrong with your commands then you 
deserve a much better error message.

> So 'latt2 now seems to be in a mess.
> 
> The theorem I used was like this (something similar worked 
> previously).
> 
> MkLat_recursion_lemma ;
> val it = %turnstile% %forall% cf C a b· %exists% f· f (MkLat 
> C a b) = cf C a b
> : THM
> 
> (it isn't really a recursion theorem, I just want to be able 
> to write function definitions by pattern matching on MkLat).
> 
There is nothing wrong with that.

> Any ideas on what is going on here?

Unfortunately, you haven't given enough to show how to reproduce the problem.

Regards,

Rob.

> 
> Roger Jones
> 
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to