packages feed

singletons-0.10.0: tests/compile-and-dump/Singletons/AtPattern.ghc76.template

Singletons/AtPattern.hs:0:0: Splicing declarations
    singletons
      [d| maybePlus :: Maybe Nat -> Maybe Nat
          maybePlus (Just n) = Just (plus (Succ Zero) n)
          maybePlus foo@Nothing = foo |]
  ======>
    Singletons/AtPattern.hs:(0,0)-(0,0)
    maybePlus :: Maybe Nat -> Maybe Nat
    maybePlus (Just n) = Just (plus (Succ Zero) n)
    maybePlus foo@Nothing = foo
    type instance MaybePlus (Just n) = Just (Plus (Succ Zero) n)
    type instance MaybePlus Nothing = Nothing
    type family MaybePlus (a :: Maybe Nat) :: Maybe Nat
    sMaybePlus :: forall (t :: Maybe Nat). Sing t -> Sing (MaybePlus t)
    sMaybePlus (SJust n) = SJust (sPlus (SSucc SZero) n)
    sMaybePlus foo@SNothing = foo