<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">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.<br>
</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 2017-06-01 16:19, Florian Haftmann
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:550bee68-da4e-b7e4-822c-9220ecd3281d@informatik.tu-muenchen.de">
<pre wrap="">isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip
</pre>
<blockquote type="cite">
<pre wrap="">*** {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")
</pre>
</blockquote>
<pre wrap="">
Any suggestion what is going on here?
Cheers,
Florian
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>