История изменений
Исправление AndreyKl, (текущая версия) :
А если не библиотечная?
Я упоминаю в том смысле что писать вроде не надо, это всё есть. А так - всё равно.
addElem:: a -> {x:List a | length x > 0} -> {r:List a|length r > length x}
Кажется требование length x > 0 лишнее. Как то вот так
addElem : a -> (x : List a) -> (r:List a ** length r > length x)
addElem a x = (Cons a x, len_x_xs)
если всё таки с требованием, то вот так
addElem : a -> (x : List a) -> (length x > 0) -> (r:List a ** length r > length x)
addElem a x _ = (Cons a x, len_x_xs)
Исправление AndreyKl, :
А если не библиотечная?
Я упоминаю в том смысле что писать вроде не надо, это всё есть. А так - всё равно.
addElem:: a -> {x:List a | length x > 0} -> {r:List a|length r > length x}
Кажется требование length x > 0 лишнее. Как то вот так
addElem : a -> (x : List a) -> (r:List a ** length r > length x)
addElem a x = (Cons a x, len_x_xs)
если всё таки с требованием, то вот так
addElem : a -> (x : List a) -> (length xs > 0) -> (r:List a ** length r > length x)
addElem a x _ = (Cons a x, len_x_xs)
Исходная версия AndreyKl, :
А если не библиотечная?
Я упоминаю в том смысле что писать вроде не надо, это всё есть. А так - всё равно.
addElem:: a -> {x:List a | length x > 0} -> {r:List a|length r > length x}
Кажется требование length x > 0 лишнее. Как то вот так
addElem : a -> (x : List a) -> (r:List a ** length r > length x)
addElem a x = (Cons a x, len_x_xs)