============================================================================================== # Digit strings (Digit⁺) and their correspondence with toNat?'

`IsDigits` is the grammar-level notion of a non-empty run of digit characters — the
`Digit⁺` production common to numeric grammars. These lemmas connect it to the stdlib
natural-number parser `toNat?'`: a digit string is exactly one `toNat?'` accepts (modulo the
`'_'` separator, which `toNat?'` rejects and `Char.isDigit` never admits). The `IsDigits.*`
projections at the end give dot-notation for the facts parser proofs consume.
============================================================================================== 

def String.IsDigits (s : String) : Prop

Digit⁺: a non-empty string all of whose characters are decimal digits.

Equations

• s.IsDigits = (0 < s.length ∧ ∀ (c : Char), c ∈ s.toList → c.isDigit = true)

def String.IsFixedDigits (n : Nat) (s : String) : Prop

Digit{n}: a run of exactly n decimal digits. The fixed-width refinement of IsDigits, used wherever a grammar pins a field's width (the datetime grammar's YYYY, MM, SSS, …).

Equations

• String.IsFixedDigits n s = (s.IsDigits ∧ s.length = n)

def String.IsAtMostNDigits (n : Nat) (s : String) : Prop

Digit{1,n}: between one and n decimal digits. IsDigits supplies the lower bound and the length constraint the upper (the decimal grammar's Fraction ::= Digit{1,4}).

Equations

• String.IsAtMostNDigits n s = (s.IsDigits ∧ s.length ≤ n)

def String.IsWfSign (s : String) : Prop

['-']: an optional leading minus sign, either present or absent. Shared by the numeric grammars that admit a signed literal (decimal's Sign, duration's leading '-').

Equations

• s.IsWfSign = (s = "-" ∨ s = "")

def String.natOf (s : String) : Nat

Natural-number value of a captured decimal digit string, defaulting to 0 when parsing fails. On a field satisfying IsDigits, the default is never taken.

Equations

• s.natOf = (Cedar.Spec.Ext.toNat?' s).getD 0

def String.lenOf (s : String) : Int

Length of a captured string as an integer, for use in grammar value formulas.

Equations

• s.lenOf = ↑s.length

def String.signOf (s : String) : Int

Sign denoted by a captured optional-minus field.

Equations

• s.signOf = if s.startsWith "-" = true then -1 else 1

theorem String.toNat?'_toString (n : Nat) : Cedar.Spec.Ext.toNat?' (toString n) = some n

Rendering a natural number and parsing it with Cedar's underscore-rejecting parser recovers the original number.

theorem String.toNat?'_repr (n : Nat) : Cedar.Spec.Ext.toNat?' n.repr = some n

Nat.repr is accepted by Cedar's natural-number parser.

theorem String.isDigits_toString (n : Nat) : (toString n).IsDigits

The canonical decimal rendering of a natural number is a nonempty digit string.

theorem String.isDigits_repr (n : Nat) : n.repr.IsDigits

Nat.repr is a nonempty digit string.

============================================================================================== # Splitting a string on a separator ==============================================================================================

============================================================================================== # toString/repr of naturals contains no '.' ==============================================================================================

============================================================================================== # Digit-accumulating folds and Nat.toDigits roundtrip ==============================================================================================