Data.Wrap0

(source)

This module defines `Wrap0`, a wrapper type containing a value
that is present at compile-time, but erased during run-time. This
wrapper is used to define categories with erased objects, such as
the category of types `Typ`.

Definitions

record Wrap0 : Type -> Type

  A wrapper for a value that is erased at runtime.

Totality: total
Visibility: public export
Constructor:

W0 : (0 _ : a) -> Wrap0 a

Projection:

0 .runW0 : Wrap0 a -> a

Hints:

Applicative Wrap0
Bimonoidal Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)
Braided Cat0 Cat0Prod (W0 One)
Braided Cat0 Cat0Sum (W0 Zero)
Cartesian Cat0 Cat0Prod (W0 One)
CatBifunctor Cat0 Cat0 Cat0 Cat0Prod
CatBifunctor Cat0 Cat0 Cat0 Cat0Sum
CatFunctor Linear Typ id
Category Cat0
Cocartesian Cat0 Cat0Sum (W0 Zero)
Functor Wrap0
LaxMonFunctor Linear LPair (W0 ()) Typ Pair (W0 ()) id
MonFunctor Linear LPair (W0 ()) Typ Pair (W0 ()) id
MonSymmetric Cat0 Cat0Prod (W0 One)
MonSymmetric Cat0 Cat0Sum (W0 Zero)
Monad Wrap0
Monoidal Cat0 Cat0Prod (W0 One)
Monoidal Cat0 Cat0Sum (W0 Zero)
Semigroupoid Cat0

0 .runW0 : Wrap0 a -> a

Totality: total
Visibility: public export

0 runW0 : Wrap0 a -> a

Totality: total
Visibility: public export

liftW : (0 _ : (a -> b)) -> Wrap0 a -> Wrap0 b

  Lift a function to act on `Wrap0` values. Since the values it
  operates on are erased, the function does not have to exist at
  runtime.

Totality: total
Visibility: public export

liftW2 : (0 _ : (a -> b -> c)) -> Wrap0 a -> Wrap0 b -> Wrap0 c

  Lift a binary operation to act on `Wrap0` values. Since the values
  it operates on are erased, the function does not have to exist at
  runtime.

Totality: total
Visibility: public export

Type0 : Type

  A type that is erased at runtime.

Totality: total
Visibility: public export