p
давно не банили за экстримизм тут?
расист
Size: a a a
2020 June 07
Т8
#AlienLivesMatter
лол, я не видел, что ещё отписались😁
AZ
я вообще не так задачу понял
AZ
vectTake : (m: Nat) -> Vect n a -> Vect (minimum m n) a
vectTake Z _ = []
vectTake m [] = rewrite minimumZeroZeroLeft m in []
vectTake (S k) (x :: xs) = x :: vectTake k xs
Ты ж помнишь)Т8
давно не банили за экстримизм тут?
э... Щас такое время, что трудно отличить сарказм от серьёзки
AZ
и общий совет для натуральных чисел вместо плюсика использовать конструктор S
G
и общий совет для натуральных чисел вместо плюсика использовать конструктор S
+
p
я уже понял, да. у меня почти ничего с плюсиком какого-то хрена не компилировалось.
G
Плюсик бывает не редуцируется
AZ
я уже понял, да. у меня почти ничего с плюсиком какого-то хрена не компилировалось.
кстати на матлогике мы проходили арифметику пеано, так что изи вкатился
G
1 + n редуцируется
G
Но вообще просто
S n пишутAZ
1 + n редуцируется
VS
VS
Наркоманы блять 😁
Т8
норм. Идея с автоматическим Box<dyn Error> везде и синтаксисом потипу экспешинов - гуд. Это конешно не оч годится для "хочу чтоб было системно", но для системности у них есть эксплицитный -> Result<T,E>.
это самое удобное, что ты видел? Невзирая на применимость в системном
p
самое удобное по идеи с алгебраическими эффектами, но это не точно
VS
@enomad Это твоя фотка у тебя на гитхабе? Ты такой сладкий пирожочек. Ми ми ми милота 😁