toki/idris2-ratio
1
0
Fork 0
Code Issues Pull requests Activity

Add unsafe ratio constructor

Browse source
This commit is contained in:
Kiana Sheibani 2023-08-06 22:10:47 -04:00
parent 2e6f56dfde
commit fdbc5b9d69
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Data/Ratio.idr
View file

@ -40,6 +40,14 @@ export
mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a) mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a)
mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d) mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d)
||| Create a ratio of two values.
||| WARNING: This is only safe if the denominator is not zero!
export %unsafe
unsafeMkRatio : (n, d : a) -> Ratio a
unsafeMkRatio = MkRatio
infix 9 // infix 9 //
||| Construct a ratio of two values. ||| Construct a ratio of two values.