Decimal grammar: definitions

This file contains only the grammar-level definitions — the well-formedness predicates and the value relation — as a direct, parser-independent transcription of the decimal grammar. DecimalProduction relates a rendering to its grammar fields, IsWfDecimal existentially hides those fields, value gives their denotation, and IsDecimalValue s v adds that denotation to the same production witness. The lemmas connecting these definitions to Decimal.parse (in particular the digit-string ↔ toInt?'/toNat?' bridges) live in Cedar.Thm.Ext.Decimal.Lemmas.

Sign ::= ['-'] uses the shared IsWfSign predicate. The decimal-specific Natural and Fraction productions are named locally using the shared digit predicates IsDigits and IsAtMostNDigits. Their value readers (natOf, signOf, and lenOf) and string-to-number bridges live in Cedar.Thm.Data.String.

@[reducible, inline]

abbrev Cedar.Thm.Decimal.IsNatural (s : String) : Prop

The grammar's Natural ::= Digit⁺: the unsigned natural-number production. An abbrev for the shared IsDigits predicate, so every IsDigits lemma applies without unfolding.

Equations

• Cedar.Thm.Decimal.IsNatural s = s.IsDigits

def Cedar.Thm.Decimal.IsWfFrac (s : String) : Prop

The grammar's Fraction ::= Digit{1,4}: 1 to DECIMAL_DIGITS digits, an instance of the shared bounded-digits predicate.

Equations

• Cedar.Thm.Decimal.IsWfFrac s = String.IsAtMostNDigits Cedar.Spec.Ext.DECIMAL_DIGITS s

def Cedar.Thm.Decimal.DecimalProduction (s sign natural fraction : String) : Prop

A decimal grammar production: s is the rendering of well-formed Sign, Natural, and Fraction fields, concatenated around the literal decimal point.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Decimal.IsWfDecimal (s : String) : Prop

Well-formed decimal syntax: s is the rendering of a well-formed Sign ::= ['-'], Natural ::= Digit⁺, '.', and Fraction ::= Digit{1,4}, concatenated in that order. This is the direct grammar transcription; it does not compute a value or invoke a parser.

Equations

• Cedar.Thm.Decimal.IsWfDecimal s = ∃ (sign : String), ∃ (natural : String), ∃ (fraction : String), Cedar.Thm.Decimal.DecimalProduction s sign natural fraction

def Cedar.Thm.Decimal.value (sign natural fraction : String) : Int

The grammar's value function, applied to an already-decomposed literal:

value = sign × (nat(Natural) × 10⁴ + nat(Fraction) × 10^(4 − |Fraction|))

IsWfFrac fraction bounds lenOf fraction ≤ DECIMAL_DIGITS, so converting the second exponent to Nat does not clamp a negative value on a well-formed field.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Decimal.IsDecimalValue (s : String) (v : Int) : Prop

v is the value of the decimal literal s: s is the rendering of a well-formed Sign ::= ['-'], Natural ::= Digit⁺, '.', and Fraction ::= Digit{1,4}, concatenated in that order, and v is what the grammar's value function assigns to those fields.

The existential supplies the split, so no string surgery (front/drop/splitToList) and no Option appear here. The relation is single-valued (isDecimalValue_unique), and a string is well-formed exactly when it has some value (wf_iff_exists_value).

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Decimal.normalize (s : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed or out-of-range inputs.

Equations

• Cedar.Thm.Decimal.normalize s = Option.map toString (Cedar.Spec.Ext.Decimal.parse s)