============================================================================================ # Duration parser lemmas

Duration quantity tokens are the `Digit⁺` strings characterized by `IsDigits`; the
`IsDigits.ne_empty` / `IsDigits.toNat?'_isSome` / `IsDigits.all_isDigit` projections (in
`Cedar.Thm.Data.String`) recover the facts these proofs consume.
============================================================================================ 

theorem Cedar.Thm.Duration.parse_eq_duration?_of_isDurationValue {str : String} {v : Int} (h : IsDurationValue str v) : Spec.Ext.Datetime.Duration.parse str = Spec.Ext.Datetime.duration? v

On a rendering to which the grammar assigns v, Duration.parse reaches the range check with exactly v. Thus acceptance is decided by duration? alone.

theorem Cedar.Thm.Duration.isDurationValue_unique {str : String} {v₁ v₂ : Int} (h₁ : IsDurationValue str v₁) (h₂ : IsDurationValue str v₂) : v₁ = v₂

The declarative value relation is single-valued: a duration string denotes at most one integer, including when that integer lies outside the parser's Int64 range.