Hi all, I have the problem that locale interpretation introduces abbreviations for locally defined constants, rather than definitions. This does not work well with the code generator. Is there a way to make locale interpretation introduce real definitions, and, if not, how much effort would it be to implement such a feature?
Example: locale l = fixes g::"'a => 'b" begin definition "foo x == (g x,x)" lemma lem: "snd (foo x) = x" unfolding foo_def by simp end interpretation i: l id . thm i.lem export_code i.foo *** Not a constant: l.foo id What I would like here is, that the interpretation command introduces a new constant i.foo, with the definition (or at least code equation) "i.foo x == (g x,x)", and that this constant is also used in the instantiated facts. For this, the code generator could then generate code. Currently, I am defining those constants by hand, after the interpretation, which causes lots of boilerplate in my real applications with more than a dozen of definitions. -- Peter _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
