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

Equations

• Std.Time.Year.instReprEra = { reprPrec := Std.Time.Year.reprEra✝ }

instance Std.Time.Year.instInhabitedEra : Inhabited Era

Equations

• Std.Time.Year.instInhabitedEra = { default := Std.Time.Year.Era.bce }

instance Std.Time.Year.instToStringEra : ToString Era

Equations

• Std.Time.Year.instToStringEra = { toString := fun (x : Std.Time.Year.Era) => match x with | Std.Time.Year.Era.bce => "BCE" | Std.Time.Year.Era.ce => "CE" }

def Std.Time.Year.Offset : Type

Offset represents a year offset, defined as an Int.

Equations

• Std.Time.Year.Offset = Int

instance Std.Time.Year.instOffsetRepr : Repr Offset

Equations

• Std.Time.Year.instOffsetRepr = instReprInt

instance Std.Time.Year.instOffsetBEq : BEq Offset

Equations

• Std.Time.Year.instOffsetBEq = instBEqOfDecidableEq

instance Std.Time.Year.instOffsetInhabited : Inhabited Offset

Equations

• Std.Time.Year.instOffsetInhabited = Int.instInhabited

instance Std.Time.Year.instOffsetAdd : Add Offset

Equations

• Std.Time.Year.instOffsetAdd = Int.instAdd

instance Std.Time.Year.instOffsetSub : Sub Offset

Equations

• Std.Time.Year.instOffsetSub = Int.instSub

instance Std.Time.Year.instOffsetNeg : Neg Offset

Equations

• Std.Time.Year.instOffsetNeg = Int.instNegInt

instance Std.Time.Year.instOffsetLE : LE Offset

Equations

• Std.Time.Year.instOffsetLE = Int.instLEInt

instance Std.Time.Year.instOffsetLT : LT Offset

Equations

• Std.Time.Year.instOffsetLT = Int.instLTInt

instance Std.Time.Year.instOffsetToString : ToString Offset

Equations

• Std.Time.Year.instOffsetToString = instToStringInt

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

Equations

• Std.Time.Year.instDecidableLeOffset = inferInstanceAs (Decidable (x ≤ y))

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

Equations

• Std.Time.Year.instDecidableLtOffset = inferInstanceAs (Decidable (x < y))

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

Equations

• Std.Time.Year.instOfNatOffset = { ofNat := Int.ofNat n }

@[inline]

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

Creates an Offset from a natural number.

Equations

• Std.Time.Year.Offset.ofNat data = Int.ofNat data

@[inline]

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

Creates an Offset from an integer.

Equations

• Std.Time.Year.Offset.ofInt data = data

@[inline]

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

Converts the Year offset to an Int.

Equations

• offset.toInt = offset

@[inline]

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

Converts the Year offset to a Month offset.

Equations

• val.toMonths = Int.mul val 12

@[inline]

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

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

Equations

• y.isLeap = decide (y.toInt.tmod 4 = 0 ∧ (y.toInt.tmod 100 ≠ 0 ∨ y.toInt.tmod 400 = 0))

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

Returns the Era of the Year.

Equations

• year.era = if year.toInt ≥ 1 then Std.Time.Year.Era.ce else Std.Time.Year.Era.bce

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

Calculates the number of days in the specified year.

Equations

• One or more equations did not get rendered due to their size.

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

Calculates the number of weeks in the specified year.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• year.Valid month day = (day ≤ Std.Time.Month.Ordinal.days year.isLeap month)