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 ;))
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
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