Idris2Doc : Data.Double.Bounded

Data.Double.Bounded

(source)
Reexports
import public Data.So
Definitions
OR : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 0
PosInf : Double
  Totality: total
  Visibility: public export
NegInf : Double
  Totality: total
  Visibility: public export
MinDouble : Double
  Totality: total
  Visibility: public export
MaxDouble : Double
  Totality: total
  Visibility: public export
min4 : Double -> Double -> Double -> Double -> Double
  Totality: total
  Visibility: public export
min6 : Double -> Double -> Double -> Double -> Double -> Double -> Double
  Totality: total
  Visibility: public export
max4 : Double -> Double -> Double -> Double -> Double
  Totality: total
  Visibility: public export
max6 : Double -> Double -> Double -> Double -> Double -> Double -> Double
  Totality: total
  Visibility: public export
zormin : Double -> Double -> Double
  Totality: total
  Visibility: public export
Finite : Double -> Type
  Totality: total
  Visibility: public export
NonZero : Double -> Type
  Totality: total
  Visibility: public export
lteRefl : {auto 0 _ : So (x == x)} -> So (x <= x)
  Totality: total
  Visibility: export
lteNotNaNL : {auto 0 _ : So (x <= y)} -> So (x == x)
  Totality: total
  Visibility: export
lteNotNaNR : {auto 0 _ : So (y <= x)} -> So (x == x)
  Totality: total
  Visibility: export
lteTrans : {auto 0 _ : So (a <= b)} -> {auto 0 _ : So (b <= c)} -> So (a <= c)
  Totality: total
  Visibility: export
lteNegInf : {auto 0 _ : So (x == x)} -> So (NegInf <= x)
  Totality: total
  Visibility: export
ltePosInf : {auto 0 _ : So (x == x)} -> So (x <= PosInf)
  Totality: total
  Visibility: export
lteMin : {auto 0 _ : So (x == x)} -> {auto 0 _ : Finite x} -> So (MinDouble <= x)
  Totality: total
  Visibility: export
lteMax : {auto 0 _ : So (x == x)} -> {auto 0 _ : Finite x} -> So (x <= MaxDouble)
  Totality: total
  Visibility: export
lteFromLt : {auto 0 _ : So (x < y)} -> So (x <= y)
  Totality: total
  Visibility: export
lteRev : {auto 0 _ : So (x == x)} -> {auto 0 _ : So (y == y)} -> {auto 0 _ : So (not (x <= y))} -> So (y < x)
  Totality: total
  Visibility: export
data DoubleBetween : Double -> Double -> Type
  The type of double in the given bounds.
  
  Both bounds and the value can be infinite.
  If either bounds is `NaN`, the type is uninhabited.
  The internal double value cannot be `NaN` since to inhabit the constructor,
  one needs to satisfy the bounds which is impossible with `NaN` value.

  Totality: total
  Visibility: public export
  Constructor: 
BoundedDouble : (x : Double) -> {auto 0 _ : So (lower <= x)} -> {auto 0 _ : So (x <= upper)} -> DoubleBetween lower upper

  Hints:
  
Cast (DoubleBetween l u) Double
  
Cast Nat (DoubleBetween 0.0 PosInf)
  
Eq (DoubleBetween l u)
  
Ord (DoubleBetween l u)
  
Show (DoubleBetween l u)
SolidDouble : Type
  Represents a bounded double which can hold any `Double` except the `NaN`.
  Actually, an alias for `DoubleBetween` with infinite bounds.

  Totality: total
  Visibility: public export
FiniteDouble : Type
  Totality: total
  Visibility: public export
maybeBoundedDouble : Double -> Maybe (DoubleBetween lower upper)
  Totality: total
  Visibility: public export
roughlyFit : {auto 0 _ : So (l <= u)} -> Double -> DoubleBetween l u
  Totality: total
  Visibility: public export
.asDouble : DoubleBetween l u -> Double
  Totality: total
  Visibility: public export
weakenBounds : DoubleBetween l u -> {auto 0 _ : So (l' <= l)} -> {auto 0 _ : So (u <= u')} -> DoubleBetween l' u'
  Totality: total
  Visibility: public export
relaxToSolid : DoubleBetween l u -> SolidDouble
  Totality: total
  Visibility: public export
relaxToFinite : {auto 0 _ : Finite l} -> {auto 0 _ : Finite u} -> DoubleBetween l u -> FiniteDouble
  Totality: total
  Visibility: public export
strengthenBounds : DoubleBetween l u -> Maybe (DoubleBetween l' u')
  Totality: total
  Visibility: public export
fromNat : Nat -> DoubleBetween 0.0 PosInf
  Totality: total
  Visibility: export
fromDouble : (x : Double) -> {auto 0 _ : So (x == x)} -> DoubleBetween x x
  Totality: total
  Visibility: public export
fromInteger : (x : Integer) -> {auto 0 _ : So (cast x == cast x)} -> DoubleBetween (cast x) (cast x)
  Totality: total
  Visibility: public export
fromDouble : (x : Double) -> {auto 0 _ : So (lower <= x)} -> {auto 0 _ : So (x <= upper)} -> DoubleBetween lower upper
  Totality: total
  Visibility: public export
fromInteger : (x : Integer) -> {auto 0 _ : So (lower <= cast x)} -> {auto 0 _ : So (cast x <= upper)} -> DoubleBetween lower upper
  Totality: total
  Visibility: public export
NegInf : {auto 0 _ : So (u == u)} -> DoubleBetween NegInf u
  Totality: total
  Visibility: public export
PosInf : {auto 0 _ : So (l == l)} -> DoubleBetween l PosInf
  Totality: total
  Visibility: public export
