3.4.1 typeclass change

Stream: general

[Kevin Buzzard]

I didn't know what typeclasses were when the 3.4.1 -> 3.4.2 chaos happened. In codewars they want to write def SUBMISSION := ... and if there are any questions about things like rings then I guess they will have to write things like

def SUBMISSION := ∀ (R : Type) [h : comm_ring R], by letI := h; exact <interesting theorem about rings>

Is this "no typeclasses after the colon" issue something which can be "fixed" now?

[Rob Lewis]

Why can't they write def SUBMISSION (R : Type) [h : comm_ring R] : <interesting theorem about rings>?

[Kevin Buzzard]

because SUBMISSION is defined to be the type, not the term.

[Rob Lewis]

def SUBMISSION (R : Type) [h : comm_ring R] : Prop := <interesting theorem about rings>?