blob: 6b67785d0bc57e0118e1c6e553099e5281d08393 (
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
|
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
class KnownNat (n :: Nat) where
natSing :: SNat n
class KnownSymbol (n :: Symbol) where
symbolSing :: SSymbol n
data Nat
data SomeNat where
SomeNat :: KnownNat n => (Proxy n) -> SomeNat
data SomeSymbol where
SomeSymbol :: KnownSymbol n => (Proxy n) -> SomeSymbol
data Symbol
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
|