Theoria.Equation.Matcher.Info (theoria v0.6.0)

Experimental/internal API for 0.2; subject to change before 0.3. Small Theoria-side mirror of Lean matcher metadata.

Summary

Types

t()

Functions

arity(info)

Returns total matcher arity in Lean's broad shape: params + motive + discriminants + alternatives.

default_name(definition_name, ordinal \\ 1)

Returns the default generated matcher declaration name for a definition.

for_schema(definition_name, schema, opts \\ [])

Builds matcher metadata from supported equation schema metadata.

new(name, num_params, num_discriminants, alternatives, opts \\ [])

Builds matcher metadata.

source_name(matcher_name)

Returns the source definition prefix for a default generated matcher declaration.

Types

t()

@type t() :: %Theoria.Equation.Matcher.Info{
  alternatives: [Theoria.Equation.Matcher.Info.Alternative.t()],
  discriminants: [Theoria.Equation.Matcher.Info.Discriminant.t()],
  elim_level_position: non_neg_integer() | nil,
  name: atom(),
  num_discriminants: pos_integer(),
  num_params: non_neg_integer(),
  overlaps: %{optional(non_neg_integer()) => [non_neg_integer()]}
}

Functions

arity(info)

@spec arity(t()) :: non_neg_integer()

Returns total matcher arity in Lean's broad shape: params + motive + discriminants + alternatives.

default_name(definition_name, ordinal \\ 1)

@spec default_name(atom(), pos_integer()) :: atom()

Returns the default generated matcher declaration name for a definition.

for_schema(definition_name, schema, opts \\ [])

@spec for_schema(atom(), Theoria.Equation.Schema.t(), keyword()) :: t()

Builds matcher metadata from supported equation schema metadata.

new(name, num_params, num_discriminants, alternatives, opts \\ [])

@spec new(
  atom(),
  non_neg_integer(),
  pos_integer(),
  [Theoria.Equation.Matcher.Info.Alternative.t()],
  keyword()
) :: t()

Builds matcher metadata.

source_name(matcher_name)

@spec source_name(atom()) :: {:ok, atom()} | :error

Returns the source definition prefix for a default generated matcher declaration.