Hoogle Search

Within LTS Haskell 24.28 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. oddSequence2 :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.StrongInduction

    Prove that the sequence 1, 3, 2 S_{k-1} - S_{k-2} generates sequence of odd numbers. We have: 

    >>> oddSequence2
Lemma: oddSequence_0                              Q.E.D.
Lemma: oddSequence_1                              Q.E.D.
Inductive lemma (strong): oddSequence_sNp2
Step: Measure is non-negative                   Q.E.D.
Step: 1                                         Q.E.D.
Step: 2                                         Q.E.D.
Step: 3 (simplify)                              Q.E.D.
Step: 4                                         Q.E.D.
Step: 5 (simplify)                              Q.E.D.
Step: 6                                         Q.E.D.
Result:                                         Q.E.D.
Lemma: oddSequence2
Step: 1 (3 way case split)
Step: 1.1                                     Q.E.D.
Step: 1.2                                     Q.E.D.
Step: 1.3.1                                   Q.E.D.
Step: 1.3.2                                   Q.E.D.
Step: 1.Completeness                          Q.E.D.
Result:                                         Q.E.D.
[Proven] oddSequence2

  2. validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool

    sbv Documentation.SBV.Examples.Lists.BoundedMutex

    A sequence is valid upto a bound if it starts at Idle, and follows the mutex rules. That is:

    The variable me identifies the agent id.

  3. isSubsequenceOf :: (Monad m, Eq a) => Stream m a -> Stream m a -> m Bool

    streamly-core Streamly.Data.Stream

    Returns True if all the elements of the first stream occur, in order, in the second stream. The elements do not have to occur consecutively. A stream is a subsequence of itself. 

    >>> Stream.isSubsequenceOf (Stream.fromList "hlo") (Stream.fromList "hello" :: Stream IO Char)
True

  4. concatSequence :: forall (m :: Type -> Type) b c t a . Fold m b c -> t (Fold m a b) -> Fold m a c

    streamly-core Streamly.Internal.Data.Fold

    concatSequence f t applies folds from stream t sequentially and collects the results using the fold f. Unimplemented

  5. subsequenceBy :: forall a (m :: Type -> Type) . (a -> a -> Bool) -> Stream m a -> Parser a m ()

    streamly-core Streamly.Internal.Data.Parser

    Match if the input stream is a subsequence of the argument stream i.e. all the elements of the input stream occur, in order, in the argument stream. The elements do not have to occur consecutively. A sequence is considered a subsequence of itself.

  6. foldSequence :: forall (m :: Type -> Type) a b . Stream m (Fold m a b) -> Stream m a -> Stream m b

    streamly-core Streamly.Internal.Data.Stream

    Apply a stream of folds to an input stream and emit the results in the output stream. Unimplemented

  7. isSubsequenceOf :: (Monad m, Eq a) => Stream m a -> Stream m a -> m Bool

    streamly-core Streamly.Internal.Data.Stream

    Returns True if all the elements of the first stream occur, in order, in the second stream. The elements do not have to occur consecutively. A stream is a subsequence of itself. 

    >>> Stream.isSubsequenceOf (Stream.fromList "hlo") (Stream.fromList "hello" :: Stream IO Char)
True

  8. parseSequence :: forall (m :: Type -> Type) a b . Stream m (Parser a m b) -> Stream m a -> Stream m b

    streamly-core Streamly.Internal.Data.Stream

    Apply a stream of parsers to an input stream and emit the results in the output stream. Unimplemented

  9. renderSequence :: (Storable y, C q y, C u, C q) => ChunkSize -> T u q -> T StrictTime [Signal s u q (T y)] -> Signal s u q (T y)

    synthesizer-midi Synthesizer.MIDI.Dimensional

    No documentation available.

  10. type FilterSequence event signal = Filter event T ShortStrictTime signal

    synthesizer-midi Synthesizer.MIDI.Generic

    No documentation available.

Page 71 of many | Previous | Next