История изменений
Исправление AndreyKl, (текущая версия) :
Ты не можешь передать туда 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
Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.
Исправление AndreyKl, :
Ты не можешь передать туда 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
Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.
Исправление AndreyKl, :
Ты не можешь передать туда 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
Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.
Исходная версия AndreyKl, :
Ты не можешь передать туда 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
Т.е. по русски говоря тебе где-то когда-то придётся вычислить длину и запомнить результат.