Theoria.Equation.Matcher.Type.Shape (theoria v0.5.0)

Copy Markdown View Source

Planned matcher declaration shape derived from a matcher descriptor.

Summary

Types

t()

Types

t()

@type t() :: %Theoria.Equation.Matcher.Type.Shape{
  alternative_binders: keyword(),
  alternatives: [Theoria.Equation.Matcher.Type.Alternative.t()],
  body: Theoria.Term.t(),
  discriminant_binders: keyword(),
  discriminants: [Theoria.Equation.Matcher.Info.Discriminant.t()],
  family: atom(),
  index_binders: keyword(),
  index_patterns: %{optional(atom() | boolean()) => [Theoria.Term.t()]},
  indexed?: boolean(),
  indices: keyword(),
  motive_arguments: [Theoria.Term.t()],
  motive_binders: keyword(),
  motive_name: atom(),
  motive_result: Theoria.Term.t(),
  motive_type: Theoria.Term.t(),
  parameters: keyword(),
  recursor: atom(),
  recursor_arguments: [Theoria.Term.t()],
  recursor_descriptor: Theoria.Equation.Recursor.Descriptor.t() | nil,
  result: Theoria.Term.t()
}