
  0 | module Text.CSS.Percentage
  1 | 
  2 | import Data.Refined
  3 | import Derive.Prelude
  4 | import Derive.Refined
  5 | 
  6 | %language ElabReflection
  7 | %default total
  8 | 
  9 | public export
 10 | IsPercentage : Double -> Bool
 11 | IsPercentage x = 0 <= x && x <= 100
 12 | 
 13 | ||| A floating point percentage value in the the
 14 | ||| range [0,100].
 15 | public export
 16 | record Percentage where
 17 |   constructor MkPercentage
 18 |   value : Double
 19 |   {auto 0 prf : Holds IsPercentage value}
 20 | 
 21 | %runElab derive "Percentage" [Show,Eq,Ord,RefinedDouble]
 22 | 
 23 | export
 24 | Interpolation Percentage where
 25 |   interpolate (MkPercentage v) = show v ++ "%"
 26 | 
 27 | ||| Convenience function for creating percentages with little
 28 | ||| syntactic overhead.
 29 | |||
 30 | ||| ```idris example
 31 | ||| perc 12
 32 | ||| ```
 33 | export %inline
 34 | perc :
 35 |      {auto _ : Cast Percentage a}
 36 |   -> (v : Double)
 37 |   -> {auto 0 prf : Holds IsPercentage v}
 38 |   -> a
 39 | perc v = cast $ MkPercentage v
 40 |