История изменений
Исправление AndreyKl, (текущая версия) :
Кстати, ну вроде ничего не мешает написать вот так (в идрисе, но не поручусь за точность синтаксиса, давно не писал на нём).
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf что ли.. вроде как то несложно)
after [] ys _ = ys
Исправление AndreyKl, :
Кстати, ну вроде ничего не мешает написать вот так (в идрисе, но не поручусь за точность синтаксиса, давно не писал на нём).
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (cong S prf что ли)
after [] ys _ = ys
Исправление AndreyKl, :
Кстати, ну вроде ничего не мешает написать вот так (в идрисе, но не поручусь за точность синтаксиса, давно не писал на нём).
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) _ = after xs ys
after [] ys _ = ys
Исходная версия AndreyKl, :
Кстати, ну вроде ничего не мешает написать вот так
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) = after xs ys
after [] ys = ys