import Std.Time
open Std.Time

def date := date("1970-01-20")

/--
info: date("1970-02-01")
-/
#guard_msgs in
#eval date + (12 : Day.Offset)

/--
info: date("1970-01-08")
-/
#guard_msgs in
#eval date - (12 : Day.Offset)

def datetime := datetime("2000-01-20T03:02:01")

/--
info: datetime("2000-01-20T04:02:01.000000000")
-/
#guard_msgs in
#eval datetime + (1 : Hour.Offset)

/--
info: datetime("2000-01-20T02:02:01.000000000")
-/
#guard_msgs in
#eval datetime - (1 : Hour.Offset)

/--
info: datetime("2000-01-20T03:12:01.000000000")
-/
#guard_msgs in
#eval datetime + (10 : Minute.Offset)

/--
info: datetime("2000-01-20T02:52:01.000000000")
-/
#guard_msgs in
#eval datetime - (10 : Minute.Offset)

/--
info: datetime("2000-01-20T03:03:01.000000000")
-/
#guard_msgs in
#eval datetime + (60 : Second.Offset)

/--
info: datetime("2000-01-20T03:01:01.000000000")
-/
#guard_msgs in
#eval datetime - (60 : Second.Offset)

/--
info: datetime("2000-01-21T03:02:01.000000000")
-/
#guard_msgs in
#eval datetime + (1 : Day.Offset)

/--
info: datetime("2000-01-19T03:02:01.000000000")
-/
#guard_msgs in
#eval datetime - (1 : Day.Offset)

def time := time("13:02:01")

/--
info: time("14:02:01.000000000")
-/
#guard_msgs in
#eval time + (1 : Hour.Offset)

/--
info: time("12:02:01.000000000")
-/
#guard_msgs in
#eval time - (1 : Hour.Offset)

/--
info: time("13:12:01.000000000")
-/
#guard_msgs in
#eval time + (10 : Minute.Offset)

/--
info: time("12:52:01.000000000")
-/
#guard_msgs in
#eval time - (10 : Minute.Offset)

/--
info: time("13:03:01.000000000")
-/
#guard_msgs in
#eval time + (60 : Second.Offset)

/--
info: time("13:01:01.000000000")
-/
#guard_msgs in
#eval time - (60 : Second.Offset)

def datetimetz := zoned("2000-01-20T06:02:01-03:00")

/--
info: zoned("2000-01-20T06:02:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz

/--
info: zoned("2000-01-22T06:02:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz + (2 : Day.Offset)

/--
info: zoned("2000-01-19T06:02:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz - (1 : Day.Offset)

/--
info: zoned("2000-01-20T07:02:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz + (1 : Hour.Offset)

/--
info: zoned("2000-01-20T05:02:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz - (1 : Hour.Offset)

/--
info: zoned("2000-01-20T06:12:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz + (10 : Minute.Offset)

/--
info: zoned("2000-01-20T05:52:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz - (10 : Minute.Offset)

/--
info: zoned("2000-01-20T06:03:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz + (60 : Second.Offset)

/--
info: zoned("2000-01-20T06:01:01.000000000-03:00")
-/
#guard_msgs in
#eval datetimetz - (60 : Second.Offset)

/--
info: "3600s"
-/
#guard_msgs in
#eval zoned("2000-12-20T00:00:00-03:00") - zoned("2000-12-20T00:00:00-02:00")

def now := PlainDateTime.ofWallTime (WallTime.ofDuration ⟨1724859638, ⟨907328169, by decide⟩, by decide⟩)
def after := PlainDateTime.ofWallTime (WallTime.ofDuration ⟨1724859639, ⟨907641224, by decide⟩, by decide⟩)
def duration := after - now

/--
info: "15:40:38.907328169"
-/
#guard_msgs in
#eval now.format "HH:mm:ss.SSSSSSSSS"

/--
info: "15.40:39.907641224"
-/
#guard_msgs in
#eval after.format "HH.mm:ss.SSSSSSSSS"

/--
info: "1.000313055s"
-/
#guard_msgs in
#eval duration