Lean: Add parsing for duration in the datetime extension

[adpaco-aws]

Issue #, if available: N/A

Description of changes

This PR adds parsing for duration strings in the datetime extension which is being introduced to the Lean models.

We define a parse function that attempts to parse a duration string from the back. This helps us avoid an issue with respect to our previous forward version where this greedy approach leads to failures due to the m unit being a substring of the ms unit. The changes also include unit tests for parsing duration strings.

Callouts

• This is my first contribution in Lean so I'm open to all kinds of feedback.
• It's likely that I'll later add a parse function for datetime values, so I'm not sure what's the best way to name the parse in these changes. Do we want another namespace for the duration definitions?

[emina]

Thanks for the PR!

Left some comments.