Date

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

structure Lake.Date : Type

A date (year-month-day).

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

def Lake.instInhabitedDate.default : Date

instance Lake.instInhabitedDate : Inhabited Date

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

instance Lake.instDecidableEqDate : DecidableEq Date

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

instance Lake.instOrdDate : Ord Date

instance Lake.instReprDate : Repr Date

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

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