> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
