Decidable membership and hashing for Int64Array

Decidable membership, slice hashing and the lawful BEq and Hashable instances on slices. Left out of the float types, which have no DecidableEq.

theorem ScalarArray.Int64Array.contains_iff_mem {a : Int64Array} {x : Int64} : a.contains x = true ↔ x ∈ a

@[implemented_by _private.ScalarArray.Int64.Decidable.0.ScalarArray.Int64Array.decMemImpl]

def ScalarArray.Int64Array.decMem (x : Int64) (a : Int64Array) : Decidable (x ∈ a)

Decides membership with contains. Logically it decides membership in a.toList, so that decide can evaluate it.

Equations

• ScalarArray.Int64Array.decMem x a = decidable_of_iff (x ∈ a.toList) ⋯

@[instance_reducible]

instance ScalarArray.Int64Array.instDecidableMemInt64 (x : Int64) (a : Int64Array) : Decidable (x ∈ a)

Equations

• ScalarArray.Int64Array.instDecidableMemInt64 x a = ScalarArray.Int64Array.decMem x a

@[simp]

theorem ScalarArray.Int64Array.contains_eq_mem {a : Int64Array} {x : Int64} : a.contains x = decide (x ∈ a)

theorem ScalarArray.Int64Array.Slice.contains_iff_mem {s : Int64Array.Slice} {x : Int64} : s.contains x = true ↔ x ∈ s

@[implemented_by _private.ScalarArray.Int64.Decidable.0.ScalarArray.Int64Array.Slice.decMemImpl]

def ScalarArray.Int64Array.Slice.decMem (x : Int64) (s : Int64Array.Slice) : Decidable (x ∈ s)

Decides membership with contains. Logically it decides membership in s.copy.toList, so that decide can evaluate it.

Equations

• ScalarArray.Int64Array.Slice.decMem x s = decidable_of_iff (x ∈ s.copy.toList) ⋯

@[instance_reducible]

instance ScalarArray.Int64Array.instDecidableMemInt64Slice (x : Int64) (s : Int64Array.Slice) : Decidable (x ∈ s)

Equations

• ScalarArray.Int64Array.instDecidableMemInt64Slice x s = ScalarArray.Int64Array.Slice.decMem x s

@[implemented_by _private.ScalarArray.Int64.Decidable.0.ScalarArray.Int64Array.Slice.hashImpl]

def ScalarArray.Int64Array.Slice.hash (s : Int64Array.Slice) : UInt64

The same hash as s.copy, so slices with the same elements have the same hash.

Equations

• s.hash = hash s.copy

@[instance_reducible]

instance ScalarArray.Int64Array.instHashableSlice : Hashable Int64Array.Slice

Equations

• ScalarArray.Int64Array.instHashableSlice = { hash := ScalarArray.Int64Array.Slice.hash }

theorem ScalarArray.Int64Array.Slice.hash_eq_hash_copy (s : Int64Array.Slice) : Hashable.hash s = Hashable.hash s.copy

theorem ScalarArray.Int64Array.Slice.beq_iff_copy_eq {s t : Int64Array.Slice} : (s == t) = true ↔ s.copy = t.copy

instance ScalarArray.Int64Array.instEquivBEqSlice : EquivBEq Int64Array.Slice

instance ScalarArray.Int64Array.instLawfulHashableSlice : LawfulHashable Int64Array.Slice