Телеграмм чат группы haskellru страница 14673

В GHC есть Nat же

22:08пожаловаться #1

зачем изобретать

22:08пожаловаться #2

И как ты туда /= 0 засунешь?

22:08пожаловаться #3

Они не индуктивные

22:08пожаловаться #4

решил в 19 строк с сигнатурами

22:09пожаловаться #5

скидывать я так понимаю нельзя

22:09пожаловаться #6

скину в лс саше

22:09пожаловаться #7

ага, давай

22:09пожаловаться #8

Блин, чо-то реально хз, как Int лифтануть в тип..

22:12пожаловаться #9

Alexander Vershilov

И как ты туда /= 0 засунешь?

NotZero n ~ True => ...

type family NotZero a where 
 NotZero 0 = 'False
 NotZero n = 'True

22:13пожаловаться #10

только надо как-то kind указать для a

22:13пожаловаться #11

(a :: Nat) же можно?

22:13пожаловаться #12

Или так не проканает?

22:14пожаловаться #13

проканает

22:15пожаловаться #14

type family NotZero (a :: Nat) :: Bool

22:16пожаловаться #15

Из наличия NotZero n ~ True в контексте не выведется невозможность кейса кажется

22:17пожаловаться #16

Maxim Koltsov in Haskell

Хаскель вам не агда

22:17пожаловаться #17

вот это вот,

22:18пожаловаться #18

даже не идрис

22:18пожаловаться #19

блин мне вставать в 5, а я ещё не дома 🙁