@[instance_reducible]

def Hex.instDecidableEqArray {α : Type u} [DecidableEq α] : DecidableEq (Array α)

DecidableEq (Array α) that reduces in the kernel under the module system, routing through the fully exposed List equality.

Equations

• Hex.instDecidableEqArray a b = match h : decEq a.toList b.toList with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯

@[instance_reducible]

def Hex.instDecidableEqVector {α : Type u} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n)

DecidableEq (Vector α n) that reduces in the kernel under the module system. Vector's core instance is derived, and derived instances are opaque across a module boundary.

Equations

• Hex.instDecidableEqVector a b = match h : decEq a.toArray.toList b.toArray.toList with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯

@[csimp]

theorem Hex.instDecidableEqArray_eq : @instDecidableEqArray = @Array.instDecidableEq

Compiled code uses the core Array decider, which compares in place. The List route exists only so that the kernel can reduce it. DecidableEq is a subsingleton, so the two agree.

@[csimp]

theorem Hex.instDecidableEqVector_eq : @instDecidableEqVector = @_root_.instDecidableEqVector

The Hex.instDecidableEqVector analogue of Hex.instDecidableEqArray_eq.