Idris2Doc : Data.Fixed

Data.Fixed

(source)
Definitions
data Fixed : Integer -> Type
  The type of fixed-point fractional numbers.

  Totality: total
  Visibility: public export
  Constructor: 
MkFixed : Integer -> Fixed res

  Hints:
  
Eq (Fixed n)
  
Fractional (Fixed n)
  
Neg (Fixed n)
  
Num (Fixed n)
  
Ord (Fixed n)
  
Show (Fixed n)
Uni : Type
  +------------+---------------------+------+------------+
  | Resolution | Scaling Factor      | Type | show 12345 |
  +============+=====================+======+============+
  | E0         | 1\1                 | Uni  | 12345.0    |
  +------------+---------------------+------+------------+

  Visibility: public export
Deci : Type
  +------------+---------------------+------+------------+
  | Resolution | Scaling Factor      | Type | show 12345 |
  +============+=====================+======+============+
  | E1         | 1\10                | Deci | 1234.5     |
  +------------+---------------------+------+------------+

  Visibility: public export
Centi : Type
  +------------+---------------------+-------+------------+
  | Resolution | Scaling Factor      | Type  | show 12345 |
  +============+=====================+=======+============+
  | E2         | 1\100               | Centi | 123.45     |
  +------------+---------------------+-------+------------+

  Visibility: public export
Milli : Type
  +------------+--------------------+-------+------------+
  | Resolution | Scaling Factor     | Type  | show 12345 |
  +============+====================+=======+============+
  | E3         | 1\1000             | Milli | 12.345     |
  +------------+--------------------+-------+------------+

  Visibility: public export
TenthMilli : Type
  +------------+--------------------+------------+------------+
  | Resolution | Scaling Factor     | Type       | show 12345 |
  +============+====================+=======+=================+
  | E4         | 1\10000            | TenthMilli | 1.2345     |
  +------------+--------------------+------------+------------+

  Visibility: public export
HundredthMilli : Type
  +------------+--------------------+------------------------+------------+
  | Resolution | Scaling Factor     | Type                   | show 12345 |
  +============+====================+========================+============+
  | E5         | 1\100000           | HundredthMilli         | 0.12345    |
  +------------+--------------------+------------------------+------------+

  Visibility: public export
Micro : Type
  +------------+-------------------+-------+------------+
  | Resolution | Scaling Factor    | Type  | show 12345 |
  +============+===================+=======+============+
  | E6         | 1\1000000         | Micro | 0.012345   |
  +------------+-------------------+-------+------------+

  Visibility: public export
DeciMicro : Type
  +------------+-------------------+-----------+------------+
  | Resolution | Scaling Factor    | Type      | show 12345 |
  +============+===================+===========+============+
  | E7         | 1\10000000        | DeciMicro | 0.0012345  |
  +------------+-------------------+-----------+------------+

  Visibility: public export
CentiMicro : Type
  +------------+--------------------+------------+------------+
  | Resolution | Scaling Factor     | Type       | show 12345 |
  +============+====================+============+============+
  | E8         | 1\100000000        | CentiMicro | 0.00012345 |
  +------------+--------------------+------------+------------+

  Visibility: public export
Nano : Type
  +------------+------------------+------+-------------+
  | Resolution | Scaling Factor   | Type | show 12345  |
  +============+==================+======+=============+
  | E9         | 1\1000000000     | Nano | 0.000012345 |
  +------------+------------------+------+-------------+

  Visibility: public export
DeciNano : Type
  +------------+-----------------+----------+--------------+
  | Resolution | Scaling Factor  | Type     | show 12345   |
  +============+=================+==========+==============+
  | E10        | 1\10000000000   | DeciNano | 0.0000012345 |
  +------------+-----------------+----------+--------------+

  Visibility: public export
CentiNano : Type
  +------------+-----------------+-----------+---------------+
  | Resolution | Scaling Factor  | Type      | show 12345    |
  +============+=================+===========+===============+
  | E11        | 1\100000000000  | CentiNano | 0.00000012345 |
  +------------+-----------------+-----------+---------------+

  Visibility: public export
Pico : Type
  +------------+-----------------+------+----------------+
  | Resolution | Scaling Factor  | Type | show 12345     |
  +============+=================+======+================+
  | E12        | 1\1000000000000 | Pico | 0.000000012345 |
  +------------+-----------------+------+----------------+

  Visibility: public export
withResolution : (Integer -> b) -> b
  Run a computation with the resolution available as an `Integer`.

  Visibility: export