blob: 0e9913966f06070cc93388e6654daf3790af6865 (
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
38
39
40
41
42
43
44
45
|
type family (*) (a :: Nat) (b :: Nat)
Kind: Nat -> Nat -> Nat
type family (+) (a :: Nat) (b :: Nat)
Kind: Nat -> Nat -> Nat
type family (-) (a :: Nat) (b :: Nat)
Kind: Nat -> Nat -> Nat
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True
type family (<=?) (a :: Nat) (b :: Nat)
Kind: Nat -> Nat -> Bool
type family CmpNat (a :: Nat) (b :: Nat)
Kind: Nat -> Nat -> Ordering
type family CmpSymbol (a :: Symbol) (b :: Symbol)
Kind: Symbol -> 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)
Kind: forall b1. ErrorMessage -> b1
type family (^) (a :: Nat) (b :: Nat)
Kind: Nat -> 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
|