pi : DoubleBetween pi pi
  Totality: total
  Visibility: public export
Pi : DoubleBetween pi pi
  Totality: total
  Visibility: public export
euler : DoubleBetween euler euler
  Totality: total
  Visibility: public export
Euler : DoubleBetween euler euler
  Totality: total
  Visibility: public export
strengthenRight : (x : DoubleBetween l u) -> (y : DoubleBetween l u) -> {auto 0 _ : So (x <= y)} -> Subset (DoubleBetween (x .asDouble) u) (\y' => y' .asDouble = y .asDouble)
  Totality: total
  Visibility: export
bisect : (m : DoubleBetween l u) -> DoubleBetween l u -> DoubleBetween l (m .asDouble) `OR` DoubleBetween (m .asDouble) u
  Totality: total
  Visibility: export
trisect : (m1 : DoubleBetween l u) -> (m2 : DoubleBetween l u) -> {auto 0 _ : So (m1 <= m2)} -> DoubleBetween l u -> DoubleBetween l (m1 .asDouble) `OR` (DoubleBetween (m1 .asDouble) (m2 .asDouble) `OR` DoubleBetween (m2 .asDouble) u)
  Totality: total
  Visibility: export
(+) : DoubleBetween l u -> DoubleBetween l' u' -> {auto 0 _ : Finite l `OR` (Finite l' `OR` So (l == l'))} -> {auto 0 _ : Finite u `OR` (Finite u' `OR` So (u == u'))} -> DoubleBetween (l + l') (u + u')
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8
negate : Neg ty => ty -> ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 10
(-) : DoubleBetween l u -> DoubleBetween l' u' -> {auto 0 _ : Finite l `OR` (Finite u' `OR` So (l /= u'))} -> {auto 0 _ : Finite u `OR` (Finite l' `OR` So (u /= l'))} -> DoubleBetween (l - u') (u - l')
  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 8
prefix operator, level 10
(*) : DoubleBetween l u -> DoubleBetween l' u' -> {auto 0 _ : Finite l `OR` NonZero l'} -> {auto 0 _ : Finite l `OR` NonZero u'} -> {auto 0 _ : Finite u `OR` NonZero l'} -> {auto 0 _ : Finite u `OR` NonZero u'} -> {auto 0 _ : Finite l' `OR` NonZero l} -> {auto 0 _ : Finite l' `OR` NonZero u} -> {auto 0 _ : Finite u' `OR` NonZero l} -> {auto 0 _ : Finite u' `OR` NonZero u} -> DoubleBetween (min4 (l * l') (l * u') (u * l') (u * u')) (max4 (l * l') (l * u') (u * l') (u * u'))
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 9
(/) : (num : DoubleBetween l u) -> (den : DoubleBetween l' u') -> {auto 0 _ : So (0.0 < l') `OR` (So (u' < 0.0) `OR` So ((l' < 0.0) && Delay ((0.0 < u') && Delay ((l /= 0.0) && Delay (u /= 0.0)))))} -> {auto 0 _ : So (0.0 < l) `OR` (So (u < 0.0) `OR` (So (0.0 < l') `OR` (So (u' < 0.0) `OR` (NonZero (num .asDouble), NonZero (den .asDouble)))))} -> {auto 0 _ : Finite l `OR` Finite l'} -> {auto 0 _ : Finite l `OR` Finite u'} -> {auto 0 _ : Finite u `OR` Finite l'} -> {auto 0 _ : Finite u `OR` Finite u'} -> {auto 0 _ : NonZero l `OR` NonZero l'} -> {auto 0 _ : NonZero l `OR` NonZero u'} -> {auto 0 _ : NonZero u `OR` NonZero l'} -> {auto 0 _ : NonZero u `OR` NonZero u'} -> DoubleBetween (min6 (l / l') (l / u') (u / l') (u / u') (l / zormin l' u') (u / zormin l' u')) (max6 (l / l') (l / u') (u / l') (u / u') (l / zormin l' u') (u / zormin l' u'))
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 9
negate : DoubleBetween l u -> DoubleBetween (negate u) (negate l)
  Totality: total
  Visibility: export
  Fixity Declaration: prefix operator, level 10
sqrt : {auto 0 _ : So (0.0 <= l)} -> DoubleBetween l u -> DoubleBetween (sqrt l) (sqrt u)
  Totality: total
  Visibility: export
sqrtRelaxed : {auto 0 _ : So (0.0 <= l)} -> DoubleBetween l u -> DoubleBetween 0.0 PosInf
  Totality: total
  Visibility: export
log : {auto 0 _ : So (0.0 <= l)} -> DoubleBetween l u -> DoubleBetween (log l) (log u)
  Totality: total
  Visibility: export
exp : DoubleBetween l u -> DoubleBetween (exp l) (exp u)
  Totality: total
  Visibility: export
expRelaxed : DoubleBetween l u -> DoubleBetween 0.0 PosInf
  Totality: total
  Visibility: export
pow2 : DoubleBetween l u -> DoubleBetween (pow 2.0 l) (pow 2.0 u)
  Totality: total
  Visibility: export
sin : FiniteDouble -> DoubleBetween -1.0 1.0
  Totality: total
  Visibility: export
cos : FiniteDouble -> DoubleBetween -1.0 1.0
  Totality: total
  Visibility: export
asin : DoubleBetween -1.0 1.0 -> DoubleBetween (negate pi / 2.0) (pi / 2.0)
  Totality: total
  Visibility: export
acos : DoubleBetween -1.0 1.0 -> DoubleBetween 0.0 pi
  Totality: total
  Visibility: export