*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Question to Sledgehammer output*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 27 May 2008 14:07:53 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <483BF72A.2040304@uni-muenster.de>*References*: <483BF72A.2040304@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

I guess the error message could be more user friendly ;-) Tobias Peter Lammich schrieb:

I get the following sledgehammer output (using E). It talks about a typeunification error, what does this mean ?The proposed metis command seems to run very long (I aborted it after afew minutes and wrote by (induct x) auto in the meantime ;))Subgoal 1: map snd (map (\<lambda>(a, b). (f a, b)) x) = map snd x Try this command:apply (metis Pair_eq Set.subsetI finite finite_surj finite_surj_injid_apply injD inj_on_id inv_f_f inv_id not_Cons_self rangeI snd_eqDsurjective_pairing)Translation of TSTP raised an exception: Type unification failed Type error in application: Incompatible operand typeOperator: op ` :: (?'X5.0 \<Rightarrow> ?'X6.0) \<Rightarrow> ?'X5.0set \<Rightarrow> ?'X6.0 setOperand: snd :: ?'X1.0 \<times> ?'X2.0 \<Rightarrow> ?'X2.0 regards, Peter

**References**:**[isabelle] Question to Sledgehammer output***From:*Peter Lammich

- Previous by Date: [isabelle] Question to Sledgehammer output
- Next by Date: [isabelle] context-sensitive termination proof
- Previous by Thread: [isabelle] Question to Sledgehammer output
- Next by Thread: [isabelle] context-sensitive termination proof
- Cl-isabelle-users May 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list