Modules
Top-level
Primitives
Bool
Cake
Choice
Coffee
Either
Existential
File
Fin
Fix
Graph
List
Maybe
Nat
Parallel
Prelude
Result
Stack
Vec
Module Existential
Meta-data
Contents
data
Exists
(f :
Type
->
Type
)
where
MkExists :
exists
{a:
Type
} . f a ->
Exists
f