isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip
> *** {n. enat n < llength stls \<and>
> *** (case lnth stls n of
> *** (s, tl, s') \<Rightarrow> \<not> \<tau>move s tl s')} ::
> *** nat set
> ***
> *** Coercion Inference:
> ***
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> ***
> *** Now trying to infer coercions globally.
> ***
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> ***
> ***
> *** At command "hence" (line 512 of
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
> *** Type unification failed
> ***
> *** Type error in application: incompatible operand type
> ***
> *** Operator: lsublist tls :: 'a \<Rightarrow> 'tl llist
> *** Operand:
> *** {n. enat n < llength stls \<and>
> *** (case lnth stls n of
> *** (s, tl, s') \<Rightarrow> \<not> \<tau>move s tl s')} ::
> *** nat set
> ***
> *** Coercion Inference:
> ***
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> ***
> *** Now trying to infer coercions globally.
> ***
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> ***
> ***
> *** At command "hence" (line 512 of
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
Any suggestion what is going on here?
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
