Theoria.Equation.Signature (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. Telescope summary for compiler-owned equation metadata generation.

Summary

Types

binder()

t()

Functions

new(name, family, arguments, result_type, opts \\ [])

Builds a definition signature for equation metadata generation.

Types

binder()

@type binder() :: {atom(), Theoria.Term.t()}

t()

@type t() :: %Theoria.Equation.Signature{
  arguments: [binder()],
  discriminant_positions: [non_neg_integer()] | nil,
  family: atom(),
  fixed_params: Theoria.Equation.FixedParams.t(),
  name: atom(),
  parameters: [binder()],
  rec_arg_pos: non_neg_integer(),
  result_type: Theoria.Term.t()
}

Functions

new(name, family, arguments, result_type, opts \\ [])

@spec new(atom(), atom(), [binder()], Theoria.Term.t(), keyword()) :: t()

Builds a definition signature for equation metadata generation.