blob: 78e09f5ef11bc9ec35ee20e81ee975e087f79365 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
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
|
