Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code



Hi Andreas,

> theory Scratch imports "~~/src/HOL/BNF/BNF" begin
> codatatype foo = Foo | Bar foo
> code_datatype Foo Bar
> code_thms foo_unfold
> 
> At code_thms, I get "Proof failed." and a huge goal state talking about
> the internal BNF construction for the the foo instead of the usual list
> of theorems that I would like to inspect. The same happens at
> export_code and value [code].

I did not inspect the code, but I guess it happens since internal proofs
are forked, which are only forced when the code generator is invoked.
Maybe the BNF gurus can tell you more.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.