AV
a*b
Size: a a a
2020 November 20
DB
Ну могу и через честные gadt c доказательствами
отсортированность списка через гадт?
AV
DB
прям списка? как?
DB
я чо-то даже не представляю
AV
Сложно, но можно потаскать все словарики
DB
а што есть словарики?
DB
Это те Dict?
AV
Да, структуры таскающие с собой информацию об ограничениях
AV
Вообще инетерсно у меня data Q = Q [Z], так вот в Z сам по себе может иметь коэффициент 0, а в Q уже нет
DB
(я не понял)
AV
ааа, есть код вида:
go t [] = [t]
go t [x] = [f t x]
go t (x0:x1:xs) = f t x0 : go x1 xs
go t [] = [t]
go t [x] = [f t x]
go t (x0:x1:xs) = f t x0 : go x1 xs
AV
Очевидно, что он возвращает непустой список, а как сделать так, чтобы тут адеватно возвращалось NonEmpty
AV
Но порядок желательно сохранять
AV
go t [] = (t:|[], [t])
go t [a0] = (f t a0:|[], [f t a0])
go t (a0:a1:as) =
let tl = snd $ go a1 as
in (f t a0 😐 tl, f t a0:tl)AV
что получше есть?
DB
Очевидно, что он возвращает непустой список, а как сделать так, чтобы тут адеватно возвращалось NonEmpty
Да просто продложить другой функцией
go?DB
go'