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