Hi Christian,
For code generation purposes and especially Quickcheck, it is necessary
that the FinFun theory would be imported by any user.
With the new developments lifting and transfer, we are getting very
close that FinFun can be used without any further ado.
I do have some latest experiments and patches in the shelf to be
published after the release.
Therefore, I am also in strong favour for moving the AFP entry FinFun
into the distribution.
In the long run, it should probably even become part of the HOL-Main image.
In the short term, we could move the FinFun theory into the HOL library
of the development version after Isabelle 2012 and the AFP 2012 has been
released, if we agree that this moves this contribution in the right
direction.
As Andreas has access to the Isabelle development and can freely change
and contribute the entry, I do not see any further difficulties.
Lukas
P.S.: The topic is interesting for isabelle-users as well in my opinion.
On 05/10/2012 05:09 PM, Christian Urban wrote:
Dear All,
In Nominal I am usually relying on types that are defined
in HOL or that I define myself. However, I now came across
the FinFun development in the AFP by Andreas Lochbihler (thanks
to Larry). The finfun type seems to be rather useful to Nominal
users, since it has finite support, in contrast to the function
type, which in general hasn't.
My question is how I should I interface with something that
is in the AFP and with something that is (eventually) in the
distribution? The problem is that Nominal always needs a wrapper
infrastructure for types, such as a definition of a permutation.
How should I write this wrapper, especially what should the import
paths be, so that users can conveniently use FinFuns and Nominal?
Should this wrapper be part of the AFP entry (in which case
the paths are clear, but then Nominal users have to fetch the
AFP explicitly and no Nominal example in the distribution can
depend on it)?
Or should the wrapper be part of Nominal (in which case I
can use it in examples, but I have no idea what the import
paths should be...the AFP can be anywhere)?
Or, should FinFun be part of the distribution (which would
make my life normal again)?
Is there any received wisdom for this problem?
Best wishes,
Christian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
