Theoria.Inductive.Spec (theoria v0.3.0)

Copy Markdown View Source

Structured description of an inductive family.

Summary

Types

t()

Functions

constructor(spec, name, type)
index(spec, name, type)
new(name, type, opts \\ [])
parameter(spec, name, type)
recursor(spec, name, type, reduction)

Types

t()

@type t() :: %Theoria.Inductive.Spec{
  constructors: [Theoria.Inductive.Constructor.t()],
  indices: [Theoria.Inductive.Index.t()],
  name: atom(),
  num_params: non_neg_integer(),
  parameters: [Theoria.Inductive.Parameter.t()],
  recursors: [Theoria.Inductive.Recursor.t()],
  type: Theoria.Term.t(),
  universe_params: [atom()]
}

Functions

constructor(spec, name, type)

@spec constructor(t(), atom(), Theoria.Term.t()) :: t()

index(spec, name, type)

@spec index(t(), atom(), Theoria.Term.t()) :: t()

new(name, type, opts \\ [])

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

parameter(spec, name, type)

@spec parameter(t(), atom(), Theoria.Term.t()) :: t()

recursor(spec, name, type, reduction)

@spec recursor(t(), atom(), Theoria.Term.t(), Theoria.Env.Reduction.t()) :: t()