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

Equations

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

instance Lake.instDecidableEqDate : DecidableEq Lake.Date

Equations

• Lake.instDecidableEqDate = Lake.decEqDate✝

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

Equations

• Lake.Date.instLT = ltOfOrd

instance Lake.Date.instLE : LE Lake.Date

Equations

• Lake.Date.instLE = leOfOrd

instance Lake.Date.instMin : Min Lake.Date

Equations

• Lake.Date.instMin = minOfLe

instance Lake.Date.instMax : Max Lake.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 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

Equations

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

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

Equations

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