[isabelle-dev] Coinductive FAILED

[Jasmin Christian Blanchette]

Hi Florian,

My bad again. Fixed (578371ba74cc). Now I see why "pervasive = true" makes sense.

Thanks for the notice.

BTW is there any particular reason why testboard and tests are kind of dead these days?

Jasmin



Am 06.11.2013 um 21:12 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> isabelle b01057e72233 / afp 30c892926c46
> 
>> Coinductive FAILED
>> (see also /mnt/home/haftmann/data/isabelle/devel/heaps/polyml-5.5.1_x86-linux/log/Coinductive)
>> 
>> s/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texmf-dist/fonts/type1/public/
>> amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cms
>> y8.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/s
>> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmti12.pfb></usr/share/texmf-dis
>> t/fonts/type1/public/amsfonts/cm/cmtt10.pfb>
>> Output written on root.pdf (303 pages, 845312 bytes).
>> Transcript written on root.log.
>> 
>> *** Theory loader: failed to load "Coinductive_List_Prefix" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "Koenigslemma" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "Lazy_LList" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "Quotient_Coinductive_List" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "Coinductive_Stream" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "TLList" (unresolved "Coinductive_List")
>> *** Theory loader: failed to load "Quotient_TLList" (unresolved "TLList")
>> *** Theory loader: failed to load "Lazy_TLList" (unresolved "Lazy_LList", "TLList")
>> *** Theory loader: failed to load "Coinductive" (unresolved "Coinductive_List_Prefix", "Coinductive_Stream", "Koenigslemma", "Quotient_Coinductive_List", "Quotient_TLList")
>> *** Error in case expression:
>> *** type mismatch
>> *** At command "lemma" (line 873 of "/mnt/home/haftmann/data/afp/devel/thys/Coinductive/Coinductive_List.thy")
> 
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev