AZ
правда представить недетерминистическую чистую функцию чет не получается
Size: a a a
2020 March 25
AZ
Слушай, я не хочу в срач скатываться. Так сделано, заниматься хитроумными оптимизациями на диспатчинге тасков я не занимался. Там всё открыто, код есть.
просто подозрительно
AZ
не огрести бы с либой где себе такое позволяют
AZ
ты говорил код отправишь, а его нте
AZ
Примерам 6 лет
G
Короче, смысл в том, чтобы возвращать не
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
[[Int]], а [GroupedList], где GroupedList - этоrecord GroupedList where
constructor MkGroupedList
start : Int
count : Nat
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
AZ
Короче, смысл в том, чтобы возвращать не
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
[[Int]], а [GroupedList], где GroupedList - этоrecord GroupedList where
constructor MkGroupedList
start : Int
count : Nat
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
а зачем это доказывать?
AZ
или обязательно нужно?
G
а зачем это доказывать?
В Идрис можно подоказывать, но вообще КМК, подход с
GroupedList более самодокументируемыйAZ
В Идрис можно подоказывать, но вообще КМК, подход с
GroupedList более самодокументируемыйон не работает стоит чутка изменить условие, например если разница между числами не больше 3
AZ
а не ровно 1
G
Изменим
GroupedListAZ
каким образом?
AZ
например [2,3,5,6,8,10] подходит под условие
G
Впихнём
step : Nat?G
Только
Nat>0, конечноAZ
Впихнём
step : Nat?тут нет step
G
А мы засунем его
AZ
и какой он будет для списка [2,3,5,6,8,10]?