MK
А что, агда мощнее идриса?
Size: a a a
2020 November 20
MK
Опять в Питер летишь?
AV
Мне кажется, что да
AV
DB
Из наличия NotZero n ~ True в контексте не выведется невозможность кейса кажется
Ну если слифтить значение в тип как-то, то нельзя будет передать туда, где у тебя такой контекст, нолек
DB
type family NotZero (a :: Nat) :: Bool
Знаешь, как можно Int в тип слифтить?
DB
Опять в Питер летишь?
Ну моднее, как минимум. Я пытался начать чо-то в нём разбираться, а они там даже в коде юникодом пишут. Хипстота(
DB
никак
sad
DB
если это известный литерал, то просто @1 скажем
а (-1)?
AV
страдай
DB
страдай
за чьто
AV
(@True, @1)
DB
(@True, @1)
sooo safe
MK
(@True, @1)
Потом до дедекиндовых сечений дойдёшь?
A
(@True, @1)
о, я похожим образом значения от 0 до 1 мутил, кажется
AV
ты ещё 2.718281828459045 попроси
a
А что, агда мощнее идриса?
allow me to introduce myself
к
а (-1)?
нет, вынести терм на тайплевел в хаскеле нельзя, но можно заранее иметь термы, которые однозначно выводимы из типа, сигнлтон типы иметь то есть