Re: [isabelle] Question to Sledgehammer output

It looks like s/h found a proof which is not a proof because type information was omitted in the translation for the first-order provers. Theorems about finiteness often indicate that that's what happened. There is nothing you can do, as far as I know.

I guess the error message could be more user friendly ;-)


Peter Lammich schrieb:
I get the following sledgehammer output (using E). It talks about a type unification error, what does this mean ? The proposed metis command seems to run very long (I aborted it after a few 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_inj id_apply injD inj_on_id inv_f_f inv_id not_Cons_self rangeI snd_eqD surjective_pairing)

Translation of TSTP raised an exception: Type unification failed
Type error in application: Incompatible operand type

Operator: op ` :: (?'X5.0 \<Rightarrow> ?'X6.0) \<Rightarrow> ?'X5.0 set \<Rightarrow> ?'X6.0 set
Operand:   snd :: ?'X1.0 \<times> ?'X2.0 \<Rightarrow> ?'X2.0


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.