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



Dear Isabelle Users:

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"


	Yours truly,

		Aaron W. Hsu

-- 
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.






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