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

In Isabelle/ZF Fin(A) -> A is a set of functions whose domain is Fin(A) and values are in A. The statement "F : Fin(A) -> A" is the same as "F \<in> Fin(A) -> A" and means that F is in this set (i.e. is such function).
Slawekk
http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
--- On Tue, 9/1/09, Bart Kastermans <Bart.Kastermans at Colorado.EDU> wrote:
> From: Bart Kastermans <Bart.Kastermans at Colorado.EDU>
> Subject: [isabelle] Defining a function on an inductively defined set.
> To: cl-isabelle-users at lists.cam.ac.uk
> Date: Tuesday, September 1, 2009, 11:07 AM
> 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.*