Hoogle Search
Within LTS Haskell 24.33 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
asSingleton :: forall (w :: Nat) . Domain w -> Maybe Integerwhat4 What4.Utils.BVDomain.Bitwise Test if this domain contains a single value, and return it if so
asSingleton :: forall (w :: Nat) . Domain w -> Maybe Integerwhat4 What4.Utils.BVDomain.XOR Test if this domain contains a single value, and return it if so
isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe bAgda Agda.Termination.SparseMatrix Returns 'Just b' iff it is a 1x1 matrix with just one entry b. O(1).
feSingleton :: FreeEnv' a b c -> Maybe Variable -> cAgda Agda.TypeChecking.Free.Lazy Method to return a single variable.
isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m BoolAgda Agda.TypeChecking.Records Is the type a hereditarily singleton record type? May return a blocking metavariable. Precondition: The name should refer to a record type, and the arguments should be the parameters to the type.
-
Agda Agda.TypeChecking.Records Return the unique (closed) inhabitant if exists. In case of counting irrelevance in, the returned inhabitant contains dummy terms.
isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m) => QName -> Args -> m BoolAgda Agda.TypeChecking.Records No documentation available.
isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)Agda Agda.TypeChecking.Records Check whether a type has a unique inhabitant and return it. Can be blocked by a metavar.
isSingletonType' :: (PureTCM m, MonadBlock m) => Bool -> Type -> Set QName -> m (Maybe Term)Agda Agda.TypeChecking.Records No documentation available.
isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m BoolAgda Agda.TypeChecking.Records Check whether a type has a unique inhabitant (irrelevant parts ignored). Can be blocked by a metavar.