[isabelle-dev] Nominal and FinFuns from the AFP
christian.urban at kcl.ac.uk
Thu May 10 17:09:26 CEST 2012
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?
More information about the isabelle-dev