From db79d9e5ce753b98d5000b825a1bef46431f42b7 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 30 Sep 2024 10:59:01 +0200 Subject: [PATCH] doc: backticks around Lean code in docstrings (#5538) Minor docstrings tweaks on the basis of #5497 --- src/Init/Data/Float.lean | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index f8153b2f02..eb7d66df1d 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -73,33 +73,33 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b @[extern "lean_float_to_string"] opaque Float.toString : Float → String /-- If the given float is non-negative, truncates the value to the nearest non-negative integer. -If negative or NaN, returns 0. -If larger than the maximum value for UInt8 (including Inf), returns maximum value of UInt8 -(i.e. UInt8.size - 1). +If negative or NaN, returns `0`. +If larger than the maximum value for `UInt8` (including Inf), returns the maximum value of `UInt8` +(i.e. `UInt8.size - 1`). -/ @[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8 /-- If the given float is non-negative, truncates the value to the nearest non-negative integer. -If negative or NaN, returns 0. -If larger than the maximum value for UInt16 (including Inf), returns maximum value of UInt16 -(i.e. UInt16.size - 1). +If negative or NaN, returns `0`. +If larger than the maximum value for `UInt16` (including Inf), returns the maximum value of `UInt16` +(i.e. `UInt16.size - 1`). -/ @[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16 /-- If the given float is non-negative, truncates the value to the nearest non-negative integer. -If negative or NaN, returns 0. -If larger than the maximum value for UInt32 (including Inf), returns maximum value of UInt32 -(i.e. UInt32.size - 1). +If negative or NaN, returns `0`. +If larger than the maximum value for `UInt32` (including Inf), returns the maximum value of `UInt32` +(i.e. `UInt32.size - 1`). -/ @[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32 /-- If the given float is non-negative, truncates the value to the nearest non-negative integer. -If negative or NaN, returns 0. -If larger than the maximum value for UInt64 (including Inf), returns maximum value of UInt64 -(i.e. UInt64.size - 1). +If negative or NaN, returns `0`. +If larger than the maximum value for `UInt64` (including Inf), returns the maximum value of `UInt64` +(i.e. `UInt64.size - 1`). -/ @[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64 /-- If the given float is non-negative, truncates the value to the nearest non-negative integer. -If negative or NaN, returns 0. -If larger than the maximum value for USize (including Inf), returns maximum value of USize -(i.e. USize.size - 1; Note that this value is platform dependent). +If negative or NaN, returns `0`. +If larger than the maximum value for `USize` (including Inf), returns the maximum value of `USize` +(i.e. `USize.size - 1`). This value is platform dependent). -/ @[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize