blob: c64f4899b41041e71fd817916f1787870bec4343 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}
module T6036 where
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing 'Nothing
SJust :: Sing b -> Sing ('Just b)
data Nat = Zero | Succ Nat
data instance Sing (a :: Nat) where
SZero :: Sing Zero
SSucc :: Sing n -> Sing (Succ n)
term = SJust SZero
|
