max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Hashable for Subtype

Browse source
This commit is contained in:
Marcus Rossel 2022-08-31 13:38:55 +02:00 • committed by Leonardo de Moura
parent d96bf8a633
commit a2a39882d5
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Prelude.lean
View file

@ -3244,6 +3244,9 @@ def USize.toUInt64 (u : USize) : UInt64 where
@[extern "lean_uint64_mix_hash"]
opaque mixHash (u₁ u₂ : UInt64) : UInt64
instance [Hashable α] {p : α → Prop} : Hashable (Subtype p) where
hash a := hash a.val
/-- A opaque string hash function. -/
@[extern "lean_string_hash"]
protected opaque String.hash (s : @& String) : UInt64