Std.Time.Date.Unit.Year

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

@[implicit_reducible]

instance Std.Time.Year.instReprEra :

Repr Era

source

def Std.Time.Year.instReprEra.repr :

Era → Nat → Std.Format

Instances For

source

def Std.Time.Year.instInhabitedEra.default :

Era

Instances For

source

@[implicit_reducible]

instance Std.Time.Year.instInhabitedEra :

Inhabited Era

source

@[implicit_reducible]

instance Std.Time.Year.instToStringEra :

ToString Era

source

def Std.Time.Year.Offset :

Type

Offset represents a year offset, defined as an Int.

Instances For

source

@[implicit_reducible]

instance Std.Time.Year.instReprOffset :

Repr Offset

source

@[implicit_reducible]

instance Std.Time.Year.instDecidableEqOffset :

DecidableEq Offset

source

@[implicit_reducible]

instance Std.Time.Year.instInhabitedOffset :

Inhabited Offset

source

@[implicit_reducible]

instance Std.Time.Year.instAddOffset :

Add Offset

source

@[implicit_reducible]

instance Std.Time.Year.instSubOffset :

Sub Offset

source

@[implicit_reducible]

instance Std.Time.Year.instNegOffset :

Neg Offset

source

@[implicit_reducible]

instance Std.Time.Year.instLEOffset :

LE Offset

source

@[implicit_reducible]

instance Std.Time.Year.instLTOffset :

LT Offset

source

@[implicit_reducible]

instance Std.Time.Year.instToStringOffset :

ToString Offset

source

@[implicit_reducible]

instance Std.Time.Year.instDecidableLeOffset {x y : Offset} :

Decidable (x ≤ y)

source

@[implicit_reducible]

instance Std.Time.Year.instDecidableLtOffset {x y : Offset} :

Decidable (x < y)

source

@[implicit_reducible]

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

OfNat Offset n

source

@[implicit_reducible]

instance Std.Time.Year.instOrdOffset :

Ord Offset

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.

Instances For

source

@[inline]

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

Offset

Creates an Offset from an integer.

Instances For

source

@[inline]

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

Int

Converts the Year offset to an Int.

Instances For

source

@[inline]

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

Month.Offset

Converts the Year offset to a Month offset.

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.

Instances For

source

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

Era

Returns the Era of the Year.

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.

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.

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.

Instances For