# Date #

A year-mont-day date. Used by Lake's TOML parser and its toolchain version parser (for nightlies).

source
structure Lake.Date :
Type

A date (year-month-day).

- year : Nat
- month : Nat
- day : Nat

Instances For

source
def Lake.instInhabitedDate.default :
Date
Equations

- Lake.instInhabitedDate.default = { year := default, month := default, day := default }

Instances For

source
instance Lake.instInhabitedDate :
Inhabited Date
Equations

- Lake.instInhabitedDate = { default := Lake.instInhabitedDate.default }

source
def Lake.instDecidableEqDate.decEq (x✝ x✝¹ : Date) :
Decidable (x✝ = x✝¹)
Equations

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

Instances For

source
instance Lake.instDecidableEqDate :
DecidableEq Date
Equations

- Lake.instDecidableEqDate = Lake.instDecidableEqDate.decEq

source
def Lake.instOrdDate.ord :
Date → Date → Ordering
Equations

- Lake.instOrdDate.ord { year := a, month := a_1, day := a_2 } { year := b, month := b_1, day := b_2 } = (compare a b).then ((compare a_1 b_1).then ((compare a_2 b_2).then Ordering.eq))

Instances For

source
instance Lake.instOrdDate :
Ord Date
Equations

- Lake.instOrdDate = { compare := Lake.instOrdDate.ord }

source
instance Lake.instReprDate :
Repr Date
Equations

- Lake.instReprDate = { reprPrec := Lake.instReprDate.repr }

source
def Lake.instReprDate.repr :
Date → Nat → Std.Format
Equations

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

Instances For

source
instance Lake.Date.instLT :
LT Date
Equations

- Lake.Date.instLT = ltOfOrd

source
instance Lake.Date.instLE :
LE Date
Equations

- Lake.Date.instLE = leOfOrd

source
instance Lake.Date.instMin :
Min Date
Equations

- Lake.Date.instMin = minOfLe

source
instance Lake.Date.instMax :
Max Date
Equations

- Lake.Date.instMax = maxOfLe

source
@[reducible, inline]
abbrev Lake.Date.IsLeapYear (y : Nat) :
Prop
Equations

- Lake.Date.IsLeapYear y = (y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0))

Instances For

source
@[reducible, inline]
abbrev Lake.Date.IsValidMonth (m : Nat) :
Prop
Equations

- Lake.Date.IsValidMonth m = (m ≥ 1 ∧ m ≤ 12)

Instances For

source
def Lake.Date.maxDay (y m : Nat) :
Nat
Equations

- Lake.Date.maxDay y m = if m = 2 then if Lake.Date.IsLeapYear y then 29 else 28 else if m ≤ 7 then 30 + m % 2 else 31 - m % 2

Instances For

source
@[reducible, inline]
abbrev Lake.Date.IsValidDay (y m d : Nat) :
Prop
Equations

- Lake.Date.IsValidDay y m d = (d ≥ 1 ∧ d ≤ Lake.Date.maxDay y m)

Instances For

source
def Lake.Date.ofValid? (year month day : Nat) :
Option Date
Equations

- Lake.Date.ofValid? year month day = do guard (Lake.Date.IsValidMonth month ∧ Lake.Date.IsValidDay year month day) pure { year := year, month := month, day := day }

Instances For

source
def Lake.Date.ofString? (t : String) :
Option Date
Equations

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

Instances For

source
def Lake.Date.toString (d : Date) :
String
Equations

- d.toString = toString (Lake.zpad d.year 4) ++ toString "-" ++ toString (Lake.zpad d.month 2) ++ toString "-" ++ toString (Lake.zpad d.day 2)

Instances For

source
instance Lake.Date.instToString :
ToString Date
Equations

- Lake.Date.instToString = { toString := Lake.Date.toString }