Hashable Subtype

Stream: lean4

[Marcus Rossel]

Is this a bad idea?:

instance [Hashable α] {p : α → Prop} : Hashable { a : α // p a } where
  hash a := hash a.val

If not, how/where would this make its way into Lean?

[Mario Carneiro]

Seems fine to me

[Mario Carneiro]

It would presumably go next to the other basic instances defined after docs4#Hashable

[Marcus Rossel]

Mario Carneiro said:

It would presumably go next to the other basic instances defined after docs4#Hashable

Is this page (https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Hashable#doc) completely blank for anyone else on Safari (mobile and desktop)?
Weirdly https://leanprover-community.github.io/mathlib4_docs/ works for me.

[Marcus Rossel]

Update: #1153