Data.Num

Definitions

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
Methods:

exp : a -> a

log : a -> a

minusInfinity : a

Implementations:

Exp a => All TensorMonoid (conts shape) => Exp (Tensor shape a)

Exp Double

exp : Exp a => a -> a

Visibility: public export

log : Exp a => a -> a

Visibility: public export

minusInfinity : Exp a => a

Visibility: public export

interface Sqrt : Type -> Type

Parameters: a
Constraints: Num a
Methods:

sqrt : a -> a

Implementations:

Sqrt Double

Sqrt ()

Sqrt a => Sqrt b => Sqrt (a, b)

Sqrt a => Sqrt b => Sqrt (DPair a (const b))

sqrt : Sqrt a => a -> a

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export