Data.Num

(source)

Definitions

applicativeNum : Num a => Applicative f => Num (f a)

Totality: total
Visibility: public export

depFunNum : {k : Fin n -> Type} -> Num ((i : Fin n) -> k i)

Totality: total
Visibility: public export

applicativeNeg : Neg a => Applicative f => Neg (f a)

Totality: total
Visibility: public export

depFunNeg : {k : Fin n -> Type} -> Neg ((i : Fin n) -> k i)

Totality: total
Visibility: public export

applicativeAbs : Abs a => Applicative f => Abs (f a)

Totality: total
Visibility: public export

applicativeFromDouble : FromDouble a => Applicative f => FromDouble (f a)

Totality: total
Visibility: public export

depFunFromDouble : {k : Fin n -> Type} -> FromDouble ((i : Fin n) -> k i)

Totality: total
Visibility: public export

applicativeFractional : Fractional a => Applicative f => Fractional (f a)

Totality: total
Visibility: public export

interface Exp : Type -> Type

  Interface for the Exponential
  We also include minus infinity because of the necessity to compute
  causal masks within the attention mechanism.
  For rules that `exp` should satisfy, see https://arxiv.org/abs/1911.04790
  We also have
  `exp . log = id`, `log . exp = id`, `exp minusInfinity = 0`...

Parameters: a
Constraints: Num a
Constructor:

MkExp

Methods:

exp : a -> a
log : a -> a
minusInfinity : a

Implementations:

Exp a => AllC TensorMonoid shape => Exp (Tensor shape a)
Exp Double

exp : Exp a => a -> a

Totality: total
Visibility: public export

log : Exp a => a -> a

Totality: total
Visibility: public export

minusInfinity : Exp a => a

Totality: total
Visibility: public export

applicativeExp : Exp a => Applicative f => Exp (f a)

Totality: total
Visibility: public export

interface Sqrt : Type -> Type

Parameters: a
Constraints: Num a
Constructor:

MkSqrt

Methods:

sqrt : a -> a

Implementations:

Sqrt a => AllC TensorMonoid shape => Sqrt (Tensor shape a)
Sqrt Double
Sqrt ()
Sqrt a => Sqrt b => Sqrt (a, b)
Sqrt a => Sqrt b => Sqrt (DPair a (const b))

sqrt : Sqrt a => a -> a

Totality: total
Visibility: public export

applicativeSqrt : Sqrt a => Applicative f => Sqrt (f a)

Totality: total
Visibility: public export