[isabelle] Defining a function on an inductively defined set.



In

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Finite.html

the collection of finite subsets Fin(A) of a set A is defined. I want to define a function
F : Fin(A) => A.

What is the best way to go about this? None of my attempts parse. I realize that Fin(A) is not a type, but am not sure how to work around this.

Best,
Bart





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.