PCase29.stderr

PCase29.hs:(18,15)-(25,9): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " e of\n\
      \         Zero                -> e .== e =: qed\n\
      \         Num k               -> sNum k .== sNum k =: e .== e =: qed\n\
      \         Var s               -> sVar s .== sVar s =: e .== e =: qed\n\
      \         Add (Num 1) (Num 2) -> sAdd (sNum 1) (sNum 2) .== sAdd (sNum 1) (sNum 2) =: e .== e =: qed\n\
      \         Add a b             -> sAdd a b .== sAdd a b =: e .== e =: qed\n\
      \         Let nm a b          -> sLet nm a b .== sLet nm a b =: e .== e =: qed\n\
      \       "
  ======>
    cases
      [(isZero e ==> (e .== e =: qed)),
       (isNum e
          ==> (let k = getNum_1 e in (sNum k) .== sNum k =: e .== e =: qed)),
       (isVar e
          ==> (let s = getVar_1 e in (sVar s) .== sVar s =: e .== e =: qed)),
       ((.&&)
          (isAdd e)
          ((.&&)
             (isNum (getAdd_1 e))
             ((.&&)
                ((.==) (getNum_1 (getAdd_1 e)) 1)
                ((.&&) (isNum (getAdd_2 e)) ((.==) (getNum_1 (getAdd_2 e)) 2))))
          ==>
            ((sAdd (sNum 1) (sNum 2)) .== sAdd (sNum 1) (sNum 2) =: e .== e
               =: qed)),
       ((.&&)
          (isAdd e)
          (sNot
             ((.&&)
                (isNum (getAdd_1 e))
                ((.&&)
                   ((.==) (getNum_1 (getAdd_1 e)) 1)
                   ((.&&) (isNum (getAdd_2 e)) ((.==) (getNum_1 (getAdd_2 e)) 2)))))
          ==>
            (let
               a = getAdd_1 e
               b = getAdd_2 e
             in (sAdd a b) .== sAdd a b =: e .== e =: qed)),
       (isLet e
          ==>
            (let
               nm = getLet_1 e
               a = getLet_2 e
               b = getLet_3 e
             in (sLet nm a b) .== sLet nm a b =: e .== e =: qed))]