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

So 'latt2 now seems to be in a mess.

The theorem I used was like this (something similar worked 

MkLat_recursion_lemma ;
val it = %turnstile% %forall% cf C a b· %exists% f· f (MkLat 
C a b) = cf C a b

(it isn't really a recursion theorem, I just want to be able 
to write function definitions by pattern matching on MkLat).

Any ideas on what is going on here?

Roger Jones

Proofpower mailing list

Reply via email to