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