    -- | Formally analyze streams.
    module Copilot.Library.Analysis
        ( triviallyTrue
        , triviallyFalse
        )
      where

    -- External imports.
    import Prelude hiding (not)

    -- Internal imports.
    import Copilot.Language      (Stream, forAll, not)
    import Copilot.Language.Spec (Prop, Universal)

    -- | Property that captures whether a stream is trivially true, meaning that
    -- there is no way to make it false.
    triviallyTrue :: Stream Bool -> Prop Universal
    triviallyTrue :: Stream Bool -> Prop Universal
    triviallyTrue = Stream Bool -> Prop Universal
    forAll

    -- | Property that captures whether a stream is trivially false, meaning that
    -- there is no way to make it true.
    triviallyFalse :: Stream Bool -> Prop Universal
    triviallyFalse :: Stream Bool -> Prop Universal
    triviallyFalse = Stream Bool -> Prop Universal
    triviallyTrue (Stream Bool -> Prop Universal)
    -> (Stream Bool -> Stream Bool) -> Stream Bool -> Prop Universal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Stream Bool -> Stream Bool
    not