[isabelle-dev] JinjaThreads FAILED
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sun Nov 16 19:48:22 CET 2014
> isabelle: 059ba950a657 tip
> afp: 0fdf8f639bb4 tip
> Running JinjaThreads ...
>
>
> JinjaThreads FAILED
> (see also /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/JinjaThreads)
>
> *** At command "inductive" (line 413 of "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> *** Type unification failed: No type arity prod :: floor_ceiling
> ***
> *** Type error in application: incompatible operand type
> ***
> *** Operator: floor :: ??'a => int
> *** Operand: (x, ln) :: ??'b * (real => real)
> ***
> *** Coercion Inference:
> ***
> *** Local coercion insertion on the operand failed:
> *** No type arity prod :: floor_ceiling
> ***
> *** Now trying to infer coercions globally.
> ***
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> *** Clash of types "_ option" and "int"
> ***
> *** At command "inductive" (line 413 of "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> Unfinished session(s): JinjaThreads
> 0:13:06 elapsed time, 1:00:51 cpu time, factor 4.64
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141116/0e8fbc29/attachment.asc>
More information about the isabelle-dev
mailing list