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

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

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 Lake.Date

instance Lake.instDecidableEqDate : DecidableEq Lake.Date

instance Lake.instOrdDate : Ord Lake.Date

Equations

• Lake.instOrdDate = { compare := Lake.ordDate✝ }

instance Lake.instReprDate : Repr Lake.Date

Equations

• Lake.instReprDate = { reprPrec := Lake.reprDate✝ }

instance Lake.Date.instLT : LT Lake.Date

instance Lake.Date.instLE : LE Lake.Date

Equations

• Lake.Date.instLE = leOfOrd

instance Lake.Date.instMin : Min Lake.Date

instance Lake.Date.instMax : Max Lake.Date

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

@[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 Lake.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 Lake.Date

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

Equations

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

instance Lake.Date.instToString : ToString Lake.Date