[PostScript]
ArraySlice2 (E, I1, I2, A): trait
  % A two-dimensional array
  % treated as a vector of vectors
  includes 
    Array1 (E, I2, A1),
    Array1 (A1, I1, A)
  introduces
    assign: A, I1, I2, E -> A
    __[__, __]: A, I1, I2 -> E
  asserts
    forall a: A, i1: I1, i2: I2, e: E
      a[i1, i2] == (a[i1])[i2];
      assign(a, i1, i2, e) ==
        assign(a, i1, assign(a[i1], i2, e))
[Table of Contents] [Index]