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

structure Lake.Date : Type

A date (year-month-day).

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

instance Lake.instInhabitedDate : Inhabited Date

instance Lake.instDecidableEqDate : DecidableEq Date

instance Lake.instOrdDate : Ord Date

instance Lake.instReprDate : Repr Date

instance Lake.Date.instLT : LT Date

instance Lake.Date.instLE : LE Date

instance Lake.Date.instMin : Min Date

instance Lake.Date.instMax : Max Date

@[reducible, inline]

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

@[reducible, inline]

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

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

@[reducible, inline]

abbrev Lake.Date.IsValidDay (y m d : Nat) : Prop

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

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

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

instance Lake.Date.instToString : ToString Date