История изменений

не скомпилируется, prf - это будет доказательство того что length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного *ему* первого меньше длинs переданного ему второго (т.е. length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться

не скомпилируется, prf - это будет доказательство того что
length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного *ему* первого меньше длинs переданного ему второго (т.е. length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться

не скомпилируется, prf - это будет доказательство того что
length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного *ему* первого меньше длинs переданного ему второго length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться

не скомпилируется, prf - это будет доказательство того что
length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного ему первого меньше длинs переданного ему второго length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться

не скомпилируется, prf - это будет доказательство того что
length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного ему первого меньше длинs переданного ему второго (length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться