mine instance lacking? #1729
Description
analysis/reals/constructive_ereal.v
Line 2740 in c55da8c
HB.instance Definition _ :=
Monoid.isLaw.Build (\bar R) +oo mine minA minye miney.{{ message }}
analysis/reals/constructive_ereal.v
Line 2740 in c55da8c
HB.instance Definition _ :=
Monoid.isLaw.Build (\bar R) +oo mine minA minye miney.