Equations
Equations
- Std.Time.Day.instInhabitedOrdinal = { default := 1 }
Equations
- Std.Time.Day.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }
OfYear
represents the day ordinal within a year, which can be bounded between 1 and 365 or 366,
depending on whether it's a leap year.
Equations
Instances For
Equations
- Std.Time.Day.Ordinal.instReprOfYear = { reprPrec := fun (r : Std.Time.Day.Ordinal.OfYear leap) (p : Nat) => reprPrec r.val p }
Equations
- Std.Time.Day.Ordinal.instToStringOfYear = { toString := fun (r : Std.Time.Day.Ordinal.OfYear leap) => toString r.val }
@[inline]
def
Std.Time.Day.Ordinal.OfYear.ofNat
{leap : Bool}
(data : Nat)
(h : data ≥ 1 ∧ data ≤ if leap = true then 366 else 365 := by decide)
:
OfYear leap
Creates an ordinal for a specific day within the year, ensuring that the provided day (data
)
is within the valid range for the year, which can be 1 to 365 or 366 for leap years.
Instances For
Equations
Equations
- Std.Time.Day.Ordinal.instInhabitedOfYear = { default := ⟨1, ⋯⟩ }
@[inline]
Creates an ordinal from a natural number, ensuring the number is within the valid range for days of a month (1 to 31).