История изменений
Исправление AndreyKl, (текущая версия) :
По моим личным впечатлениям, вектор немного неуклюжий. Но для данного случая довольно несложно выглядит:
after :: (n < m) -> Vect a n -> Vect b m -> Vect b (m - n)
А на LH основная проблема в том, что солвер плохо работает с рекурсивными условиями.
Дело в том что система неразрешима (а если ограничить её до разрешимой, то она будет неинтересна.. т.е. что то нетривиальное не выразишь) и поэтому солвер всегда будет работать плохо.
Исправление AndreyKl, :
По моим личным впечатлениям, вектор немного неуклюжий. Но для данного случая вообще то всё довольно несложно выглядит:
after :: (n < m) -> Vect a n -> Vect b m -> Vect b (m - n)
А на LH основная проблема в том, что солвер плохо работает с рекурсивными условиями.
Дело в том что система неразрешима (а если ограничить её до разрешимой, то она будет неинтересна.. т.е. что то нетривиальное не выразишь) и поэтому солвер всегда будет работать плохо.
Исходная версия AndreyKl, :
По моим личным впечатлениям, вектор немного неуклюжий. Но для данного случая вообще то всё довольно несложно выглядит:
after :: (n < m) -> Vect a n -> Vect b m -> Vect b (m - n)
А на LH основная проблема в том, что солвер плохо работает с рекурсивными условиями.
Дело в том что система неразрешима (а если ограничить её до разрешимой, то она будет неинтересна.. т.е. что то нетривиальное не выразишь) и поэтому солвер всегда будет работать плохо.