sbv-14.0: SBVTestSuite/TestSuite/CompileTests/PCase/PCase39.stderr
PCase39.hs:(19,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 i) _ -> sNum i .== sNum i =: 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))
==>
(let i = getNum_1 (getAdd_1 e)
in (sNum i) .== sNum i =: 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))]