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



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





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