Re: [isabelle] Linear Ordering for nat list
On Wed, 02 May 2012 14:59:36 +1000, Peter Gammie wrote:
> Perhaps you can give us more information on what you're trying to do.
I am trying to come up with a basic notion of multi-dimensional arrays
that I can use to model some things. Specifically, these arrays should
map indices to specific values, be finite, and should be dense. The most
basic thing I want to do with them is to get the shape. This, I want to
have functions with the following type:
f :: "'a array => 'a array"
And similar. The property of density is the one I am having trouble with
right now. I want to state that for an array of a given shape, all of
the indices of the given shape from [0,...,0] to [n_1-1,...,n_r-1] are
defined, but no others, assuming that the array is of rank r, where n_i
is the size of the array in dimension i, with 1 <= i <= r.
Any suggestions on the best way to model this would be appreciated.
Right now I am using Map.
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