Operators for Prop

Stream: lean4

[Francisco Giordano]

Is there a reason why all the operator typeclasses (e.g., HAppend) are defined for Type and not for Sort, meaning that they can't be instanced for Prop types?

[Yaël Dillies]

What would your use case be? Do you want to append propositions?

[Eric Wieser]

Occasionally it's tempting to define hx + hy : P (x + y) for hx : P x and hy : P y

[Francisco Giordano]

I just want the notation ++ for a specific proposition I've defined. In this case I want hAppend for a proposition with a non-proposition, so more like hx ++ fy : P (x ++ y) with hx : P x, fy : T y

[Francisco Giordano]

I could redefine the ++ notation or use a different symbol. But I'm not sure why there is this limitation