PCase66.stderr

PCase66.hs:(19,15)-(23,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " xs of\n\
      \         []             -> xs .== xs =: qed\n\
      \         y : _ | y .> 0 -> xs .== xs =: qed\n\
      \         _              -> xs .== xs =: qed\n\
      \       "
  ======>
    cases
      [(Data.SBV.List.null xs ==> (xs .== xs =: qed)),
       ((.&&)
          (sNot (Data.SBV.List.null xs))
          ((.&&)
             ((.===) xs (Data.SBV.List.head xs .: Data.SBV.List.tail xs))
             (let y = Data.SBV.List.head xs in y .> 0))
          ==> (xs .== xs =: qed)),
       (sNot
          ((.||)
             (Data.SBV.List.null xs)
             ((.&&)
                (sNot (Data.SBV.List.null xs))
                ((.&&)
                   ((.===) xs (Data.SBV.List.head xs .: Data.SBV.List.tail xs))
                   (let y = Data.SBV.List.head xs in y .> 0))))
          ==> (xs .== xs =: qed))]