Topic: HasEquiv in Type?
Jason Gross (Mar 11 2021 at 21:01):
Is there a reason that
HasEquiv in the standard library uses
Prop rather than
Sort _? I'd like to be able to use
≈ with relations that live in
Mario Carneiro (Mar 12 2021 at 02:27):
Do we have universe out-params? That seems like a prerequisite for this to work
Jason Gross (Mar 12 2021 at 14:23):
I think it already works. That is to say, I've had no trouble with
class HasArr (α : Sort u1) where Arr : α → α → Sort u2 infix:70 " ~> " => HasArr.Arr
Leonardo de Moura (Mar 13 2021 at 15:06):
@Mario Carneiro We have modified the typeclass resolution procedure a few weeks ago. All universes are out-param by default now like in Lean 3.
Jason Gross (Mar 15 2021 at 17:48):
Last updated: May 07 2021 at 12:15 UTC