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 > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
