Theoria.Equation.Matcher.Equation (theoria v0.4.0)

Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation generated for a matcher alternative.

Summary

Types

t()

Functions

from_lemma(matcher, constructor, lemma)

Builds matcher-equation metadata from an ordinary equation lemma.

indexed(matcher, constructor, index_patterns)

Builds indexed matcher-equation metadata from a matcher alternative.

to_lemma(equation)

Converts matcher-equation metadata to theorem-like equation lemma metadata.

Types

t()

@type t() :: %Theoria.Equation.Matcher.Equation{
  binders: [Theoria.Equation.Lemma.binder()],
  constructor: atom(),
  equality_type: Theoria.Term.t(),
  identity: Theoria.Equation.Identity.t() | nil,
  index_patterns: [Theoria.Term.t()],
  indexed?: boolean(),
  left: Theoria.Term.t(),
  matcher: atom(),
  name: atom() | Theoria.Equation.Identity.t(),
  proof: Theoria.Term.t() | nil,
  realizable?: boolean(),
  right: Theoria.Term.t(),
  source: Theoria.Equation.Lemma.t() | nil,
  statement_name: atom() | Theoria.Equation.Identity.t() | nil,
  statement_status: :planned | :realizable | :realized | :unsupported,
  statement_type: Theoria.Term.t() | nil
}

Functions

from_lemma(matcher, constructor, lemma)

@spec from_lemma(atom(), atom(), Theoria.Equation.Lemma.t()) :: t()

Builds matcher-equation metadata from an ordinary equation lemma.

indexed(matcher, constructor, index_patterns)

@spec indexed(atom(), atom(), [Theoria.Term.t()]) :: t()

Builds indexed matcher-equation metadata from a matcher alternative.

to_lemma(equation)

@spec to_lemma(t()) :: Theoria.Equation.Lemma.t()

Converts matcher-equation metadata to theorem-like equation lemma metadata.