*To*: Bart Kastermans <Bart.Kastermans at Colorado.EDU>*Subject*: Re: [isabelle] Defining a function on an inductively defined set.*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 02 Sep 2009 14:20:07 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4A9D62C6.80307@colorado.edu>*References*: <4A9D62C6.80307@colorado.edu>*User-agent*: Thunderbird 2.0.0.23 (Macintosh/20090812)

PS If the definition of the function follows the inductive definition of the set, it may be better to define your function as an inductive relation, possibly turning it into a function via THE afterwards. 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

**References**:**[isabelle] Defining a function on an inductively defined set.***From:*Bart Kastermans

- Previous by Date: Re: [isabelle] Defining a function on an inductively defined set.
- Next by Date: [isabelle] Quick question about rule+
- Previous by Thread: Re: [isabelle] Defining a function on an inductively defined set.
- Next by Thread: Re: [isabelle] Defining a function on an inductively defined set.
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list