DS
вот идрису это неочевидно, нужно сидеть и писать доказательство, что сплит даёт половинки, которые в сумме дадут исходный список
Тебе надо было в агду смотреть, там большая часть этого в стд либе есть
Size: a a a
2020 June 27
AZ
Тебе надо было в агду смотреть, там большая часть этого в стд либе есть
или пример с множеством
AZ
я ебался неделю чтобы сделать удаление элемента из множества
AZ
хотите ответ, как надо было сделать?
AZ
вот так блин
AZ
элементарно и изящно
AZ
это начиналось с
removeElemFromSet :
(value : a) ->
(xs : Vect (S n) a) ->
Elem value xs ->
Set xs ->
(ys : Vect n a ** (Set ys, Not (Elem value ys)))
Если кто не догадалсяDS
или пример с множеством
Ну эт нормально, пока руку не набьешь.
Это же конструктивные доказательства, штука редкая, нигде не учат
Это же конструктивные доказательства, штука редкая, нигде не учат
AZ
вот я не знаю где учиться
AZ
самому - я видимо слишком тупой
AZ
а книжек/обучалок такому тупо нет
AZ
только остается сидеть в чате и выпрашивать объяснение того или иного момента
AZ
энивей
Z
это как пытаться в динамике юзать синглтоны и di
di в смысле di-фреймворки? и иммутабельность ортогональна системе типов
AZ
я ощутил что ощущают динамисты
AZ
правда по мейнстрим типизации есть и книжки, и люди которые помогут
AZ
в общем, типчики помогают, если не тупить. А нетупить это то чему нужно учиться
SP
чтобы учиться нужно понять что это полезно а они не понимают
SP
ну голдштейна случай правда какое то очень странное исключение