blob: 15504ec324a431ce43a3894e6f9dc8e02d28ffa0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
type family (*) (a :: Nat) (b :: Nat) :: Nat
type family (+) (a :: Nat) (b :: Nat) :: Nat
type family (-) (a :: Nat) (b :: Nat) :: Nat
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True
type family (<=?) (a :: Nat) (b :: Nat) :: Bool
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering
type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering
data ErrorMessage where
Text :: Symbol -> ErrorMessage
ShowType :: t -> ErrorMessage
(:<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
(:$$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
class KnownNat (n :: Nat) where
natSing :: SNat n
{-# MINIMAL natSing #-}
class KnownSymbol (n :: Symbol) where
symbolSing :: SSymbol n
{-# MINIMAL symbolSing #-}
data SomeNat where
SomeNat :: KnownNat n => (Proxy n) -> SomeNat
data SomeSymbol where
SomeSymbol :: KnownSymbol n => (Proxy n) -> SomeSymbol
type family TypeError (a :: ErrorMessage) :: b where
type family (^) (a :: Nat) (b :: Nat) :: Nat
natVal :: KnownNat n => proxy n -> Integer
natVal' :: KnownNat n => Proxy# n -> Integer
sameNat ::
(KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol ::
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
someNatVal :: Integer -> Maybe SomeNat
someSymbolVal :: String -> SomeSymbol
symbolVal :: KnownSymbol n => proxy n -> String
symbolVal' :: KnownSymbol n => Proxy# n -> String
data Nat
data Symbol
|
