этих Positive, Modulo, Divisible, Even, которые выражаются друг через друга, но используют либо Nat, либо Int (или другие Numeric для вещей типа Positive ), а при этом в refined приняли использовать именно Nat? Правильно я понимаю, что если мне нужны именно Int ы, а то и другие Numeric и, то мне проще иметь свои штуки типа Positive (а то и не париться, и писать тупо Greater[0], если я в 2.13)?
В рефайнд вообще много проблем, Например, для лонгов не выводит ограничения. Ставь ишью @ делай ПР
Обсуждают сегодня