Literal

Defines `Literal`, a single value or array of values with a specified shape. It is similar to
the `Tensor` type, but differs in a number of important ways:

* `Literal` offers a convenient syntax for constructing `Literal`s with boolean and numeric
  contents. For example, `True`, `1` and `[1, 2, 3]` are all valid `Literal`s. This makes it
  useful for constructing `Tensor`s.
* `Literal` is *not* accelerated by XLA, so operations on large `Literal`s, and large sequences
  of operations on any `Literal`, can be expected to be slower than they would on an equivalent
  `Tensor`.
* A `Literal` is implemented in pure Idris. As such, it can contain elements of any type, and
  implements a number of standard Idris interfaces. This, along with its convenient syntax,
  makes it particularly useful for testing operations on `Tensor`s.

Reexports

Definitions

data Literal : Shape -> Type -> Type

  A scalar or array of values.

Totality: total
Visibility: public export
Constructors:

Scalar : a -> Literal [] a

Nil : Literal (0 :: ds) a

(::) : Literal ds a -> Literal (d :: ds) a -> Literal (S d :: ds) a

Hints:

Applicative (Literal shape)

Cast (Array shape a) (Literal shape a)

Eq a => Eq (Literal shape a)

Foldable (Literal shape)

Functor (Literal shape)

Num a => Num (Literal [] a)

Show a => Show (Literal shape a)

Traversable (Literal shape)

Zippable (Literal shape)

fromInteger : Integer -> Literal [] Int32

Totality: total
Visibility: export

fromDouble : Double -> Literal [] Double

Totality: total
Visibility: export

True : Literal [] Bool

  Convenience aliases for scalar boolean literals.

Totality: total
Visibility: export

False : Literal [] Bool

  Convenience aliases for scalar boolean literals.

Totality: total
Visibility: export

all : Literal shape Bool -> Bool

  `True` if no elements are `False`. `all []` is `True`.

Totality: total
Visibility: export

negate : Neg a => Literal shape a -> Literal shape a

Totality: total
Visibility: export
Fixity Declaration: prefix operator, level 10

data All : (0 _ : (a -> Type)) -> Literal shape a -> Type

  An `All p xs` is an array (or scalar) of proofs about each element in `xs`.
  
  For example, an `All IsSucc xs` proves that every element in `xs` is non-zero.

Totality: total
Visibility: public export
Constructors:

Scalar : p x -> All p (Scalar x)

Nil : All p []

(::) : All p x -> All p xs -> All p (x :: xs)