data.aug

JSON benchmark · Source and specification

Files in this project

• main.aug
• data.aug

Code

Indentation

// aug-spec: "data.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
record Payload(int id, string message, List<int> values)

Braces

// aug-spec: "data.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
record Payload(int id, string message, List<int> values)

Compiled specification

Interactions and sequences

Payload · immutable record · source

It takes id as an integer, kept read-only, message as a string, kept read-only, and values as List<int>, kept read-only.