Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Some (f :: k -> Type) where
- elimKnownSymbol :: String -> (forall n. KnownSymbol n => Proxy n -> r) -> r
- keepRedundantConstraint :: c => proxy c -> ()
- checkEmptyTraversable :: Traversable t => t a -> Either a (t Void)
- dropEnds :: forall a. [a] -> Maybe (a, [a], a)
- data VerifiedSize (n :: Nat) (a :: Type) where
- VerifiedSize :: forall n a (xs :: [Type]). (SListI xs, Length xs ~ n) => NP (K a) xs -> VerifiedSize n a
- verifySize :: Sing n -> [a] -> Maybe (VerifiedSize n a)
Existentials
data Some (f :: k -> Type) where Source #
Instances
Show (Some Classified) Source # | |
Defined in Debug.RecoverRTTI.Classify |
elimKnownSymbol :: String -> (forall n. KnownSymbol n => Proxy n -> r) -> r Source #
Constraints
keepRedundantConstraint :: c => proxy c -> () Source #
Can be used to silence individual "redundant constraint" warnings
foo :: ConstraintUsefulForDebugging => ... foo = .. where _ = keepRedundantConstraint (Proxy @ConstraintUsefulForDebugging))
Traversable
checkEmptyTraversable :: Traversable t => t a -> Either a (t Void) Source #
Check if a traversable data structure is empty
Returns evidence: an element of the data-structure if it's non-empty, or evidence that it is empty otherwise.
Lists
dropEnds :: forall a. [a] -> Maybe (a, [a], a) Source #
Drop the ends of a list
dropEnds "abcde" == Just ('a',"bcd",'e')
SOP
data VerifiedSize (n :: Nat) (a :: Type) where Source #
VerifiedSize :: forall n a (xs :: [Type]). (SListI xs, Length xs ~ n) => NP (K a) xs -> VerifiedSize n a |
verifySize :: Sing n -> [a] -> Maybe (VerifiedSize n a) Source #