Equations
- instHashableNat = { hash := fun n => UInt64.ofNat n }
Equations
- instHashablePos = { hash := fun p => UInt64.ofNat p.byteIdx }
Equations
- instHashableBool = { hash := fun _fun_discr => match _fun_discr with | true => 11 | false => 13 }
Equations
- instHashableList = { hash := fun as => List.foldl (fun r a => mixHash r (hash a)) 7 as }
Equations
- instHashableArray = { hash := fun as => Array.foldl (fun r a => mixHash r (hash a)) 7 as 0 (Array.size as) }
Equations
- instHashableUInt8 = { hash := fun n => UInt8.toUInt64 n }
Equations
- instHashableUInt16 = { hash := fun n => UInt16.toUInt64 n }
Equations
- instHashableUInt32 = { hash := fun n => UInt32.toUInt64 n }
Equations
- instHashableUInt64 = { hash := fun n => n }
Equations
- instHashableUSize = { hash := fun n => USize.toUInt64 n }
Equations
- instHashableFin = { hash := fun v => Nat.toUInt64 v.val }
Equations
- instHashableInt = { hash := fun _fun_discr => match _fun_discr with | Int.ofNat n => UInt64.ofNat (2 * n) | Int.negSucc n => UInt64.ofNat (2 * n + 1) }
Equations
- instHashable P = { hash := fun x => 0 }