[
Если ты сам не сравниваешь, то у тебя частичная функция
Size: a a a
2021 May 31
AN
Я думал оно выпиливается и остаётся только само значение а не пределы.
[
У меня сам Fin это и есть число пиано
gо
А зачем? Нельзя просто баунд поставить?
[
FS(FS(FS(FS(FZ))))
gо
И хранить внутри просто настоящий Nat
[
[
Это пример из доки
[
Можно вообще убрать нахуй фин и сделать так
index : (n : Nat) -> Vect (n+1+m) a -> a
index : (n : Nat) -> Vect (n+1+m) a -> a
[
И никакие Fin не нужны
AN
Ааа... Мой мозг. Почему это лучше просто проверки индекса в расте
gо
Потому что она заэнфоршена в компайл-тайме
gо
У тебя никогда не будет паники от неверного индекса, потому что операция получения от неверного индекса просто не определена
AN
Вот decEq мне понятно. Даже поверил бы что есть decLess. А это какой то взрыв мозга. Как можно неизвестные значения структурно матчить.
gо
Завтипы
gо
<конец агитки>
У тебя также никогда не будет неверного индекса в Rust, если ты просто будешь всегда использовать
У тебя также никогда не будет неверного индекса в Rust, если ты просто будешь всегда использовать
.get(), а не квадратные скобкиAN
Пфф... Но вот я создал вектор, создал число. Очевидно что их надо сравнить. В какой момент это происходит? Как вызвать эту функцию?
AN
А get типа option возвращает?
TK
get возвращает не то, что нужно
gо