Module Existential

Meta-data

Contents

data Exists (f : Type -> Type) where
    MkExists : (exists {a : Type} . f a) -> Exists f