Re: [isabelle] Set of functions
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"
Am 22.05.2013 um 21:37 schrieb "Roger H." <s57076 at hotmail.com>:
> 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