[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