H
может и так работает? я хз
Size: a a a
2020 August 02
AZ
Утверждают, что это валидный код
mutual
even : Nat -> Bool
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
Вот так имхо понятнееYS
Что за идрис?
Язык, похожий на хаскель
AZ
но с where скорее всего тоже работать будет
X
Язык, похожий на хаскель
Написанный на расте?
AZ
Написанный на расте?
на лиспе по-моему
YS
Нет, на диалекте лиспа
H
на идрисе же
YS
на лиспе по-моему
есть на рокете, и ещё что-то
AZ
может и так работает? я хз
я думаю оно и так работает, но odd снаружи недоступен
H
я думаю оно и так работает, но odd снаружи недоступен
+
YS
на идрисе же
Его позже переписали
AZ
а чтобы был доступен нужен mutual
H
первый идрис на хучкиле видел
AZ
короче компилятор видит что сходится к базовому кейсу Z и всё
AZ
вот с интами такое бы наверное не прокатило
YS
первый идрис на хучкиле видел
Блин, у меня первый скачан
AZ
у меня оже первый. я не разобрался как второй ставить
AZ
для второго нужна схема
AZ
но мне и первый норм, он только местами тупит, зато книжка соответствует