    module Clash.Verification.DSL where

    import qualified Clash.Verification           as Cv
    import           Clash.Verification.Internal

    -- Precedences taken from:
    --
    --   Table 2—FL operator precedence and associativity
    --
    -- of
    --
    --   IEEE Std 1850-2010a, Annex B.1, p149

    infixr 5 |&|
    (|&|) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a |&| :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    |&| b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.and a
    a b
    b
    {-# INLINE (|&|) #-}

    infixr 4 |||
    (|||) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a ||| :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    ||| b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.or a
    a b
    b
    {-# INLINE (|||) #-}

    (~>) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a ~> :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    ~> b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.implies a
    a b
    b
    {-# INLINE (~>) #-}
    infixr 0 ~>

    (|=>) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a |=> :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    |=> b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.timplies a
    a b
    b
    {-# INLINE (|=>) #-}
    infixr 1 |=>

    (|->) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a |-> :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    |-> b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.timpliesOverlapping a
    a b
    b
    {-# INLINE (|->) #-}
    infixr 1 |->

    (#|#) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    a
    a #|# :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    #|# b
    b = a -> b -> Assertion dom
    forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    Cv.before a
    a b
    b
    {-# INLINE (#|#) #-}
    infixr 3 #|#