Idris2Doc : Numeric.Log

Numeric.Log

(source)

Definitions

isInf : (FromDoublea, (Eqa, Fractionala)) =>a->Bool
  Numeric utility functions

Visibility: export
negInf : (Nega, Fractionala) =>a
Visibility: export
recordLog : Type->Type
  Log Domain

Totality: total
Visibility: public export
Constructor: 
Exp : a->Loga

Projection: 
.ln : Loga->a

Hints:
Abs (LogDouble)
Eqa=>Eq (Loga)
Fractional (LogDouble)
FunctorLog
Neg (LogDouble)
Num (LogDouble)
Orda=>Ord (Loga)
Show (LogDouble)
.ln : Loga->a
Visibility: public export
ln : Loga->a
Visibility: public export
interfaceToLogDomain : Type->Type
  Explicitly convert a value to the log domain

Parameters: a
Methods:
toLogDomain : a->LogDouble

Implementations:
ToLogDomainDouble
ToLogDomainNat
ToLogDomainInt
ToLogDomainInteger
toLogDomain : ToLogDomaina=>a->LogDouble
Visibility: public export
fromLogDomain : LogDouble->Double
  Explicitly convert a double from the log domain

Visibility: public export
sum : Foldablef=>f (LogDouble) ->LogDouble
Visibility: export