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.

  -- Lars




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