inductive Std.Time.Year.Era : Type

Defines the different eras.

• bce : Era

  The era before the Common Era (BCE), always represents a date before year 0.

• ce : Era

  The Common Era (CE), represents dates from year 0 onwards.

instance Std.Time.Year.instReprEra : Repr Era

instance Std.Time.Year.instInhabitedEra : Inhabited Era

instance Std.Time.Year.instToStringEra : ToString Era

def Std.Time.Year.Offset : Type

Offset represents a year offset, defined as an Int.

instance Std.Time.Year.instOffsetRepr : Repr Offset

instance Std.Time.Year.instOffsetDecidableEq : DecidableEq Offset

instance Std.Time.Year.instOffsetInhabited : Inhabited Offset

instance Std.Time.Year.instOffsetAdd : Add Offset

instance Std.Time.Year.instOffsetSub : Sub Offset

instance Std.Time.Year.instOffsetNeg : Neg Offset

instance Std.Time.Year.instOffsetLE : LE Offset

instance Std.Time.Year.instOffsetLT : LT Offset

instance Std.Time.Year.instOffsetToString : ToString Offset

instance Std.Time.Year.instDecidableLeOffset {x y : Offset} : Decidable (x ≤ y)

instance Std.Time.Year.instDecidableLtOffset {x y : Offset} : Decidable (x < y)

instance Std.Time.Year.instOfNatOffset {n : Nat} : OfNat Offset n

instance Std.Time.Year.instOrdOffset : Ord Offset

instance Std.Time.Year.instTransOrdOffset : TransOrd Offset

instance Std.Time.Year.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

def Std.Time.Year.Offset.ofNat (data : Nat) : Offset

Creates an Offset from a natural number.

@[inline]

def Std.Time.Year.Offset.ofInt (data : Int) : Offset

Creates an Offset from an integer.

@[inline]

def Std.Time.Year.Offset.toInt (offset : Offset) : Int

Converts the Year offset to an Int.

@[inline]

def Std.Time.Year.Offset.toMonths (val : Offset) : Month.Offset

Converts the Year offset to a Month offset.

@[inline]

def Std.Time.Year.Offset.isLeap (y : Offset) : Bool

Determines if a year is a leap year in the proleptic Gregorian calendar.

def Std.Time.Year.Offset.era (year : Offset) : Era

Returns the Era of the Year.

def Std.Time.Year.Offset.days (year : Offset) : Internal.Bounded.LE 365 366

Calculates the number of days in the specified year.

def Std.Time.Year.Offset.weeks (year : Offset) : Internal.Bounded.LE 52 53

Calculates the number of weeks in the specified year.

@[reducible, inline]

abbrev Std.Time.Year.Offset.Valid (year : Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Prop

Checks if the given date is valid for the specified year, month, and day.