Data.Materialise

Definitions

interface Materialise : Type -> Type

  Used for `Data.Tensor` and structures thereof: directly evaluates the tensor
  instead of keeping it tabulated form
  There's probably a more principled solution

Parameters: a
Constructor: 

MkMaterialise

Methods:

materialise : a -> a

materialiseIsId : materialise x = x

  Extensionally the data is equivalent

Implementations:

AllC IsConcrete shape => Materialise (Tensor shape a)

Materialise Double

Materialise Integer

Materialise Nat

Materialise ()

Materialise a => Materialise b => Materialise (a, b)

materialise : Materialise a => a -> a

Totality: total
Visibility: public export

materialiseIsId : {auto __con : Materialise a} -> materialise x = x

  Extensionally the data is equivalent

Totality: total
Visibility: public export