вообще философия Branded и того примера с Vec n похожая.

The key idea is that'idis notused as a normal lifetime which defines the duration of a borrow, but instead is used as abrandthatuniquelyidentifies a runtime vector value. In other words, for every concrete brand'id, thetypeBrandedVec<'id, T>is a singleton type, inhabited only bythevector (call itbvec) of typeBrandedVec<'id, T>.

Ну вот тебе ещё:
https://www.hardmo.de/article/2021-03-14-zst-proof-types.md#zsts-are-proofs

Мне было бы интересен аналог liquid haskell для раста.

Сейчас из подобного есть только какая-то убогая логика Хоара.

В завтипах n это тоже уникальный тип как и id, который привязан к вектору потом. Только отлчие в том что n это не убогий лайфтайм, а что то с ним можно делать. Я поэтому про него и вспомнил

Которая даже на leftpad'е не работает.

жопа. мои руки меня не слушают

Будет у тебя бренд-вектор и бренд-индекс, гарантия - индекс и вектор должны быть одного бренда, чтобы выполнять совместные операции над ними.
Будет у тебя Vec P, где P - натуральное, гарантия - возврат Vec N, где N - целое неотрицательное.

Плюс к завтипам - можно установить зависимость такую, что P = Succ N

кароче для каждого рантайм значения нужно установить уникальный тип. Потом с ним что то делать. В случае с брандИндекс мало что можно сделать - только сравнить с другим. В случае с Nat (или как там оно) уже можно складывать / вычитать. Собственно делать то что можно делать с нормальными типами в расте. Прикол в том что в расте сделать уникальный тип можно только в домене лайфтаймов. В идрисе в домене обычных типов. Но завтипы не про это имхо.

там на википедии просто Пи и Сигма нотация написано. И про рантайм ничего не сказано)

Завтипы да, шире гораздо, но даже на таком простом примере их сила видна для доказательств

а ты смотре зис вик ов раст *предпоследний? там что то похожее пытались сделать. (я не смотрел)

так, а можно мне поинтер на начало про завтипы?

смысл не с типом

а с тем чтобы хранить предикаты

и автоматом их затягивать

о раскажи. ты должен шарить

если ты в идрисе пишешь:

if (x != 0) {
 ...
}

то внутри ифа у тебя появляется пруф: x != 0