Lemma.ShowData (lemma_engine v0.9.11)

One declared data slot in a spec, as returned in Lemma.Show.data.

Empty needed_by_rules means offered for reuse (data x: alias.slot), not an eval intake key for this spec.

path is the import hops to this slot; empty means this spec.

type is the raw LemmaType JSON map, a Rust discriminated union tagged by its "kind" string. It is intentionally left untyped here: pattern-match on it directly (e.g. %{"kind" => "measure", "units" => units} = entry.type) rather than routing through a parallel Elixir struct hierarchy for 12 type kinds.

Summary

Types

t()

Functions

from_map(map)

Builds a Lemma.ShowData from one value of the decoded Lemma.show/4 JSON "data" map. fill/suggestion are absent (not null) from the API JSON when unset; Map.get/3 yields nil for both. path is required (empty list is valid).

Types

t()

@type t() :: %Lemma.ShowData{
  fill: map() | nil,
  needed_by_rules: [String.t()],
  path: [Lemma.PathSegment.t()],
  suggestion: map() | nil,
  type: map()
}

Functions

from_map(map)

@spec from_map(map()) :: t()