packages feed

sbv-14.0: SBVTestSuite/TestSuite/CompileTests/PCase/PCase57.stderr

PCase57.hs:(18,15)-(22,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " e of\n\
      \         Add (Num i) _ | i .> 0  -> sNum i .== sNum i =: e .== e =: qed\n\
      \         Add _ _                  -> e .== e =: qed\n\
      \         _                        -> e .== e =: qed\n\
      \       "
  ======>
    cases
      [((.&&)
          (isAdd e)
          ((.&&)
             (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0))
          ==>
            (let i = getNum_1 (getAdd_1 e)
             in (sNum i) .== sNum i =: e .== e =: qed)),
       ((.&&)
          (isAdd e)
          (sNot
             ((.&&)
                (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0)))
          ==> (e .== e =: qed)),
       (sNot
          ((.||)
             ((.&&)
                (isAdd e)
                ((.&&)
                   (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0)))
             ((.&&)
                (isAdd e)
                (sNot
                   ((.&&)
                      (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0)))))
          ==> (e .== e =: qed))]