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,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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