Closed basile-henry closed 7 years ago
The leToPlus function enables the creation of simpler constraints. The SaturatingNum instance for Index has been changed to a weaker constraint: from (KnownNat n, 1 <= (n*2), (n*2) <= (n^2)) to (KnownNat n, 1 <= n).
leToPlus
SaturatingNum
Index
(KnownNat n, 1 <= (n*2), (n*2) <= (n^2))
(KnownNat n, 1 <= n)
Thanks!
The
leToPlus
function enables the creation of simpler constraints. TheSaturatingNum
instance forIndex
has been changed to a weaker constraint: from(KnownNat n, 1 <= (n*2), (n*2) <= (n^2))
to(KnownNat n, 1 <= n)
.