Hi Andreas, > Code_Target_Nat implements the type nat as an abstract type (code abstype) > with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not > appear in any equation of the code generator. Unfortunately, this declaration > also sets up the term_of function for type nat to produce terms with this > constructor. In the second example, your import_proof method uses the term_of > function to get a term for the given proof (and the number contained in the > proof) and introduces along with this number into the goal state. > As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then > apply eval, the code generator complains that the abstract constructor is > part of the goal state.
I now see the problem. > The simplest solution is to introduce a new constructor for which you can > prove a code equation. For example, the following defines a constructor Nat2 > and redefines term_of for naturals to use Nat2. When you add it to your > theory before declaring the parser structure, the second example works, too > (tested with Isabelle 2b68f4109075). You then also have to reflect both nat > and int as datatypes. I integrated this solution also in our larger development, and it works like a charm. Thanks! > If nobody has a better solution, we should think of including this setup in > Code_Target_Nat. At least from my side, I can confirm that the solution works nicely. Cheers, René _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
