Date

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

def Lake.lpad (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.lpad s c len = "".pushn c (len - s.length) ++ s

def Lake.rpad (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.rpad s c len = s.pushn c (len - s.length)

def Lake.zpad (n len : Nat) : String

Equations

• Lake.zpad n len = Lake.lpad (toString n) '0' len

structure Lake.Date : Type

A date (year-month-day).

• year : Nat
• month : Nat
• day : Nat

instance Lake.instInhabitedDate : Inhabited Date

Equations

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

def Lake.instInhabitedDate.default : Date

Equations

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

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

Equations

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

instance Lake.instDecidableEqDate : DecidableEq Date

Equations

• Lake.instDecidableEqDate = Lake.instDecidableEqDate.decEq

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))

instance Lake.instOrdDate : Ord Date

Equations

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

instance Lake.instReprDate : Repr Date

Equations

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

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

Equations

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

instance Lake.Date.instLT : LT Date

Equations

• Lake.Date.instLT = ltOfOrd

instance Lake.Date.instLE : LE Date

Equations

• Lake.Date.instLE = leOfOrd

instance Lake.Date.instMin : Min Date

Equations

• Lake.Date.instMin = minOfLe

instance Lake.Date.instMax : Max Date

Equations

• Lake.Date.instMax = maxOfLe

@[reducible, inline]

abbrev Lake.Date.IsLeapYear (y : Nat) : Prop

Equations

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

@[reducible, inline]

abbrev Lake.Date.IsValidMonth (m : Nat) : Prop

Equations

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

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

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

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 }

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

Equations

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

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)

instance Lake.Date.instToString : ToString Date

Equations

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