Comparing arrays for equality
To compare two one-dimensional arrays for equality, we can compare
them elementwise, yielding an array of bools, then use and to
check whether all those elements are true:
def eq_arr_i32 [n] (a: [n]i32) (b: [n]i32) : bool =
and (map2 (==) a b)This function requires us to already know that the arrays have the same size. We can also write a variant that does not have this requirement, but instead checks for the size explicitly and then uses a size coercion:
def eq_arr_i32_any [n] [m] (a: [n]i32) (b: [m]i32) : bool =
n == m && eq_arr_i32 a (b :> [n]i32)This implementation is still restricted to arrays of integers. We can make a polymorphic one that expects the user to provide an equality function:
def eq_arr 'a [n] [m] (eq: a -> a -> bool) (a: [n]a) (b: [m]a) : bool =
n == m && and (map2 eq a (b :> [n]a))This can then be used to define a function that works for two-dimensional arrays:
def eq_arr_2d 'a [n1] [n2] [m1] [m2]
(eq: a -> a -> bool) (a: [n1][n2]a) (b: [m1][m2]a) : bool =
n1 == m1 && n2 == m2 && eq_arr (eq_arr eq) a (b :> [n1][n2]a)