Skip to content

Commit

Permalink
Revert "USe do notation for durationUnits?"
Browse files Browse the repository at this point in the history
This reverts commit 0f3ac7c.
  • Loading branch information
adpaco-aws committed Feb 28, 2025
1 parent 39cd454 commit ae7b3cc
Showing 1 changed file with 11 additions and 9 deletions.
20 changes: 11 additions & 9 deletions cedar-lean/Cedar/Spec/Ext/Datetime.lean
Original file line number Diff line number Diff line change
Expand Up @@ -160,15 +160,17 @@ def duration? (i: Int) : Option Duration :=
def Duration.neg? (d : Duration) : Option Duration :=
d.val.neg?

def durationUnits? (n: Nat) (suffix: String) : Option Int := do
let i ← Int64.ofInt? n
match suffix with
| "ms" => some i
| "s" => some (i * MILLISECONDS_PER_SECOND)
| "m" => some (i * MILLISECONDS_PER_MINUTE)
| "h" => some (i * MILLISECONDS_PER_HOUR)
| "d" => some (i * MILLISECONDS_PER_DAY)
| _ => none
def durationUnits? (n: Nat) (suffix: String) : Option Int :=
match Int64.ofInt? n with
| none => none
| some i =>
match suffix with
| "ms" => some i
| "s" => some (i * MILLISECONDS_PER_SECOND)
| "m" => some (i * MILLISECONDS_PER_MINUTE)
| "h" => some (i * MILLISECONDS_PER_HOUR)
| "d" => some (i * MILLISECONDS_PER_DAY)
| _ => none

def unitsToMilliseconds (days hours minutes second milliseconds: Int) : Int :=
days * MILLISECONDS_PER_DAY +
Expand Down

0 comments on commit ae7b3cc

Please sign in to comment.