Libraries.Data.Erased

Definitions

record Erased : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkErased : (0 _ : a) -> Erased a

Projection: 

0 .runErased : Erased a -> a

Hints:

Applicative Erased

Functor Erased

Monad Erased

0 .runErased : Erased a -> a

Totality: total
Visibility: public export

0 runErased : Erased a -> a

Totality: total
Visibility: public export