Vectors

Vector α n is a thin wrapper around Array α for arrays of fixed size n.

@[inline]

def Vector.allDiff {α : Type u_1} {n : Nat} [BEq α] (as : Vector α n) : Bool

Returns true when all elements of the vector are pairwise distinct using == for comparison.

Equations

• as.allDiff = as.toArray.allDiff