max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: backticks around Lean code in docstrings (#5538)

Browse source 
Minor docstrings tweaks on the basis of #5497
This commit is contained in:
David Thrane Christiansen 2024-09-30 10:59:01 +02:00 • committed by GitHub
parent 5e8718dff9
commit db79d9e5ce
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/Init/Data/Float.lean
View file

@ -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