6. Demo🔗

The Demo opens the Cedar examples in the public lean4web editor. Select a format, then open its grammar source, generated readable specification, generated parser, or completed soundness proofs.

Lean4web loads the exact source from Triptych's main branch. The public server does not install Triptych's custom Lake dependencies, so this Demo is for browsing and editing source. The repository's CI checks the files in the complete cedar-examples project.

To generate files, edit the real grammar module locally and run lake env lean Inputs/Decimal.lean from cedar-examples.

The active to "Outputs/Decimal" clause rewrites generated spec.lean and parser.lean. It creates soundness.lean once and then preserves that file because it contains user proofs.

Use New grammar to open a separate editor with a small signed-natural starting point.