Geom.Scale

Definitions

ValidScale : Double -> Bool

  Scaling factor in the range [1.0e-6,1.0e6].

Totality: total
Visibility: public export

record Scale : Type

  A scaling factor

Totality: total
Visibility: public export
Constructor: 

S : (value : Double) -> {auto 0 _ : Holds ValidScale value} -> Scale

Projections:

0 .prf : ({rec:0} : Scale) -> Holds ValidScale (value {rec:0})

.value : Scale -> Double

Hints:

Eq Scale

Ord Scale

Show Scale

.value : Scale -> Double

Totality: total
Visibility: public export

value : Scale -> Double

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Scale) -> Holds ValidScale (value {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : Scale) -> Holds ValidScale (value {rec:0})

Totality: total
Visibility: public export

scale : Double -> Scale

  Safely convert a floating point number to a `Scale`

Totality: total
Visibility: export

inverse : Scale -> Scale

  Invert the scaling factor so that `x * inverse x == 1`
  (modulo rounding errors).

Totality: total
Visibility: export

(*) : Scale -> Scale -> Scale

  Multiply two scaling factors.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 9

(/) : Scale -> Scale -> Scale

  Divide a scaling factor by another one

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 9