IdrisDoc: Data.Erased

Data.Erased

data Erased : Type -> Type

The erasure monad.

Used when explicit modelling of erasure in the type system is needed.

Erase : (x : a) -> Erased a

Construct an erased value from any value.

unerase : Erased a -> a

Project the erased value out of the monad.

This is usable only in types and other erased contexts,
where it won't cause erasure violations.