@[implicit_reducible]

instance String.instHashableRaw : Hashable Pos.Raw

Equations

• String.instHashableRaw = { hash := String.instHashableRaw.hash }

def String.instHashableRaw.hash : Pos.Raw → UInt64

Equations

• String.instHashableRaw.hash { byteIdx := a } = mixHash 0 (hash a)

def String.instHashablePos.hash {s✝ : String} : s✝.Pos → UInt64

Equations

• String.instHashablePos.hash { offset := a, isValid := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance String.instHashablePos {s✝ : String} : Hashable s✝.Pos

Equations

• String.instHashablePos = { hash := String.instHashablePos.hash }

def String.instHashablePos_1.hash {s✝ : Slice} : s✝.Pos → UInt64

Equations

• String.instHashablePos_1.hash { offset := a, isValidForSlice := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance String.instHashablePos_1 {s✝ : Slice} : Hashable s✝.Pos

Equations

• String.instHashablePos_1 = { hash := String.instHashablePos_1.hash }