# Re: [isabelle] Dealing with Int and Nat at the same time

Dear Aaron,
> I was wondering what the best, most convenient way to deal with
> numbers would be. Specifically, I have a datatype that I want
> to be something like 'a mytype, where 'a should usually be either
> an int or a nat or some other sort of number. Inside this type
> will be a list of 'a list. I then want to have another function
> that has the type of "'a mytype => 'a list" that will generate
> lists containing all zeros. I am not really sure what the best
> way to do this is, because Isabelle complains to me about the 0
> not matching the type, since Isabelle doesn't know that I only
> want 'a to be numbers. Is there some good way to do this"
Isabelle has a mechanism called "type classes" (or "sorts") to restrict the range of a type variable like 'a. "0" is defined in the "zero" type class, "1" in "one", and arbitrary numerals in "numeral". For example:
datatype 'a mytype = MyType "'a list"
fun only_zeros :: "'a mytype => ('b::zero) list" where
"only_zeros (MyType ns) = map (%x. (0::'b::zero)) ns"
value "only_zeros (MyType [1, 2, 3])"
Notice the syntax: "::" attaches a type class constraint to a type variable in a similar way that it attaches a type to a term; in fact, in "0::'b::zero", both uses of "::" are present.
If you need both zeros and ones, you can use "'b::{zero,one}". See the Isabelle tutorial, section 8.3, for details:
http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf
Regards,
Jasmin

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