hetmet_brak,
hetmet_esc,
hetmet_csp,
+ hetmet_kappa,
+ hetmet_kappa_app,
GuestIntegerLiteral, guestIntegerLiteral,
GuestStringLiteral, guestStringLiteral,
GuestCharLiteral, guestCharLiteral
) where
-hetmet_brak :: forall (c :: * -> * -> *). forall a. a -> <[a]>@c
+hetmet_brak :: forall (c :: * -> * -> *). forall a. a -> <{a}>@c
hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
-hetmet_esc :: forall (c :: * -> * -> *). forall a. <[a]>@c -> a
+hetmet_esc :: forall (c :: * -> * -> *). forall a. <{a}>@c -> a
hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?"
hetmet_csp :: forall (c :: * -> * -> *). forall a. a -> a
hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
+hetmet_kappa :: forall a b c . (( () -> a ) -> ( b -> c )) -> ( (a,b) -> c )
+hetmet_kappa = Prelude.error "hetmet_kappa should never be evaluated; did you forget to compile with -fcoqpass?"
+
+hetmet_kappa_app :: forall a b c . ( (a,b) -> c ) -> ( () -> a ) -> ( b -> c )
+hetmet_kappa_app = Prelude.error "hetmet_kappa_app should never be evaluated; did you forget to compile with -fcoqpass?"
+
-- Technically these functions ought to be invoked *during
-- compilation*; in the future I would like to use Template Haskell to
-- do that.
class GuestIntegerLiteral c where
- guestIntegerLiteral :: Integer -> <[ Integer ]>@c
+ guestIntegerLiteral :: Integer -> <{ Integer }>@c
class GuestStringLiteral c where
- guestStringLiteral :: String -> <[ String ]>@c
+ guestStringLiteral :: String -> <{ String }>@c
class GuestCharLiteral c where
- guestCharLiteral :: Char -> <[ Char ]>@c
+ guestCharLiteral :: Char -> <{ Char }>@c