That was due to my reforms of the sublist/subseq stuff and should be
repaired by this afternoon. Tomorrow's slow tests should run through
fine again. Unfortunately, these slow sessions don't have the same rapid
testing cycle as the normal sessions.
Manuel
On 2017-06-01 16:19, Florian Haftmann wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
