blob: eee64362378a6e3883ff4f60ca5f7b119e736019 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T13780c where
import Data.Kind
import T13780b
type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
(pFalse :: p False) (pTrue :: p True) :: p b where
ElimBool _ _ SFalse pFalse _ = pFalse
ElimBool _ _ STrue _ pTrue = pTrue
|
