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).

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
> Date: Tuesday, September 1, 2009, 11:07 AM
> In
> 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.