From c0a5e5badb5992fc813f4abda97c9cc8e6f63cbb Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 10 Jan 2025 19:46:21 -0300 Subject: [PATCH] chore: remove useless lines --- src/Std/Time/DateTime/PlainDateTime.lean | 2 -- tests/lean/run/timeLocalDateTime.lean | 1 - 2 files changed, 3 deletions(-) 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")