SDecide k (KProxy k) => TestEquality k (Sing k) | |
data Sing Bool where | |
data Sing Ordering where | |
data Sing Nat where | |
data Sing Symbol where | |
data Sing () where | |
data Sing Nat where | |
data Sing [a0] where | |
data Sing (Maybe a0) where | |
data Sing (TyFun k1 k2 -> *) = SLambda {} | |
data Sing (Either a0 b0) where | |
data Sing ((,) a0 b0) where | |
data Sing ((,,) a0 b0 c0) where | |
data Sing ((,,,) a0 b0 c0 d0) where | |
data Sing ((,,,,) a0 b0 c0 d0 e0) where- STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
| |
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where- STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
| |
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where- STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0
| |