9 lines
134 B
Text
9 lines
134 B
Text
constant A : Type₁
|
|
constant a : A
|
|
constant A_has_add : has_add A
|
|
|
|
check a + a -- ERROR
|
|
|
|
attribute [instance] A_has_add
|
|
|
|
check a + a
|