Idris2Doc : Text.WebIDL.Types.Numbers

Text.WebIDL.Types.Numbers

(source)
Definitions
data IntLit : Type
  An integer literal in hexadecimal, octal, or decimal representation.
  The code generator will use the same representation when
  generating code for constants and default values.

  Totality: total
  Visibility: public export
  Constructors:
  
Hex : Nat -> IntLit
  
Oct : Nat -> IntLit
  
I : Integer -> IntLit

  Hints:
  
Eq IntLit
  
HasAttributes IntLit
  
Interpolation IntLit
  
Show IntLit
data Signum : Type
  The sign of a floating point literal.

  Totality: total
  Visibility: public export
  Constructors:
  
Plus : Signum
  
Minus : Signum

  Hints:
  
Eq Signum
  
Show Signum
data FloatLit : Type
  A parsed floating point literal.
  
  A floating point literal is either one of three
  special values (`NaN`, `Infinity`, or `-Infinity`)
  or a decimal floating point number (`NoExp`: dot is
  mandatory), or a float in scientific notation (`Exp`:
  dot is optional).
  
  The main focus of this data type is one of
  preserving information. Encoding a `FloatLit` should
  yield (almost) exactly the same literal as the one
  encountered during parsin with two minor exceptions:
  a) The encoded literal will always use a lowercase 'e' as
  the delimiter for the exponent and b) in case of a
  positive exponent, there will not be a '+' in the
  encoded literal.

  Totality: total
  Visibility: public export
  Constructors:
  
Exp : Integer -> Maybe Nat -> Integer -> FloatLit
  Floating point number in scientific notation.
  
  Example: `-12.10e10`
  
NoExp : Integer -> Nat -> FloatLit
  Floating point number without exponent.
  
  Example: `-12.1002`
  
Infinity : FloatLit
  Corresponds to the WebIDL keyword `Infinity`
  
NegativeInfinity : FloatLit
  Corresponds to the WebIDL keyword `-Infinity`
  
NaN : FloatLit
  Corresponds to the WebIDL keyword `NaN`

  Hints:
  
Eq FloatLit
  
HasAttributes FloatLit
  
Interpolation FloatLit
  
Show FloatLit