Theoria.Env.Constructor (theoria v0.5.0)

Copy Markdown View Source

Lean-style metadata for an admitted inductive constructor.

Summary

Types

t()

Types

t()

@type t() :: %Theoria.Env.Constructor{
  constructor_index: non_neg_integer(),
  inductive: atom(),
  name: atom(),
  num_fields: non_neg_integer(),
  num_params: non_neg_integer(),
  type: Theoria.Term.t(),
  universe_params: [atom()]
}