interface Embed a b where
embed : a -> bLossless injection: the source type fits inside the target. Nat embeds into Int because every Nat is a valid Int.
PréludeChargé par défaut — aucun
import nécessaire.Coercion interfaces
Synopsis
interface Cast a b where
cast : a -> bPotentially lossy conversion. Int casts to Double (no precision issue for small integers).
interface TryCast a b where
tryCast : a -> Maybe bConversion that may fail, returning Maybe. A negative Int cannot become a Nat.
isFinite : Double -> BoolTrue for a Double with a genuine finite value — excludes NaN and ±Infinity. This is the representability test tryCast uses below: a finite Double is exactly the set of values truncate can turn into a faithful Int.
Convenience conversions
toInt : Nat -> IntConvert a Nat to an Int (lossless).
natToInt : Nat -> IntConvert a Nat to an Int (lossless) — toInt under the name the converse suggests (intToNat). natToInt 3 = 3.
toNat : Int -> Maybe NatTry to convert an Int to a Nat (fails if negative).
toDouble : Int -> DoubleConvert an Int to a Double.
parseInt : String -> Maybe IntParse a signed decimal integer from a string; Nothing if it is not one. The SAFE counterpart of cast : String -> Double (which is total and lossy — it returns 0.0 on garbage). parseInt "42" = Just 42, parseInt "x" = Nothing, parseInt "3.5" = Nothing.
parseDouble : String -> Maybe DoubleParse a finite double from a string; Nothing if unparseable or non-finite (inf/nan). parseDouble "3.14" = Just 3.14, parseDouble "x" = Nothing.