История изменений
Исправление AndreyKl, (текущая версия) :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее. В этом случае компилятор не должен вызывать его в рантайме, так как доказательство не зависит от конкретных параметров.
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
-- библиотечная функция
(zs, prf) = after x (Cons 1 x) len_x_xs
ну и если конкатенация с другим непустым списком - тоже сработает, только функция будет называться length_app что ли.
Исправление AndreyKl, :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее. В этом случае компилятор не должен вызывать его в рантайме, так как доказательство не зависит от конкретных параметров.
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
-- библиотечная функция
(zs, prf) = after x (Cons 1 x) len_x_xs
ну и если вариант - конкатенация с другим непустым списком - тоже сработает, только функция будет называться length_app что ли.
Исправление AndreyKl, :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее. В этом случае компилятор не должен вызывать его в рантайме, так как доказательство не зависит от конкретных параметров.
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
-- библиотечная функция
(zs, prf) = after x (Cons 1 x) len_x_xs
Исправление AndreyKl, :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее. В этом случае компилятор не должен вызывать его в рантайме, так как доказательство не зависит от конкретных параметров.
len_x_xs : {x} -> {xs} -> length x < length (x::xs)
-- библиотечная функция
(zs, prf) = after x (Cons 1 x) len_x_xs
Исправление AndreyKl, :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее
len_x_xs : {x} -> {xs} -> length x < length (x::xs)
-- библиотечная функция
(zs, prf) = after x (Cons 1 x) len_x_xs
Исходная версия AndreyKl, :
Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее
len_x_xs : {x} -> {xs} -> length x < length (x::xs)
-- библиотечная функция
(zs, prf) = after (Cons 1 x) x len_x_xs