Re: [isabelle] Set of functions



Dear Roger,

I would take the UNIV constants, which is the set of all elements
of a given type.

I.e., in your case you will require

term "UNIV :: (nat => nat) set"
term "UNIV :: (nat => nat option) set"

Cheers,
René

Am 22.05.2013 um 21:37 schrieb "Roger H." <s57076 at hotmail.com>:

> Hello,
> 
> 
> how do you denote the set of all functions from nat to nat?
> 
> 
> what about the set of all partial functions from nat to nat?
> 
> 
> Thank you!
> 		 	   		  
> 





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