Email Gateway (Aug 18 2022 at 11:56): Email Gateway (Aug 18 2022 at 11:56):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
regards,
Peter
Email Gateway (Aug 18 2022 at 11:56):From: Tobias Nipkow <nipkow@in.tum.de>
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 ;-)
Tobias
Peter Lammich schrieb:
Last updated: May 03 2024 at 04:19 UTC