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

PCase67.hs:(20,15)-(24,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " xs of\n\
      \         []              -> length xs .>= 0 =: qed\n\
      \         _ : (_ : _)     -> length xs .>= 0 =: qed\n\
      \         _ : _           -> length xs .>= 0 =: qed\n\
      \       "
  ======>
    cases
      [(Data.SBV.List.null xs ==> ((length xs) .>= 0 =: qed)),
       ((.&&)
          (sNot (Data.SBV.List.null xs))
          ((.&&)
             ((.===) xs (Data.SBV.List.head xs .: Data.SBV.List.tail xs))
             ((.&&)
                (sNot (Data.SBV.List.null (Data.SBV.List.tail xs)))
                ((.===)
                   (Data.SBV.List.tail xs)
                   (Data.SBV.List.head (Data.SBV.List.tail xs)
                      .: Data.SBV.List.tail (Data.SBV.List.tail xs)))))
          ==> ((length xs) .>= 0 =: qed)),
       ((.&&)
          (sNot (Data.SBV.List.null xs))
          ((.&&)
             ((.===) xs (Data.SBV.List.head xs .: Data.SBV.List.tail xs))
             (sNot
                ((.&&)
                   (sNot (Data.SBV.List.null (Data.SBV.List.tail xs)))
                   ((.===)
                      (Data.SBV.List.tail xs)
                      (Data.SBV.List.head (Data.SBV.List.tail xs)
                         .: Data.SBV.List.tail (Data.SBV.List.tail xs))))))
          ==> ((length xs) .>= 0 =: qed))]