@[inline]

def Array.lex {α : Type u_1} [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool

Compares arrays lexicographically with respect to a comparison lt on their elements.

Specifically, Array.lex as bs lt is true if

• bs is larger than as and as is pairwise equivalent via == to the initial segment of bs, or
• there is an index i such that lt as[i] bs[i], and for all j < i, as[j] == bs[j].

Equations

• as.lex bs lt = Array.lex.go as bs lt 0

@[specialize #[]]

def Array.lex.go {α : Type u_1} [BEq α] (as bs : Array α) (lt : α → α → Bool) (i : Nat) : Bool

Equations

• One or more equations did not get rendered due to their size.