Typed projection of the map returned by Lemma.show/4: a Draft 2020-12 JSON
Schema for the spec's evaluation-data inputs, with Lemma metadata under x-lemma-*.
Validate evaluation data against schema (the decoded document, unchanged). The struct
fields read the document: spec is title, commentary is description, types
is x-lemma-types (local data declarations), data is properties (inputs rules
need, as Lemma.ShowData), required the unbound ones, rows the instance-list
row schemas in $defs (as Lemma.ShowRow), and the remaining fields the matching
x-lemma-* keywords.
Optional repository is the interned repository name (nil for the unnamed
workspace). Rule values are Lemma.ShowRule structs (type, path, branches,
depends_on_rules); each rule type is a raw LemmaType JSON map tagged by
"kind". meta and types values are raw JSON maps.
Lemma.show/4 itself returns the plain decoded map; call from_map/1 on that map
to get a typed struct.
Summary
Functions
Builds a Lemma.Show struct from the map decoded from Lemma.show/4's JSON.
Local data declarations (x-lemma-types).
Types
@type t() :: %Lemma.Show{ commentary: String.t() | nil, data: %{optional(String.t()) => Lemma.ShowData.t()}, effective_from: String.t() | nil, effective_to: String.t() | nil, meta: %{optional(String.t()) => map()}, repository: String.t() | nil, required: [String.t()], rows: %{optional(String.t()) => Lemma.ShowRow.t()}, rules: %{optional(String.t()) => Lemma.ShowRule.t()}, schema: map(), source_type: String.t() | map() | nil, spec: String.t(), start_line: non_neg_integer(), types: %{optional(String.t()) => map()} }
Functions
Builds a Lemma.Show struct from the map decoded from Lemma.show/4's JSON.
Raises KeyError if a required keyword (title, properties,
x-lemma-start-line, x-lemma-meta, x-lemma-types, x-lemma-rules) is missing;
that shape never comes from a real Lemma.show/4 call, so a missing key here is a
caller bug, not a recoverable Show variant.
Local data declarations (x-lemma-types).