Equations
- instHashableNat = { hash := fun (n : Nat) => UInt64.ofNat n }
Equations
- instHashablePos = { hash := fun (p : String.Pos) => UInt64.ofNat p.byteIdx }
Equations
- instHashableUInt8 = { hash := fun (n : UInt8) => UInt8.toUInt64 n }
Equations
- instHashableUInt16 = { hash := fun (n : UInt16) => UInt16.toUInt64 n }
Equations
- instHashableUInt32 = { hash := fun (n : UInt32) => UInt32.toUInt64 n }
Equations
- instHashableUInt64 = { hash := fun (n : UInt64) => n }
Equations
- instHashableUSize = { hash := fun (n : USize) => USize.toUInt64 n }
Equations
- instHashableFin = { hash := fun (v : Fin n) => Nat.toUInt64 ↑v }
Equations
- instHashableInt = { hash := fun (x : Int) => match x with | Int.ofNat n => UInt64.ofNat (2 * n) | Int.negSucc n => UInt64.ofNat (2 * n + 1) }
Equations
- instHashable P = { hash := fun (x : P) => 0 }