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.instReprEra.repr }

def Std.Time.Year.instReprEra.repr : Era → Nat → Std.Format

Equations

• Std.Time.Year.instReprEra.repr Std.Time.Year.Era.bce prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Year.Era.bce")).group prec✝
• Std.Time.Year.instReprEra.repr Std.Time.Year.Era.ce prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Year.Era.ce")).group prec✝

def Std.Time.Year.instInhabitedEra.default : Era

Equations

• Std.Time.Year.instInhabitedEra.default = Std.Time.Year.Era.bce

instance Std.Time.Year.instInhabitedEra : Inhabited Era

Equations

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

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.instReprOffset : Repr Offset

Equations

• Std.Time.Year.instReprOffset = instReprInt

instance Std.Time.Year.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.Year.instDecidableEqOffset = Int.instDecidableEq

instance Std.Time.Year.instInhabitedOffset : Inhabited Offset

Equations

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

instance Std.Time.Year.instAddOffset : Add Offset

Equations

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

instance Std.Time.Year.instSubOffset : Sub Offset

Equations

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

instance Std.Time.Year.instNegOffset : Neg Offset

Equations

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

instance Std.Time.Year.instLEOffset : LE Offset

Equations

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

instance Std.Time.Year.instLTOffset : LT Offset

Equations

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

instance Std.Time.Year.instToStringOffset : ToString Offset

Equations

• Std.Time.Year.instToStringOffset = 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 }

instance Std.Time.Year.instOrdOffset : Ord Offset

Equations

• Std.Time.Year.instOrdOffset = inferInstanceAs (Ord Int)

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.

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)