| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Lib.Data.List
Description
Synopsis
- (!!~) :: (MonadUnion uf, MonadError e uf, TransformError ArrayException e, Mergeable a) => [a] -> SymInteger -> uf a
- symFilter :: (MonadUnion u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
- symTake :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a]
- symDrop :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a]
Symbolic versions of List operations
(!!~) :: (MonadUnion uf, MonadError e uf, TransformError ArrayException e, Mergeable a) => [a] -> SymInteger -> uf a Source #
Symbolic version of !!, the result would be merged and
propagate the mergeable knowledge.
symFilter :: (MonadUnion u, Mergeable a) => (a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of filter, the result would be merged and
propagate the mergeable knowledge.
symTake :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a] Source #
Symbolic version of take, the result would be merged and
propagate the mergeable knowledge.
symDrop :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a] Source #
Symbolic version of drop, the result would be merged and
propagate the mergeable knowledge.