Lean: Definitions and theorems for duration converters

[adpaco-aws]

Description of changes: #527 missed the converter "methods" associated to the duration type, as specified in the RFC for the datetime extension:

• .toMilliseconds() returns a long describing the number of milliseconds in this duration (the value as a long, itself)
• .toSeconds() returns a long describing the number of seconds in this duration (.toMilliseconds() / 1000)
• .toMinutes() returns a long describing the number of minutes in this duration (.toSeconds() / 60)
• .toHours() returns a long describing the number of hours in this duration (.toMinutes() / 60)
• .toDays() returns a long describing the number of days in this duration (.toHours() / 24)

We include unit tests for each method in addition to a type call theorem for all of them.

The changes also include fixes for an embarrassing mistake in the MILLISECONDS_PER_HOUR definition.

[shaobo-he-aws]

I'm actually a little bit concerned about the rounding of /, particularly for negative numbers. But we have unit tests so it should be fine.

[chaluli]

I'm actually a little bit concerned about the rounding of /, particularly for negative numbers. But we have unit tests so it should be fine.

Int64.div will convert both Int64s to BitVecs then use BitVec.sdiv (signed division) which removes the signs, performs unsigned division Bitvec.udiv then restores the appropriate sign. So, Int64.div will round towards zero.

E.g., duration("25h").toDays = 1 and duration("-25h").toDays = -1.