diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index dd6fc91cc785..b97ca53c3f14 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -29,10 +29,8 @@ structure PlainDateTime where The `Time` component of a `PlainTime` -/ time : PlainTime - deriving Inhabited, BEq, Repr - namespace PlainDateTime /-- diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean index ad2521a85ab3..4863a638729a 100644 --- a/tests/lean/run/timeLocalDateTime.lean +++ b/tests/lean/run/timeLocalDateTime.lean @@ -6,7 +6,6 @@ def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss") def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu") def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second - def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year def date₁ := datetime("1993-11-19T09:08:07")