2 Jan
2019
2 Jan
'19
9:32 a.m.
This question has been answered on Stack Overflow.
2019년 1월 2일 (수) 오후 5:48, Dannyu NDos
(Message re-sent) Hi everyone. I'm not so skillful with GADTs and DataKinds, so I assume this mailing list is appropriate to post on.
Basically, I wanted to do GADT like this (involving GHC.TypeNats):
data Symmetric (n :: Nat) where S1 :: Symmetric 1 (:.) :: (KnownNat n, 2 <= n) => Cyclic n -> Symmetric (n-1) -> Symmetric n
But I had some issues with this. The full question is here (on Stack Overflow):
https://stackoverflow.com/q/54000646/4540658
Sincerely, Dannyu NDos