packages feed

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

PCase44.hs:(18,15)-(26,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " e of\n\
      \         Var s | s .== literal \"a\"                       -> e .== e =: qed\n\
      \               | s .== literal \"b\" .|| s .== literal \"c\" -> e .== e =: qed\n\
      \               | sTrue                                    -> e .== e =: qed\n\
      \\n\
      \         Num _ | sTrue                                    -> e .== e =: qed\n\
      \\n\
      \         _                                                -> e .== e =: qed\n\
      \       "
  ======>
    cases
      [((.&&) (isVar e) (let s = getVar_1 e in s .== literal "a")
          ==> (e .== e =: qed)),
       ((.&&)
          (isVar e)
          ((.&&)
             (sNot (let s = getVar_1 e in s .== literal "a"))
             (let s = getVar_1 e in s .== literal "b" .|| s .== literal "c"))
          ==> (e .== e =: qed)),
       ((.&&)
          (isVar e)
          ((.&&)
             (sNot (let s = getVar_1 e in s .== literal "a"))
             (sNot
                (let s = getVar_1 e in s .== literal "b" .|| s .== literal "c")))
          ==> (e .== e =: qed)),
       (isNum e ==> (e .== e =: qed)),
       (sNot
          ((.||)
             ((.||)
                ((.||)
                   ((.&&) (isVar e) (let s = getVar_1 e in s .== literal "a"))
                   ((.&&)
                      (isVar e)
                      ((.&&)
                         (sNot (let s = getVar_1 e in s .== literal "a"))
                         (let s = getVar_1 e in s .== literal "b" .|| s .== literal "c"))))
                ((.&&)
                   (isVar e)
                   ((.&&)
                      (sNot (let s = getVar_1 e in s .== literal "a"))
                      (sNot
                         (let s = getVar_1 e in s .== literal "b" .|| s .== literal "c")))))
             (isNum e))
          ==> (e .== e =: qed))]