Re: [isabelle] Set of functions
On 22.05.2013 21:37, Roger H. wrote:
how do you denote the set of all functions from nat to nat?
For some type 'a, (UNIV :: 'a) denotes all values of this type. So "UNIV
:: nat => nat" are all functions from nat to nat.
what about the set of all partial functions from nat to nat?
Isabelle/HOL is a logic of total functions, i.e. there are no partial
functions. One way to model partial functions is to carry around an
explicit domain. Another way is to use functions from 'a to 'b option.
This archive was generated by a fusion of
Pipermail (Mailman edition) and