hls-tactics-plugin-1.3.0.0: test/golden/MetaPointwise.hs
import Data.Monoid data Foo = Foo (Sum Int) (Sum Int) mappend2 :: Foo -> Foo -> Foo mappend2 = [wingman| intros f1 f2, destruct_all, ctor Foo; pointwise (use mappend); assumption|]
import Data.Monoid data Foo = Foo (Sum Int) (Sum Int) mappend2 :: Foo -> Foo -> Foo mappend2 = [wingman| intros f1 f2, destruct_all, ctor Foo; pointwise (use mappend); assumption|]