Theoria.Inductive.Declaration (theoria v0.3.0)

Copy Markdown View Source

Generated declaration plan for an inductive specification.

Summary

Types

kind()
t()

Types

kind()

@type kind() :: :inductive | :constructor | :recursor

t()

@type t() :: %Theoria.Inductive.Declaration{
  kind: kind(),
  metadata: Theoria.Env.Constant.metadata(),
  name: atom(),
  reduction: Theoria.Env.Reduction.t() | nil,
  type: Theoria.Term.t(),
  universe_params: [atom()]
}