source
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.

Instances For

source
instance Std.Time.Year.instReprEra :
Repr Era
Equations

- Std.Time.Year.instReprEra = { reprPrec := Std.Time.Year.instReprEra.repr }

source
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✝

Instances For

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

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

Instances For

source
instance Std.Time.Year.instInhabitedEra :
Inhabited Era
Equations

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

source
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" }

source
def Std.Time.Year.Offset :
Type

`Offset` represents a year offset, defined as an `Int`.

Equations

- Std.Time.Year.Offset = Int

Instances For

source
instance Std.Time.Year.instReprOffset :
Repr Offset
Equations

- Std.Time.Year.instReprOffset = instReprInt

source
instance Std.Time.Year.instDecidableEqOffset :
DecidableEq Offset
Equations

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

source
instance Std.Time.Year.instInhabitedOffset :
Inhabited Offset
Equations

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

source
instance Std.Time.Year.instAddOffset :
Add Offset
Equations

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

source
instance Std.Time.Year.instSubOffset :
Sub Offset
Equations

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

source
instance Std.Time.Year.instNegOffset :
Neg Offset
Equations

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

source
instance Std.Time.Year.instLEOffset :
LE Offset
Equations

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

source
instance Std.Time.Year.instLTOffset :
LT Offset
Equations

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

source
instance Std.Time.Year.instToStringOffset :
ToString Offset
Equations

- Std.Time.Year.instToStringOffset = instToStringInt

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

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

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

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

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

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

source
instance Std.Time.Year.instOrdOffset :
Ord Offset
Equations

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

source
instance Std.Time.Year.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.Year.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
@[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

Instances For

source
@[inline]
def Std.Time.Year.Offset.ofInt (data : Int) :
Offset

Creates an `Offset` from an integer.

Equations

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

Instances For

source
@[inline]
def Std.Time.Year.Offset.toInt (offset : Offset) :
Int

Converts the `Year` offset to an `Int`.

Equations

- offset.toInt = offset

Instances For

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

Instances For

source
@[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))

Instances For

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[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)

Instances For