Idris2Doc : Data.NumIdr.Scalar

Data.NumIdr.Scalar

(source)
Reexports
import public Data.NumIdr.Array
Definitions
Scalar : Type -> Type
  Scalars are `Array []`, the unique 0-rank array type. They hold a single value.
  Scalars are not particularly useful as data structures, but they are
  included here anyways.

  Totality: total
  Visibility: public export
scalar : a -> Scalar a
  Convert a value to a scalar.

  Totality: total
  Visibility: export
unwrap : Scalar a -> a
  Unwrap the single value from a scalar.

  Totality: total
  Visibility: export