Contains.ghc82.template

Singletons/Contains.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| contains :: Eq a => a -> [a] -> Bool
          contains _ [] = False
          contains elt (h : t) = (elt == h) || (contains elt t) |]
  ======>
    contains :: Eq a => a -> [a] -> Bool
    contains _ GHC.Types.[] = False
    contains elt (h GHC.Types.: t) = ((elt == h) || ((contains elt) t))
    type ContainsSym2 (t :: a0123456789876543210) (t :: [a0123456789876543210]) =
        Contains t t
    instance SuppressUnusedWarnings ContainsSym1 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) ContainsSym1KindInference) GHC.Tuple.())
    data ContainsSym1 (l :: a0123456789876543210) (l :: TyFun [a0123456789876543210] Bool)
      = forall arg. SameKind (Apply (ContainsSym1 l) arg) (ContainsSym2 l arg) =>
        ContainsSym1KindInference
    type instance Apply (ContainsSym1 l) l = Contains l l
    instance SuppressUnusedWarnings ContainsSym0 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) ContainsSym0KindInference) GHC.Tuple.())
    data ContainsSym0 (l :: TyFun a0123456789876543210 (TyFun [a0123456789876543210] Bool
                                                        -> GHC.Types.Type))
      = forall arg. SameKind (Apply ContainsSym0 arg) (ContainsSym1 arg) =>
        ContainsSym0KindInference
    type instance Apply ContainsSym0 l = ContainsSym1 l
    type family Contains (a :: a) (a :: [a]) :: Bool where
      Contains _z_0123456789876543210 '[] = FalseSym0
      Contains elt ((:) h t) = Apply (Apply (:||$) (Apply (Apply (:==$) elt) h)) (Apply (Apply ContainsSym0 elt) t)
    sContains ::
      forall (t :: a) (t :: [a]).
      SEq a =>
      Sing t -> Sing t -> Sing (Apply (Apply ContainsSym0 t) t :: Bool)
    sContains _ SNil = SFalse
    sContains (sElt :: Sing elt) (SCons (sH :: Sing h) (sT :: Sing t))
      = (applySing
           ((applySing ((singFun2 @(:||$)) (%:||)))
              ((applySing ((applySing ((singFun2 @(:==$)) (%:==))) sElt)) sH)))
          ((applySing
              ((applySing ((singFun2 @ContainsSym0) sContains)) sElt))
             sT)