r
В то время google ещё не выставлял их в аренду
Size: a a a
2020 June 27
DF
Понятно😊
AZ
Кто офигенно в рекурсии шарит, а то я че-то не очень могу понять как оно работает
AZ
red75prime ты вроде в синтаксисе идриса разбираешься, может подскажешь?
AZ
мне вот этот counter ваще неясен
DF
Вроде объясняется деструктуризацией тут
DF
Как способ скипнуть два элемента
DF
Но я к сожалению не знаю Идрис
DF
Гиролот должен шарить
AZ
мне не очень понятно как пропуская первые 2 элемента при деструктуризации мы разбиваем список пополам
DF
А что значит следующий аргумент item :: items? Оно что два списка принимает?
AZ
а всё лол понял
AZ
Dollar Føølish
А что значит следующий аргумент item :: items? Оно что два списка принимает?
это деструктуризация
AZ
||| Generic lists
data List : (elem : Type) -> Type where
||| Empty list
Nil : List elem
||| A non-empty list, consisting of a head element and the rest of
||| the list.
(::) : (x : elem) -> (xs : List elem) -> List elemAZ
(::) это значит инфиксная функция с именем ::
AZ
item :: items соответственно item : elem, items : List elem
DF
Так а перед ним же уже есть аргументы , то есть чупакабра с каунтером
DF
Ну в общем мне надо знать синтаксис Идриса чтобы такие вопросы не задавать
AZ
ну растовый синтаксис ты знаешь?