Why does rationals_le use the concrete type nat?
Opened this issue · 1 comments
langston-barrett commented
I was surprised when unfolding rationals_le
to see that it specifies that le x y
if there is a fraction p/q
made of nat
s such that y=x+p/q
:
Instance rationals_le `{Rationals Q} : Le Q | 10 := λ x y,
∃ num, ∃ den, y = x + naturals_to_semiring nat Q num / naturals_to_semiring nat Q den.
Why not use any type that is an instance of Naturals
?
spitters commented
I agree. It seems better to generalize this to general instances.