2.2. Artifact one: the readable spec🔗

Elaboration writes Outputs/Decimal/spec.lean. Each production becomes a plain predicate over strings. Here is the generated sign predicate:

def Decimal.IsWf.Sign : String → Prop :=
fun s => s = "-" ∨ s = ""#print Decimal.IsWf.Sign

def Decimal.IsWf.Sign : String → Prop :=
fun s => s = "-" ∨ s = ""

The top-level predicate composes them along the concatenation structure — one existentially quantified variable per named capture, one conjunct per production:

def Decimal.IsWf.Decimal : String → Prop :=
fun s =>
  ∃ «sign» natural fraction,
    ((s = «sign» ++ natural ++ "." ++ fraction ∧ Decimal.IsWf.Sign «sign») ∧ Decimal.IsWf.Natural natural) ∧
      Decimal.IsWf.Fraction fraction#print Decimal.IsWf.Decimal

def Decimal.IsWf.Decimal : String → Prop :=
fun s =>
  ∃ «sign» natural fraction,
    ((s = «sign» ++ natural ++ "." ++ fraction ∧ Decimal.IsWf.Sign «sign») ∧ Decimal.IsWf.Natural natural) ∧
      Decimal.IsWf.Fraction fraction

The root predicate composes the productions, and Decimal.IsValid conjoins shape with the final-value range:

@[reducible] def Decimal.IsValid : String → Prop :=
fun s => Decimal.IsWf s ∧ Decimal.SatisfiesConstraints s#print Decimal.IsValid

@[reducible] def Decimal.IsValid : String → Prop :=
fun s => Decimal.IsWf s ∧ Decimal.SatisfiesConstraints s

2.2.1. A typed field view🔗

After parsing "-12.34", most code wants the useful pieces: the sign "-", the natural digits "12", and the fraction digits "34". It should not need to understand how the parser stores captures or records grammar choices.

The generated Decimal.View packages those pieces as named fields. Its input field keeps the original string, while the other fields contain the text matched by the grammar's named productions:

example : Decimal.View :=
  {
    input := "-12.34"
    sign := "-"
    natural := "12"
    fraction := "34"
  }

example (view : Decimal.View) : String :=
  view.natural ++ "." ++ view.fraction

Code using a view can simply write view.natural or view.fraction. Without this record, each caller would have to inspect the parser's generic capture map and know how the grammar match was represented internally.

2.2.2. A structural derivation🔗

A view deliberately forgets how the grammar matched. That keeps ordinary field access simple, but printer and roundtrip proofs need the missing structure: which alternative was selected, which optional pieces were present, and how repeated or referenced productions were built.

A derivation preserves that evidence as a tree. This gives a printer a grammar-shaped target: construct a valid derivation for a domain value, then turn the derivation into text. Its constructor records the chosen alternative, while its children record how each referenced production matched. For Decimal, the root constructor has children for Sign, Natural, and Fraction. The dot is a fixed literal, so it does not need its own field:

example
    (signTree : Decimal.Derivation.Sign)
    (natural : Decimal.Derivation.Natural)
    (fraction : Decimal.Derivation.Fraction) :
    Decimal.Derivation.Decimal :=
  .alt0 signTree natural fraction

2.2.3. Rendering for verified printers🔗

Parsing moves from text to a derivation and its fields. Decimal.Derivation.Decimal.render performs the tree-to-text direction: it concatenates the terminal strings stored in a derivation and inserts the grammar's fixed literals.

example :
    decimalDerivation =
      .alt0
        (.alt0 (some ()))
        (.alt0 "12")
        (.alt0 "34") := by⊢ decimalDerivation =
  CedarExamples.Decimal.Decimal.Derivation.Decimal.alt0 (CedarExamples.Decimal.Decimal.Derivation.Sign.alt0 (some ()))
    (CedarExamples.Decimal.Decimal.Derivation.Natural.alt0 "12")
    (CedarExamples.Decimal.Decimal.Derivation.Fraction.alt0 "34")
  rflAll goals completed! 🐙

Evaluating rendering and validity together makes their separate roles visible:

("-12.34", true)#eval
  (decimalDerivation.render,
    decide decimalDerivation.Valid)

("-12.34", true)

Crucially, Decimal.Derivation.Decimal.render does not validate the tree. Terminal nodes store ordinary strings, so rendering also serializes a Natural node whose text violates the grammar:

("abc", false)#eval
  let tree := Decimal.Derivation.Natural.alt0 "abc"
  (tree.render, decide tree.Valid)

("abc", false)

The text "abc" is still rendered; the separate Decimal.Derivation.Natural.Valid predicate rejects it.

Therefore Decimal.Derivation.Decimal.render is not itself a verified Decimal printer. A printer certificate chooses a derivation for each domain value and proves that the tree is valid and denotes that value; Decimal.Derivation.Decimal.render performs only the final tree-to-string step. For valid derivations, later engine theorems prove that decoding the rendered text recovers the tree's captures and typed view.

Note: Decimal.Derivation.Decimal.Valid checks only that the derivation is well-formed according to the grammar, corresponding to the string-level Decimal.IsWf. Decimal.IsValid checks both Decimal.IsWf and Decimal.SatisfiesConstraints; for Decimal, the semantic constraint requires the computed value to fit in Int64.