PCase56.stderr

PCase56.hs:(18,15)-(23,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " e of\n\
      \         Add (Num i) _ | i .> 0  -> e .== e =: qed\n\
      \         Add _ _                  -> e .== e =: qed\n\
      \         _ | isZero e             -> e .== e =: qed\n\
      \           | sTrue                -> e .== e =: qed\n\
      \       "
  ======>
    cases
      [((.&&)
          (isAdd e)
          ((.&&)
             (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0))
          ==> (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))))))
          (isZero e)
          ==> (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)))))
             ((.&&)
                (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))))))
                (isZero e)))
          ==> (e .== e =: qed))]