From 5b7a8fd07aa65216f08989848dc46a0199af54bb Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 7 Nov 2024 11:19:27 -0300 Subject: [PATCH] Update src/Std/Time.lean Co-authored-by: Markus Himmel --- src/Std/Time.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time.lean b/src/Std/Time.lean index f85d37cef44b..96e67b4f4891 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -83,7 +83,7 @@ nanoseconds corresponds to one second. # Date and Time Types -Dates and times are made up of different parts. an `Ordinal` is an absolute value, like a specific day in a month, +Dates and times are made up of different parts. An `Ordinal` is an absolute value, like a specific day in a month, while an `Offset` is a shift forward or backward in time, used in arithmetic operations to add or subtract days, months or years. Dates use components like `Year.Ordinal`, `Month.Ordinal`, and `Day.Ordinal` to ensure they represent valid points in time.