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.
Bart Kastermans schrieb:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and