История изменений
Исправление monk, (текущая версия) :
LH конечно интересная штука, но только если с зависимыми типами не знаком.
Чем? Чтобы вместо {l:[a] | len l = n} писать Vect a n и придумывать по типу на каждое условие?
Исходная версия monk, :
LH конечно интересная штука, но только если с зависимыми типами не знаком.
Чем? Чтобы вместо {l:[a] | len l = n} писать Vect a n и так на каждое условие?