reg055a.idr

module Foo

data Cheat : Type -> Type where
     CAny : a -> Cheat a
     CInt : Cheat Int

foo : Cheat a -> Int
foo (CAny Nothing) = 42 
foo (CAny (Just x)) = 43 
foo CInt = 0 

apply : (a -> a -> b) -> a -> a
apply (\x => \y => x) a = a
apply f a = a