Text.CSS.Percentage

Reexports

Definitions

record Percentage : Type

  A floating point percentage value in the the
  range [0,100].

Totality: total
Visibility: public export
Constructor: 

MkPercentage : (value : Double) -> (0 _ : So ((0.0 <= value) && Delay (value <= 100))) -> Percentage

Projections:

0 .prf : ({rec:0} : Percentage) -> So ((0.0 <= value {rec:0}) && Delay (value {rec:0} <= 100))

.value : Percentage -> Double

Hints:

Cast Percentage a => Cast Percentage (Dir a)

Cast Percentage MinMaxValue

Cast Percentage GridValue

Cast Percentage FlexBasis

Cast Percentage FontSize

Cast Percentage BorderRadius

Cast Percentage Width

Eq Percentage

Ord Percentage

Render Percentage

Show Percentage

.value : Percentage -> Double

Totality: total
Visibility: public export

value : Percentage -> Double

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Percentage) -> So ((0.0 <= value {rec:0}) && Delay (value {rec:0} <= 100))

Totality: total
Visibility: public export

0 prf : ({rec:0} : Percentage) -> So ((0.0 <= value {rec:0}) && Delay (value {rec:0} <= 100))

Totality: total
Visibility: public export

fromInteger : (n : Integer) -> {auto 0 _ : IsJust (refine (cast n))} -> Percentage

Totality: total
Visibility: export

perc : Cast Percentage a => (v : Double) -> {auto 0 _ : So ((0.0 <= v) && Delay (v <= 100))} -> a

  Convenience function for creating percentages with little
  syntactic overhead.
  
  ```idris example
  perc 12
  ```

Totality: total
Visibility: export