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

You cannot use sets as types. You have to use the underlying type of the
set. Thus you need to define
F :: "t set => t"
where A is of type "t set". If F has no sensible extension to arbitrary
sets, you may need to define something like
"F B = (if finite B then ... else undefined)"
where "undefined" is a predefined constant whose value is not known.
Regards
Tobias
Bart Kastermans schrieb:
> 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.*