Text.CSS.Percentage

Reexports

Definitions

IsPercentage : Double -> Bool

Totality: total
Visibility: public export

record Percentage : Type

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

Totality: total
Visibility: public export
Constructor: 

MkPercentage : (value : Double) -> {auto 0 _ : Holds IsPercentage value} -> Percentage

Projections:

0 .prf : ({rec:0} : Percentage) -> Holds IsPercentage (value {rec:0})

.value : Percentage -> Double

Hints:

Cast Percentage LengthOrPercentage

Cast Percentage a => Cast Percentage (Dir a)

Cast Percentage MinMaxValue

Cast Percentage GridValue

Cast Percentage FlexBasis

Cast Percentage FontSize

Cast Percentage BorderRadius

Cast Percentage LineHeight

Cast Percentage Width

DoubleLit Percentage

Eq Percentage

IntegerLit Percentage

Interpolation Percentage

Ord Percentage

Show Percentage

.value : Percentage -> Double

Totality: total
Visibility: public export

value : Percentage -> Double

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Percentage) -> Holds IsPercentage (value {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : Percentage) -> Holds IsPercentage (value {rec:0})

Totality: total
Visibility: public export

perc : Cast Percentage a => (v : Double) -> {auto 0 _ : Holds IsPercentage v} -> a

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

Totality: total
Visibility: export

.perc : Cast Percentage a => (v : Double) -> {auto 0 _ : Holds IsPercentage v} -> a

Totality: total
Visibility: export