История изменений

Ты не можешь передать туда true, это не булев тип. Это прям такой тип length xs < length ys. соотвественно туда можно передать только это значение. Если ты его откуда то с собой имеешь, то туда его и пиши, вроде так

(prf, zs) = after xs ys proof_len_xs_lt_len_ys

Если же «с собой» доказательтва нет, то в общем случае надо вызвать ф-цию вычиления длины и создать значение, как-то так (могу ошибиться насчёт congr здесь, но принцип похожий).

lenlt : (xs ys : list a) -> Either (length xs < length ys) (length xs >= length ys)
lenlt [] y::ys = Left (length [] < length (y::ys)
lenlt xs [] =  Right (length xs >= length [])
lenlt x::xs y::ys = congr S (lenlt xs ys)

case lenlt (Cons 1 x) x of
  Left prf => Some (after (Cons 1 x) x prf)
  Right prf => None

Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.

Ты не можешь передать туда true, это не булев тип. Это прям такой тип length xs < length ys. соотвественно туда можно передать только это значение. Если ты его откуда то с собой имеешь, то туда его и пиши, вроде так

(prf, zs) = after xs ys proof_len_xs_lt_len_ys

Если же «с собой» доказательтва нет, то надо вызвать ф-цию вычиления длины и создать значение, как-то так (могу ошибиться насчёт congr здесь, но принцип похожий).

lenlt : (xs ys : list a) -> Either (length xs < length ys) (length xs >= length ys)
lenlt [] y::ys = Left (length [] < length (y::ys)
lenlt xs [] =  Right (length xs >= length [])
lenlt x::xs y::ys = congr S (lenlt xs ys)

case lenlt (Cons 1 x) x of
  Left prf => Some (after (Cons 1 x) x prf)
  Right prf => None

Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.

Ты не можешь передать туда true, это не булев тип. Это прям такой тип length xs < length ys. соотвественно туда можно передать только это значение. Если ты его откуда то с собой имеешь, то туда его и пиши, вроде так

(prf, zs) = after xs ys proof_len_xs_lt_len_ys

Если же «с собой» доказательтва нет, то надо вызвать ф-цию вычиления длины и создать значение, как-то так (могу ошибиться насчёт congr здесь, но принцип похожий).

lenlt : (xs ys : list a) -> Either (length xs < length ys) (length xs >= length ys)
lenlt [] y::ys = Left (length [] < length (y::ys)
lenlt xs [] =  Right (length xs >= length [])
lenlt x::xs y::ys = congr S (lenlt xs ys)

case lenlt xs ys of
  Left prf => Some (after xs ys prf)
  Right prf => None

Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.

Ты не можешь передать туда true, это не будево значение. Это прям такой тип length xs < length ys. соотвественно туда можно передать только это значение. Если ты его откуда то с собой имеешь, то туда его и пиши, вроде так

(prf, zs) = after xs ys proof_len_xs_lt_len_ys

Если же «с собой» доказательтва нет, то надо вызвать ф-цию вычиления длины и создать значение, как-то так (могу ошибиться насчёт congr здесь, но принцип похожий).

lenlt : (xs ys : list a) -> Either (length xs < length ys) (length xs >= length ys)
lenlt [] y::ys = Left (length [] < length (y::ys)
lenlt xs [] =  Right (length xs >= length [])
lenlt x::xs y::ys = congr S (lenlt xs ys)

case lenlt xs ys of
  Left prf => Some (after xs ys prf)
  Right prf => None

Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.