Theoria.Inductive.Constructor.Result (theoria v0.6.0)

Copy Markdown View Source

Decomposed constructor target and binders.

Summary

Types

binder()
t()

Types

binder()

@type binder() :: %{name: atom(), domain: Theoria.Term.t(), depth: non_neg_integer()}

t()

@type t() :: %Theoria.Inductive.Constructor.Result{
  arguments: [Theoria.Term.t()],
  binders: [binder()],
  head: Theoria.Term.Const.t(),
  indices: [Theoria.Term.t()],
  parameters: [Theoria.Term.t()]
}