Documentation

Time

Imports

Init
Time.Fixed
Time.Format
Time.Specifier
Time.ZeroPad
Time.Calendar.CalendarDiffDays
Time.Calendar.Clip
Time.Calendar.Days
Time.Calendar.Gregorian
Time.Calendar.MonthDay
Time.Calendar.OrdinalDate
Time.Calendar.Week
Time.Calendar.WeekDate
Time.Clock.DiffTime
Time.Clock.SystemTime
Time.Clock.UTCTime
Time.Format.Locale
Time.Format.Parse
Time.LocalTime.LocalTime
Time.LocalTime.TimeOfDay
Time.LocalTime.TimeZone
Time.LocalTime.ZonedTime
Time.Format.Parse.Class
Time.Format.Parse.Instances

Imported by

Time library #

Time, clocks and calendars. Port of the haskell time library to Lean 4.

Usage #

see time library doc