Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data (a :: k) :~: (b :: k) where
- withRefl :: forall k (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r
- asProxyTypeOf :: a -> proxy a -> a
- data Proxy (t :: k) = Proxy
- data KProxy t = KProxy
- class KnownNat (n :: Nat)
- data Nat
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- type family Log2 (a :: Nat) :: Nat where ...
- someNatVal :: Natural -> SomeNat
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True
- withSingI :: forall k (n :: k) r. Sing n -> (SingI n => r) -> r
- type family Demote k = (r :: Type) | r -> k
- type family Sing :: k -> Type
- class SingI (a :: k) where
- class SingKind k where
- data SomeSing k where
- pattern (:<) :: (Dom f a, KnownNat n, CFreeMonoid f) => (n ~ (1 + n1), KnownNat n1) => a -> Sized f n1 a -> Sized f n a
- pattern (:>) :: (Dom f a, KnownNat n, CFreeMonoid f) => (n ~ (n1 + 1), KnownNat n1) => Sized f n1 a -> a -> Sized f n a
- pattern Nil :: forall f n a. (KnownNat n, CFreeMonoid f, Dom f a) => n ~ 0 => Sized f n a
- generate :: forall (f :: Type -> Type) (n :: Nat) a. (CFreeMonoid f, Dom f a) => SNat n -> (Ordinal n -> a) -> Sized f n a
- sIndex :: forall (f :: Type -> Type) (n :: Nat) c. (CFoldable f, Dom f c) => Ordinal n -> Sized f n c -> c
- singleton :: forall (f :: Type -> Type) a. (CPointed f, Dom f a) => a -> Sized f 1 a
- unsafeFromList :: forall (f :: Type -> Type) (n :: Nat) a. (CFreeMonoid f, Dom f a) => SNat n -> [a] -> Sized f n a
- unsafeFromList' :: forall (f :: Type -> Type) (n :: Nat) a. (KnownNat n, CFreeMonoid f, Dom f a) => [a] -> Sized f n a
- zipWithSame :: forall (f :: Type -> Type) (n :: Nat) a b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
- viewNat :: forall (n :: Nat). SNat n -> ZeroOrSucc n
- type Pred (n :: Nat) = n - 1
- data SNat (n :: Nat) where
- type (<) (n :: Nat) (m :: Nat) = (n <? m) ~ 'True
- type Succ (n :: Nat) = n + 1
- type (-.) (n :: Nat) (m :: Nat) = Subt n m (m <=? n)
- type S (n :: Nat) = Succ n
- type Min (n :: Nat) (m :: Nat) = MinAux (n <=? m) n m
- withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
- toNatural :: forall (n :: Nat). SNat n -> Natural
- sNatP :: forall (n :: Nat) pxy. KnownNat n => pxy n -> SNat n
- snat :: QuasiQuoter
- toSomeSNat :: Natural -> SomeSNat
- withSNat :: Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
- (%*) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
- (%+) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
- (%-) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
- (%<=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
- (%^) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m)
- sCmpNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m)
- sCompare :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m)
- sDiv :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Div n m)
- sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord)
- sLog2 :: forall (n :: Nat). SNat n -> SNat (Log2 n)
- sMod :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Mod n m)
- sNat :: forall (n :: Nat). KnownNat n => SNat n
- sOne :: SNat 1
- sPred :: forall (n :: Nat). SNat n -> SNat (Pred n)
- sS :: forall (n :: Nat). SNat n -> SNat (Succ n)
- sSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
- sZero :: SNat 0
- induction :: forall p (k :: Nat). p 0 -> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
- zeroOrSucc :: forall (n :: Nat). SNat n -> ZeroOrSucc n
- (%-.) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
- (%<?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
- (%>=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m)
- (%>?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >? m)
- sMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
- sMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
- data SomeSNat where
- type family (a :: k) === (b :: k) :: Bool where ...
- data Equality (n :: k) (m :: k) where
- type family FlipOrdering (ord :: Ordering) :: Ordering where ...
- type One = 1
- data SBool (b :: Bool) where
- data SOrdering (ord :: Ordering) where
- type Zero = 0
- data ZeroOrSucc (n :: Nat) where
- IsZero :: ZeroOrSucc 0
- IsSucc :: forall (n1 :: Nat). SNat n1 -> ZeroOrSucc (n1 + 1)
- type (<?) (n :: Nat) (m :: Nat) = (n + 1) <=? m
- type (>) (n :: Nat) (m :: Nat) = (n >? m) ~ 'True
- type (>=) (n :: Nat) (m :: Nat) = (n >=? m) ~ 'True
- type (>=?) (n :: Nat) (m :: Nat) = m <=? n
- type (>?) (n :: Nat) (m :: Nat) = m <? n
- type Max (n :: Nat) (m :: Nat) = MaxAux (n >=? m) n m
- data IsTrue (b :: Bool) where
- withWitness :: forall (b :: Bool) r. IsTrue b -> (b ~ 'True => r) -> r
- (===) :: forall k eq (x :: k) (y :: k) (z :: k). Equality eq => eq x y -> Reason eq y z -> eq x z
- (=~=) :: forall k1 k2 r (x :: k1) (y :: k2) proxy. r x y -> proxy y -> r x y
- because :: forall k1 k2 proxy (y :: k1) eq (x :: k2). proxy y -> eq x y -> Reason eq x y
- coerce :: forall k (a :: k) (b :: k) f. (a :=: b) -> f a -> f b
- start :: forall k eq proxy (a :: k). Preorder eq => proxy a -> eq a a
- type family Flipped f a :: Nat -> Type where ...
- type Sized' n a = Sized Seq n a
- type Sized n a = Sized Vector n a
- type USized n a = Sized Vector n a
- pattern Flipped :: Sized f n a -> Flipped f a n
- toProxy :: a -> Proxy a
- sNatToSingleton :: SNat n -> Sing n
- singToSNat :: Sing n -> SNat n
- coerceLength :: (n :~: m) -> Sized f n a -> Sized f m a
- sizedLength :: (KnownNat n, DomC f a) => Sized f n a -> SNat n
- padVecs :: forall a n m. (Unbox a, KnownNat n, KnownNat m) => a -> USized n a -> USized m a -> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
- sNatToInt :: SNat n -> Int
Documentation
data (a :: k) :~: (b :: k) where infix 4 #
Propositional equality. If a :~: b
is inhabited by some terminating
value, then the type a
is the same as the type b
. To use this equality
in practice, pattern-match on the a :~: b
to get out the Refl
constructor;
in the body of the pattern-match, the compiler knows that a ~ b
.
Since: base-4.7.0.0
Instances
Equality ((:=:) :: k -> k -> Type) | |
Defined in Proof.Equational symmetry :: forall (a :: k0) (b :: k0). (a :=: b) -> b :=: a | |
Preorder ((:=:) :: k -> k -> Type) | |
Defined in Proof.Equational reflexivity :: forall proxy (a :: k0). proxy a -> a :=: a transitivity :: forall (a :: k0) (b :: k0) (c :: k0). (a :=: b) -> (b :=: c) -> a :=: c | |
Semigroupoid ((:~:) :: k -> k -> Type) | |
Defined in Data.Semigroupoid | |
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
Eq (a :~: b) | Since: base-4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # | |
Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
Show (a :~: b) | Since: base-4.7.0.0 |
NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint |
asProxyTypeOf :: a -> proxy a -> a #
asProxyTypeOf
is a type-restricted version of const
.
It is usually used as an infix operator, and its typing forces its first
argument (which is usually overloaded) to have the same type as the tag
of the second.
>>>
import Data.Word
>>>
:type asProxyTypeOf 123 (Proxy :: Proxy Word8)
asProxyTypeOf 123 (Proxy :: Proxy Word8) :: Word8
Note the lower-case proxy
in the definition. This allows any type
constructor with just one argument to be passed to the function, for example
we could also write
>>>
import Data.Word
>>>
:type asProxyTypeOf 123 (Just (undefined :: Word8))
asProxyTypeOf 123 (Just (undefined :: Word8)) :: Word8
Proxy
is a type that holds no data, but has a phantom parameter of
arbitrary type (or even kind). Its use is to provide type information, even
though there is no value available of that type (or it may be too costly to
create one).
Historically,
is a safer alternative to the
Proxy
:: Proxy
a
idiom.undefined
:: a
>>>
Proxy :: Proxy (Void, Int -> Int)
Proxy
Proxy can even hold types of higher kinds,
>>>
Proxy :: Proxy Either
Proxy
>>>
Proxy :: Proxy Functor
Proxy
>>>
Proxy :: Proxy complicatedStructure
Proxy
Instances
Generic1 (Proxy :: k -> Type) | Since: base-4.6.0.0 |
FoldableWithIndex Void (Proxy :: Type -> Type) | |
FunctorWithIndex Void (Proxy :: Type -> Type) | |
TraversableWithIndex Void (Proxy :: Type -> Type) | |
Defined in Control.Lens.Indexed itraverse :: Applicative f => (Void -> a -> f b) -> Proxy a -> f (Proxy b) itraversed :: IndexedTraversal Void (Proxy a) (Proxy b) a b | |
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Foldable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Defined in Data.Foldable fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> m # foldMap' :: Monoid m => (a -> m) -> Proxy a -> m # foldr :: (a -> b -> b) -> b -> Proxy a -> b # foldr' :: (a -> b -> b) -> b -> Proxy a -> b # foldl :: (b -> a -> b) -> b -> Proxy a -> b # foldl' :: (b -> a -> b) -> b -> Proxy a -> b # foldr1 :: (a -> a -> a) -> Proxy a -> a # foldl1 :: (a -> a -> a) -> Proxy a -> a # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # | |
Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Contravariant (Proxy :: Type -> Type) | |
Eq1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Ord1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Read1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Show1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
NFData1 (Proxy :: Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
Hashable1 (Proxy :: Type -> Type) | |
Defined in Data.Hashable.Class | |
Representable (Proxy :: Type -> Type) | |
Apply (Proxy :: Type -> Type) | |
Bind (Proxy :: Type -> Type) | |
Adjustable (Proxy :: Type -> Type) | |
FoldableWithKey (Proxy :: Type -> Type) | |
Defined in Data.Key toKeyedList :: Proxy a -> [(Key Proxy, a)] foldMapWithKey :: Monoid m => (Key Proxy -> a -> m) -> Proxy a -> m foldrWithKey :: (Key Proxy -> a -> b -> b) -> b -> Proxy a -> b foldlWithKey :: (b -> Key Proxy -> a -> b) -> b -> Proxy a -> b | |
Indexable (Proxy :: Type -> Type) | |
Keyed (Proxy :: Type -> Type) | |
Defined in Data.Key mapWithKey :: (Key Proxy -> a -> b) -> Proxy a -> Proxy b | |
Lookup (Proxy :: Type -> Type) | |
TraversableWithKey (Proxy :: Type -> Type) | |
Defined in Data.Key traverseWithKey :: Applicative f => (Key Proxy -> a -> f b) -> Proxy a -> f (Proxy b) mapWithKeyM :: Monad m => (Key Proxy -> a -> m b) -> Proxy a -> m (Proxy b) | |
Zip (Proxy :: Type -> Type) | |
ZipWithKey (Proxy :: Type -> Type) | |
PFoldable (Proxy :: Type -> Type) | |
Defined in Data.Singletons.Prelude.Foldable type Fold arg :: m type FoldMap arg arg1 :: m type Foldr arg arg1 arg2 :: b type Foldr' arg arg1 arg2 :: b type Foldl arg arg1 arg2 :: b type Foldl' arg arg1 arg2 :: b type Foldr1 arg arg1 :: a type Foldl1 arg arg1 :: a type ToList arg :: [a] type Null arg :: Bool type Length arg :: Nat type Elem arg arg1 :: Bool type Maximum arg :: a type Minimum arg :: a type Sum arg :: a type Product arg :: a | |
SFoldable (Proxy :: Type -> Type) | |
Defined in Data.Singletons.Prelude.Foldable sFold :: forall m (t1 :: Proxy m). SMonoid m => Sing t1 -> Sing (Apply FoldSym0 t1) sFoldMap :: forall a m (t1 :: a ~> m) (t2 :: Proxy a). SMonoid m => Sing t1 -> Sing t2 -> Sing (Apply (Apply FoldMapSym0 t1) t2) sFoldr :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Proxy a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply FoldrSym0 t1) t2) t3) sFoldr' :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Proxy a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply Foldr'Sym0 t1) t2) t3) sFoldl :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Proxy a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply FoldlSym0 t1) t2) t3) sFoldl' :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Proxy a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply Foldl'Sym0 t1) t2) t3) sFoldr1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (Apply (Apply Foldr1Sym0 t1) t2) sFoldl1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (Apply (Apply Foldl1Sym0 t1) t2) sToList :: forall a (t1 :: Proxy a). Sing t1 -> Sing (Apply ToListSym0 t1) sNull :: forall a (t1 :: Proxy a). Sing t1 -> Sing (Apply NullSym0 t1) sLength :: forall a (t1 :: Proxy a). Sing t1 -> Sing (Apply LengthSym0 t1) sElem :: forall a (t1 :: a) (t2 :: Proxy a). SEq a => Sing t1 -> Sing t2 -> Sing (Apply (Apply ElemSym0 t1) t2) sMaximum :: forall a (t1 :: Proxy a). SOrd a => Sing t1 -> Sing (Apply MaximumSym0 t1) sMinimum :: forall a (t1 :: Proxy a). SOrd a => Sing t1 -> Sing (Apply MinimumSym0 t1) sSum :: forall a (t1 :: Proxy a). SNum a => Sing t1 -> Sing (Apply SumSym0 t1) sProduct :: forall a (t1 :: Proxy a). SNum a => Sing t1 -> Sing (Apply ProductSym0 t1) | |
PTraversable (Proxy :: Type -> Type) | |
Defined in Data.Singletons.Prelude.Traversable type Traverse arg arg1 :: f (t b) type SequenceA arg :: f (t a) type MapM arg arg1 :: m (t b) type Sequence arg :: m (t a) | |
STraversable (Proxy :: Type -> Type) | |
Defined in Data.Singletons.Prelude.Traversable sTraverse :: forall a (f :: Type -> Type) b (t1 :: a ~> f b) (t2 :: Proxy a). SApplicative f => Sing t1 -> Sing t2 -> Sing (Apply (Apply TraverseSym0 t1) t2) sSequenceA :: forall (f :: Type -> Type) a (t1 :: Proxy (f a)). SApplicative f => Sing t1 -> Sing (Apply SequenceASym0 t1) sMapM :: forall a (m :: Type -> Type) b (t1 :: a ~> m b) (t2 :: Proxy a). SMonad m => Sing t1 -> Sing t2 -> Sing (Apply (Apply MapMSym0 t1) t2) sSequence :: forall (m :: Type -> Type) a (t1 :: Proxy (m a)). SMonad m => Sing t1 -> Sing (Apply SequenceSym0 t1) | |
CFoldable (Proxy :: Type -> Type) | |
Defined in Control.Subcategory.Foldable cfoldMap :: (Dom Proxy a, Monoid w) => (a -> w) -> Proxy a -> w cfoldMap' :: (Dom Proxy a, Monoid m) => (a -> m) -> Proxy a -> m cfold :: (Dom Proxy w, Monoid w) => Proxy w -> w cfoldr :: Dom Proxy a => (a -> b -> b) -> b -> Proxy a -> b cfoldlM :: (Monad m, Dom Proxy b) => (a -> b -> m a) -> a -> Proxy b -> m a cfoldlM' :: (Monad m, Dom Proxy b) => (a -> b -> m a) -> a -> Proxy b -> m a cfoldrM :: (Monad m, Dom Proxy a) => (a -> b -> m b) -> b -> Proxy a -> m b cfoldrM' :: (Monad m, Dom Proxy a) => (a -> b -> m b) -> b -> Proxy a -> m b cfoldl :: Dom Proxy a => (b -> a -> b) -> b -> Proxy a -> b cfoldr' :: Dom Proxy a => (a -> b -> b) -> b -> Proxy a -> b cfoldl' :: Dom Proxy a => (b -> a -> b) -> b -> Proxy a -> b cbasicToList :: Dom Proxy a => Proxy a -> [a] cfoldr1 :: Dom Proxy a => (a -> a -> a) -> Proxy a -> a cfoldl1 :: Dom Proxy a => (a -> a -> a) -> Proxy a -> a cindex :: Dom Proxy a => Proxy a -> Int -> a cnull :: Dom Proxy a => Proxy a -> Bool clength :: Dom Proxy a => Proxy a -> Int cany :: Dom Proxy a => (a -> Bool) -> Proxy a -> Bool call :: Dom Proxy a => (a -> Bool) -> Proxy a -> Bool celem :: (Eq a, Dom Proxy a) => a -> Proxy a -> Bool cnotElem :: (Eq a, Dom Proxy a) => a -> Proxy a -> Bool cminimum :: (Ord a, Dom Proxy a) => Proxy a -> a cmaximum :: (Ord a, Dom Proxy a) => Proxy a -> a csum :: (Num a, Dom Proxy a) => Proxy a -> a cproduct :: (Num a, Dom Proxy a) => Proxy a -> a cctraverse_ :: (CApplicative g, CPointed g, Dom g (), Dom Proxy a, Dom g b) => (a -> g b) -> Proxy a -> g () ctraverse_ :: (Applicative g, Dom Proxy a) => (a -> g b) -> Proxy a -> g () clast :: Dom Proxy a => Proxy a -> a chead :: Dom Proxy a => Proxy a -> a cfind :: Dom Proxy a => (a -> Bool) -> Proxy a -> Maybe a cfindIndex :: Dom Proxy a => (a -> Bool) -> Proxy a -> Maybe Int cfindIndices :: Dom Proxy a => (a -> Bool) -> Proxy a -> [Int] celemIndex :: (Dom Proxy a, Eq a) => a -> Proxy a -> Maybe Int celemIndices :: (Dom Proxy a, Eq a) => a -> Proxy a -> [Int] | |
CZip (Proxy :: Type -> Type) | |
CFunctor (Proxy :: Type -> Type) | |
CPointed (Proxy :: Type -> Type) | |
Defined in Control.Subcategory.Pointed | |
CTraversable (Proxy :: Type -> Type) | |
Defined in Control.Subcategory.Foldable | |
CUnzip (Proxy :: Type -> Type) | |
Constrained (Proxy :: Type -> Type) | |
Defined in Control.Subcategory.Functor type Dom Proxy a | |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (Proxy s) | Since: base-4.7.0.0 |
Eq (Proxy s) | Since: base-4.7.0.0 |
Data t => Data (Proxy t) | Since: base-4.7.0.0 |
Defined in Data.Data gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy t -> c (Proxy t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy t) # toConstr :: Proxy t -> Constr # dataTypeOf :: Proxy t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Proxy t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Proxy t)) # gmapT :: (forall b. Data b => b -> b) -> Proxy t -> Proxy t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r # gmapQ :: (forall d. Data d => d -> u) -> Proxy t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t) # | |
Ord (Proxy s) | Since: base-4.7.0.0 |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Ix (Proxy s) | Since: base-4.7.0.0 |
Defined in Data.Proxy | |
Generic (Proxy t) | Since: base-4.6.0.0 |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |
Hashable (Proxy a) | |
Defined in Data.Hashable.Class | |
NFData (Proxy a) | Since: deepseq-1.4.0.0 |
Defined in Control.DeepSeq | |
MonoFoldable (Proxy a) | |
Defined in Data.MonoTraversable ofoldMap :: Monoid m => (Element (Proxy a) -> m) -> Proxy a -> m ofoldr :: (Element (Proxy a) -> b -> b) -> b -> Proxy a -> b ofoldl' :: (a0 -> Element (Proxy a) -> a0) -> a0 -> Proxy a -> a0 otoList :: Proxy a -> [Element (Proxy a)] oall :: (Element (Proxy a) -> Bool) -> Proxy a -> Bool oany :: (Element (Proxy a) -> Bool) -> Proxy a -> Bool ocompareLength :: Integral i => Proxy a -> i -> Ordering otraverse_ :: Applicative f => (Element (Proxy a) -> f b) -> Proxy a -> f () ofor_ :: Applicative f => Proxy a -> (Element (Proxy a) -> f b) -> f () omapM_ :: Applicative m => (Element (Proxy a) -> m ()) -> Proxy a -> m () oforM_ :: Applicative m => Proxy a -> (Element (Proxy a) -> m ()) -> m () ofoldlM :: Monad m => (a0 -> Element (Proxy a) -> m a0) -> a0 -> Proxy a -> m a0 ofoldMap1Ex :: Semigroup m => (Element (Proxy a) -> m) -> Proxy a -> m ofoldr1Ex :: (Element (Proxy a) -> Element (Proxy a) -> Element (Proxy a)) -> Proxy a -> Element (Proxy a) ofoldl1Ex' :: (Element (Proxy a) -> Element (Proxy a) -> Element (Proxy a)) -> Proxy a -> Element (Proxy a) headEx :: Proxy a -> Element (Proxy a) lastEx :: Proxy a -> Element (Proxy a) unsafeHead :: Proxy a -> Element (Proxy a) unsafeLast :: Proxy a -> Element (Proxy a) maximumByEx :: (Element (Proxy a) -> Element (Proxy a) -> Ordering) -> Proxy a -> Element (Proxy a) minimumByEx :: (Element (Proxy a) -> Element (Proxy a) -> Ordering) -> Proxy a -> Element (Proxy a) | |
MonoFunctor (Proxy a) | |
MonoTraversable (Proxy a) | |
Defined in Data.MonoTraversable | |
MonoPointed (Proxy a) | |
Defined in Data.MonoTraversable | |
SuppressUnusedWarnings (Elem_6989586621680823507Sym0 :: TyFun a (Proxy a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Pure_6989586621680787330Sym0 :: TyFun a (Proxy a) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Sum_6989586621680823515Sym0 :: TyFun (Proxy a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Product_6989586621680823521Sym0 :: TyFun (Proxy a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Fold_6989586621680823444Sym0 :: TyFun (Proxy m) m -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldr1_6989586621680823486Sym0 :: TyFun (a ~> (a ~> a)) (Proxy a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldl1_6989586621680823477Sym0 :: TyFun (a ~> (a ~> a)) (Proxy a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
TestCoercion (SProxy :: Proxy t -> Type) | |
Defined in Data.Singletons.Prelude.Proxy testCoercion :: forall (a :: k) (b :: k). SProxy a -> SProxy b -> Maybe (Coercion a b) # | |
TestEquality (SProxy :: Proxy t -> Type) | |
Defined in Data.Singletons.Prelude.Proxy testEquality :: forall (a :: k) (b :: k). SProxy a -> SProxy b -> Maybe (a :~: b) # | |
SuppressUnusedWarnings (Mconcat_6989586621680787315Sym0 :: TyFun [Proxy s] (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621680787264Sym0 :: TyFun Nat (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680787233Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Sequence_6989586621681088388Sym0 :: TyFun (Proxy (m a)) (m (Proxy a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (SequenceA_6989586621681088373Sym0 :: TyFun (Proxy (f a)) (f (Proxy a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldr1_6989586621680823486Sym1 a6989586621680823491 :: TyFun (Proxy a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldl1_6989586621680823477Sym1 a6989586621680823482 :: TyFun (Proxy a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787337Sym0 :: TyFun (Proxy (a ~> b)) (Proxy a ~> Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Elem_6989586621680823507Sym1 a6989586621680823512 :: TyFun (Proxy a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Null_6989586621680823500Sym0 :: TyFun (Proxy a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823494Sym0 :: TyFun (Proxy a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787349Sym0 :: TyFun (Proxy a) (Proxy a ~> Proxy a) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787298Sym0 :: TyFun (Proxy s) (Proxy s ~> Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787214Sym0 :: TyFun (Proxy s) (Proxy s ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Succ_6989586621680787246Sym0 :: TyFun (Proxy s) (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Pred_6989586621680787252Sym0 :: TyFun (Proxy s) (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621680787258Sym0 :: TyFun (Proxy s) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromTo_6989586621680787289Sym0 :: TyFun (Proxy s) (Proxy s ~> [Proxy s]) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromThenTo_6989586621680787278Sym0 :: TyFun (Proxy s) (Proxy s ~> (Proxy s ~> [Proxy s])) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Compare_6989586621680787223Sym0 :: TyFun (Proxy s) (Proxy s ~> Ordering) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Sconcat_6989586621680787306Sym0 :: TyFun (NonEmpty (Proxy s)) (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldr_6989586621680823452Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (Proxy a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldl_6989586621680823465Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (Proxy a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FoldMap_6989586621680823436Sym0 :: TyFun (a ~> m) (Proxy a ~> m) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Fmap_6989586621680787322Sym0 :: TyFun (a ~> b) (Proxy a ~> Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldr_6989586621680823452Sym1 a6989586621680823458 :: TyFun b (Proxy a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldl_6989586621680823465Sym1 a6989586621680823471 :: TyFun b (Proxy a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FoldMap_6989586621680823436Sym1 a6989586621680823441 :: TyFun (Proxy a) m -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787358Sym0 :: TyFun (Proxy a) ((a ~> Proxy b) ~> Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787337Sym1 a6989586621680787342 :: TyFun (Proxy a) (Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Fmap_6989586621680787322Sym1 a6989586621680787327 :: TyFun (Proxy a) (Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787349Sym1 a6989586621680787354 :: TyFun (Proxy a) (Proxy a) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787298Sym1 a6989586621680787303 :: TyFun (Proxy s) (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787214Sym1 a6989586621680787219 :: TyFun (Proxy s) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680787233Sym1 a6989586621680787241 :: TyFun (Proxy s) (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromTo_6989586621680787289Sym1 a6989586621680787294 :: TyFun (Proxy s) [Proxy s] -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromThenTo_6989586621680787278Sym1 a6989586621680787284 :: TyFun (Proxy s) (Proxy s ~> [Proxy s]) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Compare_6989586621680787223Sym1 a6989586621680787228 :: TyFun (Proxy s) Ordering -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Traverse_6989586621681088365Sym0 :: TyFun (a ~> f b) (Proxy a ~> f (Proxy b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (MapM_6989586621681088380Sym0 :: TyFun (a ~> m b) (Proxy a ~> m (Proxy b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Traverse_6989586621681088365Sym1 a6989586621681088370 :: TyFun (Proxy a) (f (Proxy b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (MapM_6989586621681088380Sym1 a6989586621681088385 :: TyFun (Proxy a) (m (Proxy b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldr_6989586621680823452Sym2 a6989586621680823458 a6989586621680823459 :: TyFun (Proxy a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Foldl_6989586621680823465Sym2 a6989586621680823471 a6989586621680823472 :: TyFun (Proxy a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromThenTo_6989586621680787278Sym2 a6989586621680787284 a6989586621680787285 :: TyFun (Proxy s) [Proxy s] -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (TFHelper_6989586621680787358Sym1 a6989586621680787363 :: TyFun (a ~> Proxy b) (Proxy b) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
type MapM (a2 :: a1 ~> m b) (a3 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Traverse (a2 :: a1 ~> f b) (a3 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Traversable | |
type LiftA2 (arg1 :: a ~> (b ~> c)) (arg2 :: Proxy a) (arg3 :: Proxy b) | |
type FoldMap (a2 :: a1 ~> k2) (a3 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Fmap (a2 :: a1 ~> b) (a3 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Foldl (a2 :: k2 ~> (a1 ~> k2)) (a3 :: k2) (a4 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Foldr (a2 :: a1 ~> (k2 ~> k2)) (a3 :: k2) (a4 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Foldl' (arg1 :: b ~> (a ~> b)) (arg2 :: b) (arg3 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Foldr' (arg1 :: a ~> (b ~> b)) (arg2 :: b) (arg3 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Rep1 (Proxy :: k -> Type) | |
type Pure (a :: k1) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Return (arg :: a) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Mzero | |
Defined in Data.Singletons.Prelude.Proxy type Mzero = Mzero_6989586621680012075Sym0 :: Proxy a | |
type Empty | |
Defined in Data.Singletons.Prelude.Proxy type Empty = Empty_6989586621680787344Sym0 :: Proxy a | |
type Elem (a1 :: k1) (a2 :: Proxy k1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Foldl1 (a1 :: k2 ~> (k2 ~> k2)) (a2 :: Proxy k2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Foldr1 (a1 :: k2 ~> (k2 ~> k2)) (a2 :: Proxy k2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type (arg1 :: a) <$ (arg2 :: Proxy b) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Mplus (arg1 :: Proxy a) (arg2 :: Proxy a) | |
type (a2 :: Proxy a1) <|> (a3 :: Proxy a1) | |
type Apply (Elem_6989586621680823507Sym0 :: TyFun a (Proxy a ~> Bool) -> Type) (a6989586621680823512 :: a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Pure_6989586621680787330Sym0 :: TyFun a (Proxy a) -> Type) (a6989586621680787334 :: a) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (ToEnum_6989586621680787264Sym0 :: TyFun Nat (Proxy s) -> Type) (a6989586621680787268 :: Nat) | |
type Apply (ShowsPrec_6989586621680787233Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) (a6989586621680787241 :: Nat) | |
type Apply (Foldr_6989586621680823452Sym1 a6989586621680823458 :: TyFun b (Proxy a ~> b) -> Type) (a6989586621680823459 :: b) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldl_6989586621680823465Sym1 a6989586621680823471 :: TyFun b (Proxy a ~> b) -> Type) (a6989586621680823472 :: b) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Rep (Proxy :: Type -> Type) | |
Defined in Data.Functor.Rep | |
type Key (Proxy :: Type -> Type) | |
type Dom (Proxy :: Type -> Type) a | |
Defined in Control.Subcategory.Functor | |
type Maximum (arg :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Minimum (arg :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Null (a2 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Product (a :: Proxy k2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Sum (a :: Proxy k2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Fold (a :: Proxy k2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Length (a2 :: Proxy a1) | |
Defined in Data.Singletons.Prelude.Foldable | |
type ToList (arg :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Sequence (a2 :: Proxy (m a1)) | |
Defined in Data.Singletons.Prelude.Traversable | |
type SequenceA (a2 :: Proxy (f a1)) | |
Defined in Data.Singletons.Prelude.Traversable | |
type (arg1 :: Proxy a) *> (arg2 :: Proxy b) | |
type (arg1 :: Proxy a) <* (arg2 :: Proxy b) | |
type (a2 :: Proxy (a1 ~> b)) <*> (a3 :: Proxy a1) | |
type (arg1 :: Proxy a) >> (arg2 :: Proxy b) | |
type (a2 :: Proxy a1) >>= (a3 :: a1 ~> Proxy b) | |
type Apply (Mconcat_6989586621680787315Sym0 :: TyFun [Proxy s] (Proxy s) -> Type) (a6989586621680787319 :: [Proxy s]) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Sconcat_6989586621680787306Sym0 :: TyFun (NonEmpty (Proxy s)) (Proxy s) -> Type) (a6989586621680787310 :: NonEmpty (Proxy s)) | |
type Rep (Proxy t) | |
type Demote (Proxy t) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Sing | |
Defined in Data.Singletons.Prelude.Proxy | |
type MaxBound | |
Defined in Data.Singletons.Prelude.Proxy type MaxBound = MaxBound_6989586621680787209Sym0 :: Proxy s | |
type MinBound | |
Defined in Data.Singletons.Prelude.Proxy type MinBound = MinBound_6989586621680787206Sym0 :: Proxy s | |
type Mempty | |
Defined in Data.Singletons.Prelude.Proxy type Mempty = Mempty_6989586621680787311Sym0 :: Proxy s | |
type Element (Proxy a) | |
Defined in Data.MonoTraversable type Element (Proxy a) = a | |
type FromEnum (a :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type ToEnum a | |
Defined in Data.Singletons.Prelude.Proxy | |
type Mconcat (a :: [Proxy s]) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Show_ (arg :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Pred (a :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Succ (a :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Sconcat (a :: NonEmpty (Proxy s)) | |
type EnumFromTo (a1 :: Proxy s) (a2 :: Proxy s) | |
type (x :: Proxy s) /= (y :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type (a1 :: Proxy s) == (a2 :: Proxy s) | |
type Mappend (arg1 :: Proxy s) (arg2 :: Proxy s) | |
type (arg1 :: Proxy s) < (arg2 :: Proxy s) | |
type (arg1 :: Proxy s) <= (arg2 :: Proxy s) | |
type (arg1 :: Proxy s) > (arg2 :: Proxy s) | |
type (arg1 :: Proxy s) >= (arg2 :: Proxy s) | |
type Compare (a1 :: Proxy s) (a2 :: Proxy s) | |
type Max (arg1 :: Proxy s) (arg2 :: Proxy s) | |
type Min (arg1 :: Proxy s) (arg2 :: Proxy s) | |
type (a1 :: Proxy s) <> (a2 :: Proxy s) | |
type ShowList (arg1 :: [Proxy s]) arg2 | |
type EnumFromThenTo (a1 :: Proxy s) (a2 :: Proxy s) (a3 :: Proxy s) | |
type ShowsPrec a1 (a2 :: Proxy s) a3 | |
type Apply (Fold_6989586621680823444Sym0 :: TyFun (Proxy m) m -> Type) (a6989586621680823448 :: Proxy m) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Sum_6989586621680823515Sym0 :: TyFun (Proxy a) a -> Type) (a6989586621680823519 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Product_6989586621680823521Sym0 :: TyFun (Proxy a) a -> Type) (a6989586621680823525 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldl1_6989586621680823477Sym1 a6989586621680823482 :: TyFun (Proxy a) a -> Type) (a6989586621680823483 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldr1_6989586621680823486Sym1 a6989586621680823491 :: TyFun (Proxy a) a -> Type) (a6989586621680823492 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Elem_6989586621680823507Sym1 a6989586621680823512 :: TyFun (Proxy a) Bool -> Type) (a6989586621680823513 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Length_6989586621680823494Sym0 :: TyFun (Proxy a) Nat -> Type) (a6989586621680823498 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Null_6989586621680823500Sym0 :: TyFun (Proxy a) Bool -> Type) (a6989586621680823504 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (FromEnum_6989586621680787258Sym0 :: TyFun (Proxy s) Nat -> Type) (a6989586621680787262 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (FoldMap_6989586621680823436Sym1 a6989586621680823441 :: TyFun (Proxy a) m -> Type) (a6989586621680823442 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (TFHelper_6989586621680787214Sym1 a6989586621680787219 :: TyFun (Proxy s) Bool -> Type) (a6989586621680787220 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Compare_6989586621680787223Sym1 a6989586621680787228 :: TyFun (Proxy s) Ordering -> Type) (a6989586621680787229 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Foldr_6989586621680823452Sym2 a6989586621680823458 a6989586621680823459 :: TyFun (Proxy a) b -> Type) (a6989586621680823460 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldl_6989586621680823465Sym2 a6989586621680823471 a6989586621680823472 :: TyFun (Proxy a) b -> Type) (a6989586621680823473 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (SequenceA_6989586621681088373Sym0 :: TyFun (Proxy (f a)) (f (Proxy a)) -> Type) (a6989586621681088377 :: Proxy (f a)) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (Sequence_6989586621681088388Sym0 :: TyFun (Proxy (m a)) (m (Proxy a)) -> Type) (a6989586621681088392 :: Proxy (m a)) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (EnumFromTo_6989586621680787289Sym1 a6989586621680787294 :: TyFun (Proxy s) [Proxy s] -> Type) (a6989586621680787295 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Traverse_6989586621681088365Sym1 a6989586621681088370 :: TyFun (Proxy a) (f (Proxy b)) -> Type) (a6989586621681088371 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (MapM_6989586621681088380Sym1 a6989586621681088385 :: TyFun (Proxy a) (m (Proxy b)) -> Type) (a6989586621681088386 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (EnumFromThenTo_6989586621680787278Sym2 a6989586621680787284 a6989586621680787285 :: TyFun (Proxy s) [Proxy s] -> Type) (a6989586621680787286 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Foldl1_6989586621680823477Sym0 :: TyFun (a ~> (a ~> a)) (Proxy a ~> a) -> Type) (a6989586621680823482 :: a ~> (a ~> a)) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldr1_6989586621680823486Sym0 :: TyFun (a ~> (a ~> a)) (Proxy a ~> a) -> Type) (a6989586621680823491 :: a ~> (a ~> a)) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (TFHelper_6989586621680787337Sym0 :: TyFun (Proxy (a ~> b)) (Proxy a ~> Proxy b) -> Type) (a6989586621680787342 :: Proxy (a ~> b)) | |
type Apply (TFHelper_6989586621680787214Sym0 :: TyFun (Proxy s) (Proxy s ~> Bool) -> Type) (a6989586621680787219 :: Proxy s) | |
type Apply (Compare_6989586621680787223Sym0 :: TyFun (Proxy s) (Proxy s ~> Ordering) -> Type) (a6989586621680787228 :: Proxy s) | |
type Apply (Succ_6989586621680787246Sym0 :: TyFun (Proxy s) (Proxy s) -> Type) (a6989586621680787250 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Pred_6989586621680787252Sym0 :: TyFun (Proxy s) (Proxy s) -> Type) (a6989586621680787256 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (EnumFromThenTo_6989586621680787278Sym0 :: TyFun (Proxy s) (Proxy s ~> (Proxy s ~> [Proxy s])) -> Type) (a6989586621680787284 :: Proxy s) | |
type Apply (EnumFromTo_6989586621680787289Sym0 :: TyFun (Proxy s) (Proxy s ~> [Proxy s]) -> Type) (a6989586621680787294 :: Proxy s) | |
type Apply (TFHelper_6989586621680787298Sym0 :: TyFun (Proxy s) (Proxy s ~> Proxy s) -> Type) (a6989586621680787303 :: Proxy s) | |
type Apply (TFHelper_6989586621680787349Sym0 :: TyFun (Proxy a) (Proxy a ~> Proxy a) -> Type) (a6989586621680787354 :: Proxy a) | |
type Apply (FoldMap_6989586621680823436Sym0 :: TyFun (a ~> m) (Proxy a ~> m) -> Type) (a6989586621680823441 :: a ~> m) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldr_6989586621680823452Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (Proxy a ~> b)) -> Type) (a6989586621680823458 :: a ~> (b ~> b)) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Foldl_6989586621680823465Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (Proxy a ~> b)) -> Type) (a6989586621680823471 :: b ~> (a ~> b)) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Fmap_6989586621680787322Sym0 :: TyFun (a ~> b) (Proxy a ~> Proxy b) -> Type) (a6989586621680787327 :: a ~> b) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Fmap_6989586621680787322Sym1 a6989586621680787327 :: TyFun (Proxy a) (Proxy b) -> Type) (a6989586621680787328 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (TFHelper_6989586621680787337Sym1 a6989586621680787342 :: TyFun (Proxy a) (Proxy b) -> Type) (a6989586621680787343 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (TFHelper_6989586621680787358Sym0 :: TyFun (Proxy a) ((a ~> Proxy b) ~> Proxy b) -> Type) (a6989586621680787363 :: Proxy a) | |
type Apply (ShowsPrec_6989586621680787233Sym1 a6989586621680787241 :: TyFun (Proxy s) (Symbol ~> Symbol) -> Type) (a6989586621680787242 :: Proxy s) | |
type Apply (EnumFromThenTo_6989586621680787278Sym1 a6989586621680787284 :: TyFun (Proxy s) (Proxy s ~> [Proxy s]) -> Type) (a6989586621680787285 :: Proxy s) | |
type Apply (TFHelper_6989586621680787298Sym1 a6989586621680787303 :: TyFun (Proxy s) (Proxy s) -> Type) (a6989586621680787304 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (TFHelper_6989586621680787349Sym1 a6989586621680787354 :: TyFun (Proxy a) (Proxy a) -> Type) (a6989586621680787355 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (Traverse_6989586621681088365Sym0 :: TyFun (a ~> f b) (Proxy a ~> f (Proxy b)) -> Type) (a6989586621681088370 :: a ~> f b) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (MapM_6989586621681088380Sym0 :: TyFun (a ~> m b) (Proxy a ~> m (Proxy b)) -> Type) (a6989586621681088385 :: a ~> m b) | |
Defined in Data.Singletons.Prelude.Traversable | |
type Apply (TFHelper_6989586621680787358Sym1 a6989586621680787363 :: TyFun (a ~> Proxy b) (Proxy b) -> Type) (a6989586621680787364 :: a ~> Proxy b) | |
Defined in Data.Singletons.Prelude.Proxy |
A concrete, promotable proxy type, for use at the kind level. There are no instances for this because it is intended at the kind level only
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
natSing
(Kind) This is the kind of type-level natural numbers.
Instances
PEnum Nat | |
Defined in Data.Singletons.Prelude.Enum type Succ arg :: a type Pred arg :: a type ToEnum arg :: a type FromEnum arg :: Nat type EnumFromTo arg arg1 :: [a] type EnumFromThenTo arg arg1 arg2 :: [a] | |
SEnum Nat | |
Defined in Data.Singletons.Prelude.Enum sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) sEnumFromTo :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) sEnumFromThenTo :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) | |
PNum Nat | |
Defined in Data.Singletons.Prelude.Num type arg + arg1 :: a type arg - arg1 :: a type arg * arg1 :: a type Negate arg :: a type Abs arg :: a type Signum arg :: a type FromInteger arg :: a | |
SNum Nat | |
Defined in Data.Singletons.Prelude.Num (%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) (%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) (%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) | |
PShow Nat | |
Defined in Data.Singletons.Prelude.Show | |
SShow Nat | |
Defined in Data.Singletons.Prelude.Show sShowsPrec :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) sShowList :: forall (t1 :: [Nat]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) | |
KnownNat n => HasResolution (n :: Nat) | For example, |
Defined in Data.Fixed resolution :: p n -> Integer # | |
TestEquality SNat | |
Defined in Data.Type.Natural.Core | |
KnownNat n => Reifies (n :: Nat) Integer | |
Defined in Data.Reflection | |
(IsMonomialOrder k ord, ones ~ Replicate n 1, SingI ones, Length ones <= k, KnownNat k) => EliminationType k (n :: Nat) (WeightOrder ones ord) Source # | |
Defined in Algebra.Ring.Polynomial.Monomial | |
(KnownNat n, KnownNat m, IsMonomialOrder n ord, IsMonomialOrder m ord', k ~ (n + m), KnownNat k) => EliminationType k (n :: Nat) (ProductOrder n m ord ord') Source # | |
Defined in Algebra.Ring.Polynomial.Monomial | |
SingI Log2Sym0 | |
Defined in Data.Singletons.TypeLits | |
SingI (<=?@#@$) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI (^@#@$) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI DivSym0 | |
Defined in Data.Singletons.TypeLits | |
SingI ModSym0 | |
Defined in Data.Singletons.TypeLits | |
SingI EftNatSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatDnSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatUpSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SuppressUnusedWarnings FromEnum_6989586621680204253Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings FromEnum_6989586621680204277Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ToEnum_6989586621680204240Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ToEnum_6989586621680204261Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings KnownNatSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings Log2Sym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings FromEnum_6989586621680181073Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings Pred_6989586621680181059Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings Succ_6989586621680181052Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ToEnum_6989586621680181066Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ToEnum_6989586621680204284Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621680654062Sym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621680654084Sym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (<=?@#@$) | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EftNatSym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EnumFromTo_6989586621680181081Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (^@#@$) | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings DivSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ModSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings QuotSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings RemSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings DivModSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings QuotRemSym0 | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EfdtNatDnSym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EfdtNatSym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EfdtNatUpSym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings EnumFromThenTo_6989586621680181097Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsNatSym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621680636824Sym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621680653912Sym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621680654112Sym0 | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621681187235Sym0 | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ShowsPrec_6989586621681187261Sym0 | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings FromEnum_6989586621680204294Sym0 | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits | |
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits | |
SingI (ListlengthSym0 :: TyFun [a] Nat -> Type) | |
SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) | |
SingI (LengthSym0 :: TyFun [a] Nat -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SuppressUnusedWarnings (ListlengthSym0 :: TyFun [a] Nat -> Type) | |
SuppressUnusedWarnings (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) | |
SuppressUnusedWarnings (LengthSym0 :: TyFun [a] Nat -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823238Sym0 :: TyFun [a] Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ((<=?@#@$$) a6989586621679910752 :: TyFun Nat Bool -> Type) | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EftNatSym1 a6989586621680180958 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromTo_6989586621680181081Sym1 a6989586621680181090 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings ((^@#@$$) a6989586621679910455 :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (DivSym1 a6989586621679947651 :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ModSym1 a6989586621679947992 :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (QuotSym1 a6989586621679948468 :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (RemSym1 a6989586621679948457 :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (DivModSym1 a6989586621679948486 :: TyFun Nat (Nat, Nat) -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (QuotRemSym1 a6989586621679948479 :: TyFun Nat (Nat, Nat) -> Type) | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621679976084Sym0 :: TyFun Nat (Down a) -> Type) | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681203117Sym0 :: TyFun Nat (Min a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621681203279Sym0 :: TyFun Nat (Min a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681203394Sym0 :: TyFun Nat (Max a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621681203556Sym0 :: TyFun Nat (Max a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681203842Sym0 :: TyFun Nat (First a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681204050Sym0 :: TyFun Nat (Last a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681204219Sym0 :: TyFun Nat (WrappedMonoid a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621681012388Sym0 :: TyFun Nat (Identity a) -> Type) | |
Defined in Data.Singletons.Prelude.Identity suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621681012485Sym0 :: TyFun Nat (Identity a) -> Type) | |
Defined in Data.Singletons.Prelude.Identity suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621680269281Sym0 :: TyFun Nat (Sum a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621680269410Sym0 :: TyFun Nat (Product a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SuppressUnusedWarnings (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
SuppressUnusedWarnings (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636806Sym0 :: TyFun Nat ([a] ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680653944Sym0 :: TyFun Nat (Maybe a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatDnSym1 a6989586621680180866 :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatSym1 a6989586621680180940 :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatUpSym1 a6989586621680180903 :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromThenTo_6989586621680181097Sym1 a6989586621680181109 :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636774Sym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187348Sym0 :: TyFun Nat (Min a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187377Sym0 :: TyFun Nat (Max a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187406Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187435Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187464Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187180Sym0 :: TyFun Nat (Option a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681012505Sym0 :: TyFun Nat (Identity a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Identity suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680698028Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680698057Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187209Sym0 :: TyFun Nat (Dual a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187290Sym0 :: TyFun Nat (Sum a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681187319Sym0 :: TyFun Nat (Product a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680654038Sym0 :: TyFun Nat (NonEmpty a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Nat -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681203126Sym0 :: TyFun (Min a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681203403Sym0 :: TyFun (Max a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681203851Sym0 :: TyFun (First a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681204059Sym0 :: TyFun (Last a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681204228Sym0 :: TyFun (WrappedMonoid a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621681012654Sym0 :: TyFun (Identity a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Identity suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681012395Sym0 :: TyFun (Identity a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Identity suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823647Sym0 :: TyFun (Dual a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823822Sym0 :: TyFun (Sum a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823997Sym0 :: TyFun (Product a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type) | |
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SuppressUnusedWarnings (FindIndicesSym1 a6989586621680379629 :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FindIndexSym1 a6989586621680379652 :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621680379661 :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ElemIndexSym1 a6989586621680379670 :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823420Sym0 :: TyFun (Either a1 a2) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatDnSym2 a6989586621680180866 a6989586621680180867 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatSym2 a6989586621680180940 a6989586621680180941 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EfdtNatUpSym2 a6989586621680180903 a6989586621680180904 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (EnumFromThenTo_6989586621680181097Sym2 a6989586621680181109 a6989586621680181110 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ListindexSym1 a6989586621680765275 :: TyFun Nat a -> Type) | |
SuppressUnusedWarnings ((!!@#@$$) a6989586621680379294 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ToEnum_6989586621680787264Sym0 :: TyFun Nat (Proxy s) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680653998Sym0 :: TyFun Nat (Either a b ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636842Sym0 :: TyFun Nat ((a, b) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681203710Sym0 :: TyFun Nat (Arg a b ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680787233Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823494Sym0 :: TyFun (Proxy a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621680787258Sym0 :: TyFun (Proxy s) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Proxy suppressUnusedWarnings :: () | |
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SuppressUnusedWarnings (ToEnum_6989586621681044546Sym0 :: TyFun Nat (Const a b) -> Type) | |
Defined in Data.Singletons.Prelude.Const suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromInteger_6989586621681044643Sym0 :: TyFun Nat (Const a b) -> Type) | |
Defined in Data.Singletons.Prelude.Const suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636857Sym0 :: TyFun Nat ((a, b, c) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621681044663Sym0 :: TyFun Nat (Const a b ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Const suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621680379633BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Length_6989586621680823002Sym0 :: TyFun (t a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (LengthSym0 :: TyFun (t a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501314LoopSym0 :: TyFun k (TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501296LoopSym0 :: TyFun k (TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (FromEnum_6989586621681044553Sym0 :: TyFun (Const a b) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Const suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636873Sym0 :: TyFun Nat ((a, b, c, d) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621680379633BuildListSym1 p6989586621680379631 :: TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501314LoopSym1 cnt06989586621681501312 :: TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501296LoopSym1 cnt06989586621681501294 :: TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501314LoopSym2 cnt06989586621681501312 f6989586621681501313 :: TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621681501296LoopSym2 cnt06989586621681501294 f6989586621681501295 :: TyFun Nat (m6989586621681500906 ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621680379633BuildListSym2 p6989586621680379631 xs6989586621680379632 :: TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636890Sym0 :: TyFun Nat ((a, b, c, d, e) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (Let6989586621680379633BuildListSym3 p6989586621680379631 xs6989586621680379632 a6989586621680379634 :: TyFun [b6989586621680375544] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636908Sym0 :: TyFun Nat ((a, b, c, d, e, f) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
SuppressUnusedWarnings (ShowsPrec_6989586621680636927Sym0 :: TyFun Nat ((a, b, c, d, e, f, g) ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show suppressUnusedWarnings :: () | |
type Demote Nat | |
Defined in Data.Singletons.TypeLits.Internal | |
type Sing | |
Defined in Data.Singletons.TypeLits.Internal type Sing = SNat | |
type FromEnum (a :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type FromEnum (a :: Nat) = Apply FromEnum_6989586621680181073Sym0 a | |
type ToEnum a | |
Defined in Data.Singletons.Prelude.Enum type ToEnum a = Apply ToEnum_6989586621680181066Sym0 a | |
type Abs (a :: Nat) | |
Defined in Data.Singletons.Prelude.Num type Abs (a :: Nat) = a | |
type FromInteger a | |
Defined in Data.Singletons.Prelude.Num type FromInteger a = a | |
type Negate (a :: Nat) | |
Defined in Data.Singletons.Prelude.Num | |
type Signum (a :: Nat) | |
Defined in Data.Singletons.Prelude.Num type Signum (a :: Nat) = SignumNat a | |
type Show_ (arg :: Nat) | |
Defined in Data.Singletons.Prelude.Show | |
type Pred (a :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Pred (a :: Nat) = Apply Pred_6989586621680181059Sym0 a | |
type Succ (a :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Succ (a :: Nat) = Apply Succ_6989586621680181052Sym0 a | |
type EnumFromTo (a1 :: Nat) (a2 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type (x :: Nat) /= (y :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal | |
type (x :: Nat) == (y :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal | |
type (a :: Nat) * (b :: Nat) | |
Defined in Data.Singletons.Prelude.Num | |
type (a :: Nat) + (b :: Nat) | |
Defined in Data.Singletons.Prelude.Num | |
type (a :: Nat) - (b :: Nat) | |
Defined in Data.Singletons.Prelude.Num | |
type (arg1 :: Nat) < (arg2 :: Nat) | |
type (arg1 :: Nat) <= (arg2 :: Nat) | |
type (arg1 :: Nat) > (arg2 :: Nat) | |
type (arg1 :: Nat) >= (arg2 :: Nat) | |
type Compare (a :: Nat) (b :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal | |
type Max (arg1 :: Nat) (arg2 :: Nat) | |
type Min (arg1 :: Nat) (arg2 :: Nat) | |
type ShowList (arg1 :: [Nat]) arg2 | |
type Apply FromEnum_6989586621680204253Sym0 (a6989586621680204257 :: Bool) | |
Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680204253Sym0 (a6989586621680204257 :: Bool) = FromEnum_6989586621680204253Sym1 a6989586621680204257 | |
type Apply FromEnum_6989586621680204277Sym0 (a6989586621680204281 :: Ordering) | |
Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680204277Sym0 (a6989586621680204281 :: Ordering) = FromEnum_6989586621680204277Sym1 a6989586621680204281 | |
type Apply ToEnum_6989586621680204240Sym0 (a6989586621680204244 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680204240Sym0 (a6989586621680204244 :: Nat) = ToEnum_6989586621680204240Sym1 a6989586621680204244 | |
type Apply ToEnum_6989586621680204261Sym0 (a6989586621680204265 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680204261Sym0 (a6989586621680204265 :: Nat) = ToEnum_6989586621680204261Sym1 a6989586621680204265 | |
type Apply KnownNatSym0 (a6989586621679946868 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (a6989586621679946868 :: Nat) = KnownNatSym1 a6989586621679946868 | |
type Apply Log2Sym0 (a6989586621679947438 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (a6989586621679947438 :: Nat) = Log2Sym1 a6989586621679947438 | |
type Apply FromEnum_6989586621680181073Sym0 (a6989586621680181077 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680181073Sym0 (a6989586621680181077 :: Nat) = FromEnum_6989586621680181073Sym1 a6989586621680181077 | |
type Apply Pred_6989586621680181059Sym0 (a6989586621680181063 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply Pred_6989586621680181059Sym0 (a6989586621680181063 :: Nat) = Pred_6989586621680181059Sym1 a6989586621680181063 | |
type Apply Succ_6989586621680181052Sym0 (a6989586621680181056 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply Succ_6989586621680181052Sym0 (a6989586621680181056 :: Nat) = Succ_6989586621680181052Sym1 a6989586621680181056 | |
type Apply ToEnum_6989586621680181066Sym0 (a6989586621680181070 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680181066Sym0 (a6989586621680181070 :: Nat) = ToEnum_6989586621680181066Sym1 a6989586621680181070 | |
type Apply ToEnum_6989586621680204284Sym0 (a6989586621680204288 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680204284Sym0 (a6989586621680204288 :: Nat) = ToEnum_6989586621680204284Sym1 a6989586621680204288 | |
type Apply FromEnum_6989586621680204294Sym0 (a6989586621680204298 :: ()) | |
Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680204294Sym0 (a6989586621680204298 :: ()) = FromEnum_6989586621680204294Sym1 a6989586621680204298 | |
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type ShowsPrec _1 (n :: Nat) x | |
Defined in Data.Singletons.Prelude.Show type ShowsPrec _1 (n :: Nat) x = ShowsNat n x | |
type Apply ((<=?@#@$$) a6989586621679910752 :: TyFun Nat Bool -> Type) (a6989586621679910753 :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal | |
type Apply ((^@#@$$) a6989586621679910455 :: TyFun Nat Nat -> Type) (a6989586621679910456 :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal | |
type Apply (DivSym1 a6989586621679947651 :: TyFun Nat Nat -> Type) (a6989586621679947652 :: Nat) | |
Defined in Data.Singletons.TypeLits | |
type Apply (ModSym1 a6989586621679947992 :: TyFun Nat Nat -> Type) (a6989586621679947993 :: Nat) | |
Defined in Data.Singletons.TypeLits | |
type Apply (QuotSym1 a6989586621679948468 :: TyFun Nat Nat -> Type) (a6989586621679948469 :: Nat) | |
Defined in Data.Singletons.TypeLits | |
type Apply (RemSym1 a6989586621679948457 :: TyFun Nat Nat -> Type) (a6989586621679948458 :: Nat) | |
Defined in Data.Singletons.TypeLits | |
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621680180987 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679976010 :: Nat) | |
Defined in Data.Singletons.Prelude.Num | |
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621680180990 :: a) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (ListindexSym1 a6989586621680765275 :: TyFun Nat a -> Type) (a6989586621680765276 :: Nat) | |
type Apply ((!!@#@$$) a6989586621680379294 :: TyFun Nat a -> Type) (a6989586621680379295 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (EftNatSym1 a6989586621680180958 :: TyFun Nat [Nat] -> Type) (a6989586621680180959 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (EnumFromTo_6989586621680181081Sym1 a6989586621680181090 :: TyFun Nat [Nat] -> Type) (a6989586621680181091 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (FromInteger_6989586621679976084Sym0 :: TyFun Nat (Down a) -> Type) (a6989586621679976088 :: Nat) | |
type Apply (ToEnum_6989586621681203117Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681203123 :: Nat) | |
type Apply (FromInteger_6989586621681203279Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681203285 :: Nat) | |
type Apply (ToEnum_6989586621681203394Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681203400 :: Nat) | |
type Apply (FromInteger_6989586621681203556Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681203562 :: Nat) | |
type Apply (ToEnum_6989586621681203842Sym0 :: TyFun Nat (First a) -> Type) (a6989586621681203848 :: Nat) | |
type Apply (ToEnum_6989586621681204050Sym0 :: TyFun Nat (Last a) -> Type) (a6989586621681204056 :: Nat) | |
type Apply (ToEnum_6989586621681204219Sym0 :: TyFun Nat (WrappedMonoid a) -> Type) (a6989586621681204225 :: Nat) | |
Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681204219Sym0 :: TyFun Nat (WrappedMonoid a) -> Type) (a6989586621681204225 :: Nat) = ToEnum_6989586621681204219Sym1 a6989586621681204225 :: WrappedMonoid a | |
type Apply (ToEnum_6989586621681012388Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681012392 :: Nat) | |
type Apply (FromInteger_6989586621681012485Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681012489 :: Nat) | |
type Apply (FromInteger_6989586621680269281Sym0 :: TyFun Nat (Sum a) -> Type) (a6989586621680269285 :: Nat) | |
type Apply (FromInteger_6989586621680269410Sym0 :: TyFun Nat (Product a) -> Type) (a6989586621680269414 :: Nat) | |
type Apply (EfdtNatDnSym2 a6989586621680180866 a6989586621680180867 :: TyFun Nat [Nat] -> Type) (a6989586621680180868 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (EfdtNatSym2 a6989586621680180940 a6989586621680180941 :: TyFun Nat [Nat] -> Type) (a6989586621680180942 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (EfdtNatUpSym2 a6989586621680180903 a6989586621680180904 :: TyFun Nat [Nat] -> Type) (a6989586621680180905 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (EnumFromThenTo_6989586621680181097Sym2 a6989586621680181109 a6989586621680181110 :: TyFun Nat [Nat] -> Type) (a6989586621680181111 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (Let6989586621681501296LoopSym2 cnt06989586621681501294 f6989586621681501295 :: TyFun Nat (m6989586621681500906 ()) -> Type) (a6989586621681501297 :: Nat) | |
Defined in Data.Singletons.Prelude.Monad | |
type Apply (Let6989586621681501314LoopSym2 cnt06989586621681501312 f6989586621681501313 :: TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) (a6989586621681501315 :: Nat) | |
Defined in Data.Singletons.Prelude.Monad | |
type Apply ShowsPrec_6989586621680654062Sym0 (a6989586621680654072 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680654062Sym0 (a6989586621680654072 :: Nat) = ShowsPrec_6989586621680654062Sym1 a6989586621680654072 | |
type Apply ShowsPrec_6989586621680654084Sym0 (a6989586621680654096 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680654084Sym0 (a6989586621680654096 :: Nat) = ShowsPrec_6989586621680654084Sym1 a6989586621680654096 | |
type Apply (<=?@#@$) (a6989586621679910752 :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal type Apply (<=?@#@$) (a6989586621679910752 :: Nat) = (<=?@#@$$) a6989586621679910752 | |
type Apply EftNatSym0 (a6989586621680180958 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EftNatSym0 (a6989586621680180958 :: Nat) = EftNatSym1 a6989586621680180958 | |
type Apply EnumFromTo_6989586621680181081Sym0 (a6989586621680181090 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EnumFromTo_6989586621680181081Sym0 (a6989586621680181090 :: Nat) = EnumFromTo_6989586621680181081Sym1 a6989586621680181090 | |
type Apply (^@#@$) (a6989586621679910455 :: Nat) | |
Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (a6989586621679910455 :: Nat) = (^@#@$$) a6989586621679910455 | |
type Apply DivSym0 (a6989586621679947651 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply DivSym0 (a6989586621679947651 :: Nat) = DivSym1 a6989586621679947651 | |
type Apply ModSym0 (a6989586621679947992 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply ModSym0 (a6989586621679947992 :: Nat) = ModSym1 a6989586621679947992 | |
type Apply QuotSym0 (a6989586621679948468 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply QuotSym0 (a6989586621679948468 :: Nat) = QuotSym1 a6989586621679948468 | |
type Apply RemSym0 (a6989586621679948457 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply RemSym0 (a6989586621679948457 :: Nat) = RemSym1 a6989586621679948457 | |
type Apply DivModSym0 (a6989586621679948486 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply DivModSym0 (a6989586621679948486 :: Nat) = DivModSym1 a6989586621679948486 | |
type Apply QuotRemSym0 (a6989586621679948479 :: Nat) | |
Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (a6989586621679948479 :: Nat) = QuotRemSym1 a6989586621679948479 | |
type Apply EfdtNatDnSym0 (a6989586621680180866 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatDnSym0 (a6989586621680180866 :: Nat) = EfdtNatDnSym1 a6989586621680180866 | |
type Apply EfdtNatSym0 (a6989586621680180940 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatSym0 (a6989586621680180940 :: Nat) = EfdtNatSym1 a6989586621680180940 | |
type Apply EfdtNatUpSym0 (a6989586621680180903 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatUpSym0 (a6989586621680180903 :: Nat) = EfdtNatUpSym1 a6989586621680180903 | |
type Apply EnumFromThenTo_6989586621680181097Sym0 (a6989586621680181109 :: Nat) | |
Defined in Data.Singletons.Prelude.Enum type Apply EnumFromThenTo_6989586621680181097Sym0 (a6989586621680181109 :: Nat) = EnumFromThenTo_6989586621680181097Sym1 a6989586621680181109 | |
type Apply ShowsNatSym0 (a6989586621680653440 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsNatSym0 (a6989586621680653440 :: Nat) = ShowsNatSym1 a6989586621680653440 | |
type Apply ShowsPrec_6989586621680636824Sym0 (a6989586621680636834 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680636824Sym0 (a6989586621680636834 :: Nat) = ShowsPrec_6989586621680636824Sym1 a6989586621680636834 | |
type Apply ShowsPrec_6989586621680653912Sym0 (a6989586621680653920 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680653912Sym0 (a6989586621680653920 :: Nat) = ShowsPrec_6989586621680653912Sym1 a6989586621680653920 | |
type Apply ShowsPrec_6989586621680654112Sym0 (a6989586621680654120 :: Nat) | |
Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680654112Sym0 (a6989586621680654120 :: Nat) = ShowsPrec_6989586621680654112Sym1 a6989586621680654120 | |
type Apply ShowsPrec_6989586621681187235Sym0 (a6989586621681187243 :: Nat) | |
Defined in Data.Singletons.Prelude.Semigroup type Apply ShowsPrec_6989586621681187235Sym0 (a6989586621681187243 :: Nat) = ShowsPrec_6989586621681187235Sym1 a6989586621681187243 | |
type Apply ShowsPrec_6989586621681187261Sym0 (a6989586621681187269 :: Nat) | |
Defined in Data.Singletons.Prelude.Semigroup type Apply ShowsPrec_6989586621681187261Sym0 (a6989586621681187269 :: Nat) = ShowsPrec_6989586621681187261Sym1 a6989586621681187269 | |
type Apply (DivModSym1 a6989586621679948486 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679948487 :: Nat) | |
type Apply (QuotRemSym1 a6989586621679948479 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679948480 :: Nat) | |
type Apply (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680765286 :: Nat) | |
type Apply (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680765297 :: Nat) | |
type Apply (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680765308 :: Nat) | |
type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680379456 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680379469 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680379449 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ShowsPrec_6989586621680636806Sym0 :: TyFun Nat ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636816 :: Nat) | |
type Apply (ShowsPrec_6989586621680653944Sym0 :: TyFun Nat (Maybe a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653954 :: Nat) | |
type Apply (EfdtNatDnSym1 a6989586621680180866 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180867 :: Nat) | |
type Apply (EfdtNatSym1 a6989586621680180940 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180941 :: Nat) | |
type Apply (EfdtNatUpSym1 a6989586621680180903 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180904 :: Nat) | |
type Apply (EnumFromThenTo_6989586621680181097Sym1 a6989586621680181109 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680181110 :: Nat) | |
type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621680379314 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ShowsPrec_6989586621680636774Sym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636780 :: Nat) | |
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636760 :: Nat) | |
type Apply (ShowsPrec_6989586621681187348Sym0 :: TyFun Nat (Min a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187356 :: Nat) | |
type Apply (ShowsPrec_6989586621681187377Sym0 :: TyFun Nat (Max a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187385 :: Nat) | |
type Apply (ShowsPrec_6989586621681187406Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187414 :: Nat) | |
type Apply (ShowsPrec_6989586621681187435Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187443 :: Nat) | |
type Apply (ShowsPrec_6989586621681187464Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187472 :: Nat) | |
Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681187464Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187472 :: Nat) = ShowsPrec_6989586621681187464Sym1 a6989586621681187472 :: TyFun (WrappedMonoid m) (Symbol ~> Symbol) -> Type | |
type Apply (ShowsPrec_6989586621681187180Sym0 :: TyFun Nat (Option a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187188 :: Nat) | |
type Apply (ShowsPrec_6989586621681012505Sym0 :: TyFun Nat (Identity a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681012513 :: Nat) | |
type Apply (ShowsPrec_6989586621680698028Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680698036 :: Nat) | |
type Apply (ShowsPrec_6989586621680698057Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680698065 :: Nat) | |
type Apply (ShowsPrec_6989586621681187209Sym0 :: TyFun Nat (Dual a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187217 :: Nat) | |
type Apply (ShowsPrec_6989586621681187290Sym0 :: TyFun Nat (Sum a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187298 :: Nat) | |
type Apply (ShowsPrec_6989586621681187319Sym0 :: TyFun Nat (Product a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681187327 :: Nat) | |
type Apply (ShowsPrec_6989586621680654038Sym0 :: TyFun Nat (NonEmpty a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680654046 :: Nat) | |
type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621680379661 :: a) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621680379670 :: a) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ToEnum_6989586621680787264Sym0 :: TyFun Nat (Proxy s) -> Type) (a6989586621680787268 :: Nat) | |
type Apply (ShowsPrec_6989586621680653998Sym0 :: TyFun Nat (Either a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621680654008 :: Nat) | |
type Apply (ShowsPrec_6989586621680636842Sym0 :: TyFun Nat ((a, b) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636848 :: Nat) | |
type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681501292 :: Nat) | |
Defined in Data.Singletons.Prelude.Monad | |
type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681501310 :: Nat) | |
Defined in Data.Singletons.Prelude.Monad | |
type Apply (ShowsPrec_6989586621681203710Sym0 :: TyFun Nat (Arg a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681203718 :: Nat) | |
type Apply (ShowsPrec_6989586621680787233Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) (a6989586621680787241 :: Nat) | |
type Apply (ShowsPrec_6989586621680636857Sym0 :: TyFun Nat ((a, b, c) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636863 :: Nat) | |
type Apply (ShowsPrec_6989586621681044663Sym0 :: TyFun Nat (Const a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681044671 :: Nat) | |
type Apply (Let6989586621680379633BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) -> Type) (p6989586621680379631 :: k1) | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680379633BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) -> Type) (p6989586621680379631 :: k1) = Let6989586621680379633BuildListSym1 p6989586621680379631 :: TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type | |
type Apply (Let6989586621681501296LoopSym0 :: TyFun k (TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type) -> Type) (cnt06989586621681501294 :: k) | |
Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681501296LoopSym0 :: TyFun k (TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type) -> Type) (cnt06989586621681501294 :: k) = Let6989586621681501296LoopSym1 cnt06989586621681501294 :: TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type | |
type Apply (Let6989586621681501314LoopSym0 :: TyFun k (TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) -> Type) (cnt06989586621681501312 :: k) | |
Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681501314LoopSym0 :: TyFun k (TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) -> Type) (cnt06989586621681501312 :: k) = Let6989586621681501314LoopSym1 cnt06989586621681501312 :: TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type | |
type Apply (ShowsPrec_6989586621680636873Sym0 :: TyFun Nat ((a, b, c, d) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636879 :: Nat) | |
type Apply (Let6989586621680379633BuildListSym1 p6989586621680379631 :: TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) (xs6989586621680379632 :: k2) | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680379633BuildListSym1 p6989586621680379631 :: TyFun k2 (TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) -> Type) (xs6989586621680379632 :: k2) = Let6989586621680379633BuildListSym2 p6989586621680379631 xs6989586621680379632 :: TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type | |
type Apply (Let6989586621680379633BuildListSym2 p6989586621680379631 xs6989586621680379632 :: TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) (a6989586621680379634 :: Nat) | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680379633BuildListSym2 p6989586621680379631 xs6989586621680379632 :: TyFun Nat ([b6989586621680375544] ~> [Nat]) -> Type) (a6989586621680379634 :: Nat) = Let6989586621680379633BuildListSym3 p6989586621680379631 xs6989586621680379632 a6989586621680379634 :: TyFun [b6989586621680375544] [Nat] -> Type | |
type Apply (ShowsPrec_6989586621680636890Sym0 :: TyFun Nat ((a, b, c, d, e) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636896 :: Nat) | |
type Apply (ShowsPrec_6989586621680636908Sym0 :: TyFun Nat ((a, b, c, d, e, f) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636914 :: Nat) | |
type Apply (ShowsPrec_6989586621680636927Sym0 :: TyFun Nat ((a, b, c, d, e, f, g) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636933 :: Nat) | |
type Apply (ToEnum_6989586621681044546Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681044550 :: Nat) | |
type Apply (FromInteger_6989586621681044643Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681044647 :: Nat) | |
type Apply (Length_6989586621680823238Sym0 :: TyFun [a] Nat -> Type) (a6989586621680823244 :: [a]) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (ListlengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680765266 :: [a]) | |
type Apply (LengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680379325 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (FromEnum_6989586621681203126Sym0 :: TyFun (Min a) Nat -> Type) (a6989586621681203130 :: Min a) | |
Defined in Data.Singletons.Prelude.Semigroup | |
type Apply (FromEnum_6989586621681203403Sym0 :: TyFun (Max a) Nat -> Type) (a6989586621681203407 :: Max a) | |
Defined in Data.Singletons.Prelude.Semigroup | |
type Apply (FromEnum_6989586621681203851Sym0 :: TyFun (First a) Nat -> Type) (a6989586621681203855 :: First a) | |
Defined in Data.Singletons.Prelude.Semigroup | |
type Apply (FromEnum_6989586621681204059Sym0 :: TyFun (Last a) Nat -> Type) (a6989586621681204063 :: Last a) | |
Defined in Data.Singletons.Prelude.Semigroup | |
type Apply (FromEnum_6989586621681204228Sym0 :: TyFun (WrappedMonoid a) Nat -> Type) (a6989586621681204232 :: WrappedMonoid a) | |
Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681204228Sym0 :: TyFun (WrappedMonoid a) Nat -> Type) (a6989586621681204232 :: WrappedMonoid a) = FromEnum_6989586621681204228Sym1 a6989586621681204232 | |
type Apply (FromEnum_6989586621681012395Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681012399 :: Identity a) | |
Defined in Data.Singletons.Prelude.Identity | |
type Apply (Length_6989586621681012654Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681012658 :: Identity a) | |
Defined in Data.Singletons.Prelude.Identity | |
type Apply (Length_6989586621680823647Sym0 :: TyFun (Dual a) Nat -> Type) (a6989586621680823651 :: Dual a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Length_6989586621680823822Sym0 :: TyFun (Sum a) Nat -> Type) (a6989586621680823826 :: Sum a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Length_6989586621680823997Sym0 :: TyFun (Product a) Nat -> Type) (a6989586621680824001 :: Product a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Length_6989586621680823002Sym0 :: TyFun (t a) Nat -> Type) (a6989586621680823008 :: t a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680822817 :: t a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (FindIndicesSym1 a6989586621680379629 :: TyFun [a] [Nat] -> Type) (a6989586621680379630 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ElemIndicesSym1 a6989586621680379661 :: TyFun [a] [Nat] -> Type) (a6989586621680379662 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (FindIndexSym1 a6989586621680379652 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680379653 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (ElemIndexSym1 a6989586621680379670 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680379671 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (Let6989586621680379633BuildListSym3 p6989586621680379631 xs6989586621680379632 a6989586621680379634 :: TyFun [b6989586621680375544] [Nat] -> Type) (a6989586621680379635 :: [b6989586621680375544]) | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680379633BuildListSym3 p6989586621680379631 xs6989586621680379632 a6989586621680379634 :: TyFun [b6989586621680375544] [Nat] -> Type) (a6989586621680379635 :: [b6989586621680375544]) = Let6989586621680379633BuildListSym4 p6989586621680379631 xs6989586621680379632 a6989586621680379634 a6989586621680379635 | |
type Apply (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680765275 :: [a]) | |
type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680379294 :: [a]) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (Let6989586621681501296LoopSym1 cnt06989586621681501294 :: TyFun (m6989586621681500906 a) (TyFun Nat (m6989586621681500906 ()) -> Type) -> Type) (f6989586621681501295 :: m6989586621681500906 a) | |
Defined in Data.Singletons.Prelude.Monad | |
type Apply (Let6989586621681501314LoopSym1 cnt06989586621681501312 :: TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) (f6989586621681501313 :: m6989586621681500908 a6989586621681500909) | |
Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681501314LoopSym1 cnt06989586621681501312 :: TyFun (m6989586621681500908 a6989586621681500909) (TyFun Nat (m6989586621681500908 [a6989586621681500909]) -> Type) -> Type) (f6989586621681501313 :: m6989586621681500908 a6989586621681500909) = Let6989586621681501314LoopSym2 cnt06989586621681501312 f6989586621681501313 | |
type Apply (Length_6989586621680823420Sym0 :: TyFun (Either a1 a2) Nat -> Type) (a6989586621680823424 :: Either a1 a2) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (Length_6989586621680823494Sym0 :: TyFun (Proxy a) Nat -> Type) (a6989586621680823498 :: Proxy a) | |
Defined in Data.Singletons.Prelude.Foldable | |
type Apply (FromEnum_6989586621680787258Sym0 :: TyFun (Proxy s) Nat -> Type) (a6989586621680787262 :: Proxy s) | |
Defined in Data.Singletons.Prelude.Proxy | |
type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621680379629 :: a ~> Bool) | |
Defined in Data.Singletons.Prelude.List.Internal | |
type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621680379652 :: a ~> Bool) | |
type Apply (FromEnum_6989586621681044553Sym0 :: TyFun (Const a b) Nat -> Type) (a6989586621681044557 :: Const a b) | |
Defined in Data.Singletons.Prelude.Const |
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat
, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Log2 (a :: Nat) :: Nat where ... #
Log base 2 (round down) of natural numbers.
Log 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
someNatVal :: Natural -> SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.10.0.0
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True infix 4 #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family Demote k = (r :: Type) | r -> k #
Instances
type family Sing :: k -> Type #
Instances
Instances
SingI n => SingI ('MaxInternal n :: MaxInternal a) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI n => SingI ('MinInternal n :: MinInternal a) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI NotSym0 | |
Defined in Data.Singletons.Prelude.Bool | |
SingI (&&@#@$) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI (||@#@$) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI Log2Sym0 | |
Defined in Data.Singletons.TypeLits | |
SingI (<=?@#@$) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI (^@#@$) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI DivSym0 | |
Defined in Data.Singletons.TypeLits | |
SingI ModSym0 | |
Defined in Data.Singletons.TypeLits | |
SingI AllSym0 | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI All_Sym0 | |
SingI AnySym0 | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI Any_Sym0 | |
SingI ShowParenSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI AndSym0 | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI OrSym0 | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI UnlinesSym0 | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI UnwordsSym0 | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI Show_tupleSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI ThenCmpSym0 | |
Defined in Data.Singletons.Prelude.Ord | |
SingI EftNatSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatDnSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI EfdtNatUpSym0 | |
Defined in Data.Singletons.Prelude.Enum | |
SingI ShowSpaceSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI ShowCommaSpaceSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI ShowCharSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI ShowStringSym0 | |
Defined in Data.Singletons.Prelude.Show | |
SingI GetAllSym0 | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI GetAnySym0 | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits | |
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) | |
Defined in Data.Singletons.TypeLits | |
SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (UnlessSym0 :: TyFun Bool (f () ~> f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (ListtransposeSym0 :: TyFun [[a]] [[a]] -> Type) | |
SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ConcatSym0 :: TyFun [[a]] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (ListtailsSym0 :: TyFun [a] [[a]] -> Type) | |
SNum a => SingI (ListsumSym0 :: TyFun [a] a -> Type) | |
SOrd a => SingI (ListsortSym0 :: TyFun [a] [a] -> Type) | |
SingI (ListreverseSym0 :: TyFun [a] [a] -> Type) | |
SNum a => SingI (ListproductSym0 :: TyFun [a] a -> Type) | |
SingI (ListnullSym0 :: TyFun [a] Bool -> Type) | |
SOrd a => SingI (ListminimumSym0 :: TyFun [a] a -> Type) | |
SOrd a => SingI (ListmaximumSym0 :: TyFun [a] a -> Type) | |
SingI (ListlengthSym0 :: TyFun [a] Nat -> Type) | |
SingI (ListlastSym0 :: TyFun [a] a -> Type) | |
SEq a => SingI (ListisPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) | |
SingI (ListinitsSym0 :: TyFun [a] [[a]] -> Type) | |
SingI (ListinitSym0 :: TyFun [a] [a] -> Type) | |
SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) | |
SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (TailsSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (TailSym0 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SNum a => SingI (SumSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ReverseSym0 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SNum a => SingI (ProductSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (NullSym0 :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (NonEmptySubsequencesSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SOrd a => SingI (MinimumSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SOrd a => SingI (MaximumSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (LengthSym0 :: TyFun [a] Nat -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (LastSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (InitsSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (InitSym0 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (HeadSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (MinInternalSym0 :: TyFun (Maybe a) (MinInternal a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI (MaxInternalSym0 :: TyFun (Maybe a) (MaxInternal a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI (OptionSym0 :: TyFun (Maybe a) (Option a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI d => SingI (Show_tupleSym1 d :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) | |
Defined in Data.Singletons.Prelude.IsString | |
SingI (Sum_Sym0 :: TyFun a (Sum a) -> Type) | |
SingI (Product_Sym0 :: TyFun a (Product a) -> Type) | |
SOrd a => SingI (Min_Sym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Ord.Disambiguation | |
SOrd a => SingI (Max_Sym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Ord.Disambiguation | |
SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (ListintersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
SOrd a => SingI (ListinsertSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
SEq a => SingI (ListelemSym0 :: TyFun a ([a] ~> Bool) -> Type) | |
SingI (PrependToAllSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (NotElemSym0 :: TyFun a ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (ElemSym0 :: TyFun a ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SEnum a => SingI (SuccSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (PredSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Eq | |
SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Eq | |
SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI (SignumSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI (NegateSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI (AbsSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI (IdSym0 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (JustSym0 :: TyFun a (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI ((:|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SingI (DownSym0 :: TyFun a (Down a) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (SumSym0 :: TyFun a (Sum a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (ProductSym0 :: TyFun a (Product a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (MinSym0 :: TyFun a (Min a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (MaxSym0 :: TyFun a (Max a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (LastSym0 :: TyFun a (Last a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (FirstSym0 :: TyFun a (First a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (DualSym0 :: TyFun a (Dual a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (GetDownSym0 :: TyFun (Down a) a -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SingI (GetMinSym0 :: TyFun (Min a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetMaxSym0 :: TyFun (Max a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetFirstSym0 :: TyFun (First a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetLastSym0 :: TyFun (Last a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (UnwrapMonoidSym0 :: TyFun (WrappedMonoid m) m -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetOptionSym0 :: TyFun (Option a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (RunIdentitySym0 :: TyFun (Identity a) a -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI (GetFirstSym0 :: TyFun (First a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (GetLastSym0 :: TyFun (Last a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (GetDualSym0 :: TyFun (Dual a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetSumSym0 :: TyFun (Sum a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI (GetProductSym0 :: TyFun (Product a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI (ListtakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
SingI (ListspanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) | |
SingI (ListsortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) | |
SingI (Listscanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) | |
SingI (ListpartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) | |
SingI (ListnubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) | |
SingI (Listfoldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) | |
SingI (Listfoldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) | |
SingI (ListfilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
SingI (ListdropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (SelectSym0 :: TyFun (a ~> Bool) (a ~> (([a], [a]) ~> ([a], [a]))) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (FindSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Elem_bySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> Bool)) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (AnySym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (AllSym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (AppEndoSym0 :: TyFun (Endo a) (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI (GetMaxInternalSym0 :: TyFun (MaxInternal a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI (GetMinInternalSym0 :: TyFun (MinInternal a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
SingI (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
SingI (ListunzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) | |
SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ListzipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) | |
SingI d => SingI (ListtakeWhileSym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (ListtakeSym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (ListsplitAtSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
SingI d => SingI (ListspanSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
SingI d => SingI (ListsortBySym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (Listscanr1Sym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (ListpartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
SingI d => SingI (ListnubBySym1 d :: TyFun [a] [a] -> Type) | |
(SEq a, SingI d) => SingI (ListisPrefixOfSym1 d :: TyFun [a] Bool -> Type) | |
SingI d => SingI (ListintersperseSym1 d :: TyFun [a] [a] -> Type) | |
(SOrd a, SingI d) => SingI (ListinsertSym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (Listfoldr1Sym1 d :: TyFun [a] a -> Type) | |
SingI d => SingI (Listfoldl1Sym1 d :: TyFun [a] a -> Type) | |
SingI d => SingI (ListfilterSym1 d :: TyFun [a] [a] -> Type) | |
(SEq a, SingI d) => SingI (ListelemSym1 d :: TyFun [a] Bool -> Type) | |
SingI d => SingI (ListdropWhileSym1 d :: TyFun [a] [a] -> Type) | |
SingI d => SingI (ListdropSym1 d :: TyFun [a] [a] -> Type) | |
(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (TakeSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (SplitAtSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (PrependToAllSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (MinimumBySym1 d :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (MaximumBySym1 d :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Foldr1Sym1 d :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Foldl1Sym1 d :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (FindSym1 d :: TyFun [a] (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (ElemSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (DropSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (AnySym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (AllSym1 d :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI ((:|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type) | |
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI (ErrorSym0 :: TyFun Symbol a -> Type) | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
SingI (SndSym0 :: TyFun (a, b) b -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
SingI (FstSym0 :: TyFun (a, b) a -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
(SOrd a, SingI d) => SingI (Min_Sym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Ord.Disambiguation | |
(SOrd a, SingI d) => SingI (Max_Sym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Ord.Disambiguation | |
SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI d => SingI (SelectSym1 d :: TyFun a (([a], [a]) ~> ([a], [a])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ReplicateSym1 d :: TyFun a [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Elem_bySym1 d :: TyFun a ([a] ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SShow a, SingI d) => SingI (ShowsPrecSym1 d :: TyFun a (Symbol ~> Symbol) -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI d => SingI (AppEndoSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Eq | |
(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Eq | |
(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Num | |
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Bool | |
SingI (SeqSym0 :: TyFun a (b ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (ConstSym0 :: TyFun a (b ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SApplicative f, SingI d) => SingI (WhenSym1 d :: TyFun (f ()) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI (RightSym0 :: TyFun b (Either a b) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI (LeftSym0 :: TyFun a (Either a b) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Monoid | |
SingI (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Proxy | |
SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
SingI (Option_Sym0 :: TyFun b ((a ~> b) ~> (Option a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup | |
SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup | |
SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) | |
Defined in Data.Singletons.Prelude.Applicative | |
(SApplicative f, SingI d) => SingI (UnlessSym1 d :: TyFun (f ()) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (ListscanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) | |
SingI (ListscanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) | |
SingI (ListmapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) | |
SingI (ListfoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) | |
SingI (ListfoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) | |
SingI (Listfoldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) | |
SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (ConcatMapSym0 :: TyFun (a ~> [b]) ([a] ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SMonadPlus m => SingI (MfilterSym0 :: TyFun (a ~> Bool) (m a ~> m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SApplicative m => SingI (FilterMSym0 :: TyFun (a ~> m Bool) ([a] ~> m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (RunStateLSym0 :: TyFun (StateL s a) (s ~> (s, a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI (RunStateRSym0 :: TyFun (StateR s a) (s ~> (s, a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI (ConstSym0 :: TyFun a (Const a b) -> Type) | |
Defined in Data.Singletons.Prelude.Const | |
SingI a => SingI ('WrapSing s :: WrappedSing a) | |
Defined in Data.Singletons.Internal | |
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) | |
Defined in Data.Singletons.Prelude.Bool | |
SMonadFail m => SingI (FailSym0 :: TyFun [Char] (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Fail | |
(SEq a, SingI d) => SingI (LookupSym1 d :: TyFun [(a, b)] (Maybe b) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI d => SingI (ListzipSym1 d :: TyFun [b] [(a, b)] -> Type) | |
SingI d => SingI (ListmapSym1 d :: TyFun [a] [b] -> Type) | |
SingI d => SingI (ZipSym1 d :: TyFun [b] [(a, b)] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (Elem_bySym2 d1 d2 :: TyFun [a] Bool -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ConcatMapSym1 d :: TyFun [a] [b] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SApplicative m, SingI d) => SingI (FilterMSym1 d :: TyFun [a] (m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) | |
Defined in Data.Singletons.Prelude.Show | |
(SingI d1, SingI d2) => SingI (SelectSym2 d1 d2 :: TyFun ([a], [a]) ([a], [a]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI d => SingI (RunStateRSym1 d :: TyFun s (s, a) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI d => SingI (RunStateLSym1 d :: TyFun s (s, a) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI d => SingI (ListscanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) | |
SingI d => SingI (ListscanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) | |
SingI d => SingI (ListfoldrSym1 d :: TyFun b ([a] ~> b) -> Type) | |
SingI d => SingI (ListfoldlSym1 d :: TyFun b ([a] ~> b) -> Type) | |
SingI d => SingI (Listfoldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) | |
SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Foldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) | |
Defined in Data.Singletons.Prelude.Enum | |
(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun (t a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (MinimumBySym1 d :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (MaximumBySym1 d :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (Foldr1Sym1 d :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (Foldl1Sym1 d :: TyFun (t a) a -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (FindSym1 d :: TyFun (t a) (Maybe a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d :: TyFun (t a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (AnySym1 d :: TyFun (t a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (AllSym1 d :: TyFun (t a) Bool -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (SeqSym1 d :: TyFun b b -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (ConstSym1 d :: TyFun b a -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (($@#@$$) d :: TyFun a b -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SAlternative f => SingI ((<|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d => SingI (Tuple2Sym1 d :: TyFun b (a, b) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d => SingI (FoldlSym1 d :: TyFun b ([a] ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
SingI d => SingI (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type) | |
Defined in Data.Singletons.Prelude.Proxy | |
SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
SingI d => SingI (ArgSym1 d :: TyFun b (Arg a b) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup | |
(SApplicative m, SingI d) => SingI (ReplicateM_Sym1 d :: TyFun (m a) (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SApplicative m, SingI d) => SingI (ReplicateMSym1 d :: TyFun (m a) (m [a]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SMonadPlus m, SingI d) => SingI (MfilterSym1 d :: TyFun (m a) (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (GetConstSym0 :: TyFun (Const a b) a -> Type) | |
Defined in Data.Singletons.Prelude.Const | |
SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI d => SingI (Maybe_Sym1 d :: TyFun (a ~> b) (Maybe a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI (ListzipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) | |
SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (MapAccumRSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (MapAccumLSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
SingI d => SingI (Option_Sym1 d :: TyFun (a ~> b) (Option a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup | |
SMonad m => SingI ((<$!>@#@$) :: TyFun (a ~> b) (m a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (ListzipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) | |
(SingI d1, SingI d2) => SingI (ListscanrSym2 d1 d2 :: TyFun [a] [b] -> Type) | |
(SingI d1, SingI d2) => SingI (ListscanlSym2 d1 d2 :: TyFun [a] [b] -> Type) | |
(SingI d1, SingI d2) => SingI (ListfoldrSym2 d1 d2 :: TyFun [a] b -> Type) | |
(SingI d1, SingI d2) => SingI (ListfoldlSym2 d1 d2 :: TyFun [a] b -> Type) | |
(SingI d1, SingI d2) => SingI (Listfoldl'Sym2 d1 d2 :: TyFun [a] b -> Type) | |
SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Zip3Sym1 d :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun [a] b -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun [a] b -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) | |
Defined in Data.Singletons.Prelude.Maybe | |
SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d :: TyFun (t a) m -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SingI d) => SingI (FmapDefaultSym1 d :: TyFun (t a) (t b) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI d => SingI (MapAccumRSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (MapAccumLSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (FoldrSym1 d :: TyFun b (t a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (Foldr'Sym1 d :: TyFun b (t a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (FoldlSym1 d :: TyFun b (t a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (Foldl'Sym1 d :: TyFun b (t a ~> b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d :: TyFun (t a) m -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d) => SingI (ConcatMapSym1 d :: TyFun (t a) [b] -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI (LiftMSym1 d :: TyFun (m a1) (m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI (LiftASym1 d :: TyFun (f a) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SFunctor f, SingI d) => SingI (FmapSym1 d :: TyFun (f a) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SAlternative f, SingI d) => SingI ((<|>@#@$$) d :: TyFun (f a) (f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI ((<**>@#@$$) d :: TyFun (f (a ~> b)) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SFunctor f, SingI d) => SingI ((<$@#@$$) d :: TyFun (f b) (f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d => SingI (Tuple3Sym1 d :: TyFun b (c ~> (a, b, c)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) | |
Defined in Data.Singletons.Prelude.Ord | |
(SFunctor f, SingI d) => SingI ((<$>@#@$$) d :: TyFun (f a) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
(SFunctor f, SingI d) => SingI (($>@#@$$) d :: TyFun b (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
(SMonad m, SingI d) => SingI ((<$!>@#@$$) d :: TyFun (m a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SingI d1, SingI d2) => SingI (Option_Sym2 d1 d2 :: TyFun (Option a) b -> Type) | |
Defined in Data.Singletons.Prelude.Semigroup | |
(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d => SingI (Either_Sym1 d :: TyFun (b ~> c) (Either a b ~> c) -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SingI d => SingI ((.@#@$$) d :: TyFun (a ~> b) (a ~> c) -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI ((>>=@#@$$) d :: TyFun (a ~> m b) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SFunctor f, SingI d) => SingI ((<&>@#@$$) d :: TyFun (a ~> b) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Functor | |
SApplicative m => SingI (ZipWithM_Sym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m ())) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SApplicative m => SingI (ZipWithMSym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m [c])) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SApplicative m => SingI (MapAndUnzipMSym0 :: TyFun (a ~> m (b, c)) ([a] ~> m ([b], [c])) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SFoldable t, SMonad m) => SingI (FoldM_Sym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m ())) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SFoldable t, SMonad m) => SingI (FoldMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SMonad m => SingI ((>=>@#@$) :: TyFun (a ~> m b) ((b ~> m c) ~> (a ~> m c)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SMonad m => SingI ((<=<@#@$) :: TyFun (b ~> m c) ((a ~> m b) ~> (a ~> m c)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (ListzipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) | |
(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 :: TyFun [c] [(a, b, c)] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SApplicative m, SingI d) => SingI (ZipWithM_Sym1 d :: TyFun [a] ([b] ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SApplicative m, SingI d) => SingI (ZipWithMSym1 d :: TyFun [a] ([b] ~> m [c]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SApplicative m, SingI d) => SingI (MapAndUnzipMSym1 d :: TyFun [a] (m ([b], [c])) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) | |
Defined in Data.Singletons.Prelude.Either | |
(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type) | |
Defined in Data.Singletons.Prelude.Tuple | |
(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d :: TyFun (t a) (f (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d :: TyFun (t a) (m (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SingI d) => SingI (MapAccumRSym1 d :: TyFun a (t b ~> (a, t c)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SingI d) => SingI (MapAccumLSym1 d :: TyFun a (t b ~> (a, t c)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d :: TyFun (t a) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d :: TyFun (t a) (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun (t a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d :: TyFun b (t a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 :: TyFun (t a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun (t a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d :: TyFun b (t a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun (t a) b -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) | |
Defined in Data.Singletons.Prelude.Base | |
(SMonad m, SingI d) => SingI (LiftM2Sym1 d :: TyFun (m a1) (m a2 ~> m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI (LiftA2Sym1 d :: TyFun (f a) (f b ~> f c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI ((>>@#@$$) d :: TyFun (m b) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI ((<*@#@$$) d :: TyFun (f b) (f a) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d) => SingI ((*>@#@$$) d :: TyFun (f b) (f b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d1 => SingI (Tuple4Sym1 d1 :: TyFun b (c ~> (d2 ~> (a, b, c, d2))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 :: TyFun c (a, b, c) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SFoldable t, SMonad m, SingI d) => SingI (FoldM_Sym1 d :: TyFun b (t a ~> m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SFoldable t, SMonad m, SingI d) => SingI (FoldMSym1 d :: TyFun b (t a ~> m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d :: TyFun (a ~> f b) (f (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d :: TyFun (a ~> m b) (m (t b)) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d :: TyFun (a ~> f b) (f ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d :: TyFun (a ~> m b) (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI ((>=>@#@$$) d :: TyFun (b ~> m c) (a ~> m c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SMonad m, SingI d) => SingI ((<=<@#@$$) d :: TyFun (a ~> m b) (a ~> m c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithM_Sym2 d1 d2 :: TyFun [b] (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithMSym2 d1 d2 :: TyFun [b] (m [c]) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun (t b) (a, t c) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun (t b) (a, t c) -> Type) | |
Defined in Data.Singletons.Prelude.Traversable | |
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 :: TyFun (t a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 :: TyFun (t a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Foldable | |
(SMonad m, SingI d) => SingI (LiftM3Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d1 => SingI (Tuple5Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (a, b, c, d2, e)))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2) => SingI (Tuple4Sym2 d1 d2 :: TyFun c (d3 ~> (a, b, c, d3)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldM_Sym2 d1 d2 :: TyFun (t a) (m ()) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldMSym2 d1 d2 :: TyFun (t a) (m b) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SMonad m, SingI d1, SingI d2) => SingI (d1 >=>@#@$$$ d2 :: TyFun a (m c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
(SMonad m, SingI d1, SingI d2) => SingI (d1 <=<@#@$$$ d2 :: TyFun a (m c) -> Type) | |
Defined in Data.Singletons.Prelude.Monad | |
SMonad m => SingI (LiftM4Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> r)))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> m r)))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Unzip7Sym0 :: TyFun [(a, b, c, d, e, f, g)] ([a], [b], [c], [d], [e], [f], [g]) -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SingI d2, SingI d3, SingI d4) => SingI (ZipWith3Sym3 d2 d3 d4 :: TyFun [c] [d1] -> Type) | |
Defined in Data.Singletons.Prelude.List.Internal | |
(SMonad m, SingI d) => SingI (LiftM4Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> m r))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2) => SingI (LiftM3Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SingI d1 => SingI (Tuple6Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (a, b, c, d2, e, f))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2) => SingI (Tuple5Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (a, b, c, d3, e))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3) => SingI (Tuple4Sym3 d1 d2 d3 :: TyFun d4 (a, b, c, d4) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
SMonad m => SingI (LiftM5Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> r))))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r))))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d) => SingI (LiftM5Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r)))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2) => SingI (LiftM4Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> m r)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM3Sym3 d1 d2 d3 :: TyFun (m a3) (m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
SingI d1 => SingI (Tuple7Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g)))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2) => SingI (Tuple6Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (a, b, c, d3, e, f)))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3) => SingI (Tuple5Sym3 d1 d2 d3 :: TyFun d4 (e ~> (a, b, c, d4, e)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SMonad m, SingI d1, SingI d2) => SingI (LiftM5Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> (m a5 ~> m r))) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM4Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SingI d1, SingI d2) => SingI (Tuple7Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (g ~> (a, b, c, d3, e, f, g))))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3) => SingI (Tuple6Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (a, b, c, d4, e, f))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple5Sym4 d1 d2 d3 d5 :: TyFun e (a, b, c, d4, e) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM5Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> (m a5 ~> m r)) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM4Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SingI d1, SingI d2, SingI d3) => SingI (Tuple7Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (g ~> (a, b, c, d4, e, f, g)))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple6Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (a, b, c, d4, e, f)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM5Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m a5 ~> m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple7Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (g ~> (a, b, c, d4, e, f, g))) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple6Sym5 d1 d2 d3 d5 d6 :: TyFun f (a, b, c, d4, e, f) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4, SingI d5) => SingI (LiftM5Sym5 d1 d2 d3 d4 d5 :: TyFun (m a5) (m r) -> Type) | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple7Sym5 d1 d2 d3 d5 d6 :: TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type) | |
Defined in Data.Singletons.Prelude.Instances | |
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d1 d2 d3 d5 d6 d7 :: TyFun g (a, b, c, d4, e, f, g) -> Type) | |
Defined in Data.Singletons.Prelude.Instances |
pattern (:<) :: (Dom f a, KnownNat n, CFreeMonoid f) => (n ~ (1 + n1), KnownNat n1) => a -> Sized f n1 a -> Sized f n a #
pattern (:>) :: (Dom f a, KnownNat n, CFreeMonoid f) => (n ~ (n1 + 1), KnownNat n1) => Sized f n1 a -> a -> Sized f n a #
generate :: forall (f :: Type -> Type) (n :: Nat) a. (CFreeMonoid f, Dom f a) => SNat n -> (Ordinal n -> a) -> Sized f n a #
sIndex :: forall (f :: Type -> Type) (n :: Nat) c. (CFoldable f, Dom f c) => Ordinal n -> Sized f n c -> c #
unsafeFromList :: forall (f :: Type -> Type) (n :: Nat) a. (CFreeMonoid f, Dom f a) => SNat n -> [a] -> Sized f n a #
unsafeFromList' :: forall (f :: Type -> Type) (n :: Nat) a. (KnownNat n, CFreeMonoid f, Dom f a) => [a] -> Sized f n a #
zipWithSame :: forall (f :: Type -> Type) (n :: Nat) a b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c #
viewNat :: forall (n :: Nat). SNat n -> ZeroOrSucc n #
pattern Zero :: () => n ~ 0 => SNat n | |
pattern Succ :: forall n n1. () => n ~ Succ n1 => SNat n1 -> SNat n |
Instances
TestEquality SNat | |
Defined in Data.Type.Natural.Core | |
Eq (SNat n) | |
Ord (SNat n) | |
Show (SNat n) | |
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r #
snat :: QuasiQuoter #
toSomeSNat :: Natural -> SomeSNat #
sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord) #
induction :: forall p (k :: Nat). p 0 -> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k #
zeroOrSucc :: forall (n :: Nat). SNat n -> ZeroOrSucc n #
type family FlipOrdering (ord :: Ordering) :: Ordering where ... #
FlipOrdering 'LT = 'GT | |
FlipOrdering 'GT = 'LT | |
FlipOrdering 'EQ = 'EQ |
data ZeroOrSucc (n :: Nat) where #
IsZero :: ZeroOrSucc 0 | |
IsSucc :: forall (n1 :: Nat). SNat n1 -> ZeroOrSucc (n1 + 1) |
data IsTrue (b :: Bool) where #
Instances
Eq (IsTrue b) | |
Data (IsTrue 'True) | |
Defined in Proof.Propositional gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsTrue 'True -> c (IsTrue 'True) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (IsTrue 'True) # toConstr :: IsTrue 'True -> Constr # dataTypeOf :: IsTrue 'True -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (IsTrue 'True)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (IsTrue 'True)) # gmapT :: (forall b. Data b => b -> b) -> IsTrue 'True -> IsTrue 'True # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r # gmapQ :: (forall d. Data d => d -> u) -> IsTrue 'True -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsTrue 'True -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # | |
Ord (IsTrue b) | |
Defined in Proof.Propositional | |
Read (IsTrue 'True) | |
Show (IsTrue b) | |
Empty (IsTrue 'False) | |
Defined in Proof.Propositional | |
Inhabited (IsTrue 'True) | |
Defined in Proof.Propositional |
withWitness :: forall (b :: Bool) r. IsTrue b -> (b ~ 'True => r) -> r #
sNatToSingleton :: SNat n -> Sing n Source #
singToSNat :: Sing n -> SNat n Source #
coerceLength :: (n :~: m) -> Sized f n a -> Sized f m a Source #
sizedLength :: (KnownNat n, DomC f a) => Sized f n a -> SNat n Source #
padVecs :: forall a n m. (Unbox a, KnownNat n, KnownNat m) => a -> USized n a -> USized m a -> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a) Source #