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
(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
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
participants (1)
-
Dannyu NDos