Theoria.Env.Constant (theoria v0.3.0)

Copy Markdown View Source

A checked constant or definition in a kernel environment.

Summary

Types

kind()
metadata()
t()

Types

kind()

@type kind() ::
  :constant
  | :axiom
  | :definition
  | :theorem
  | :inductive
  | :constructor
  | :recursor
  | :matcher

metadata()

@type metadata() ::
  Theoria.Env.Inductive.t()
  | Theoria.Env.Constructor.t()
  | Theoria.Env.Recursor.t()
  | Theoria.Env.Matcher.t()
  | Theoria.Equation.Info.t()
  | nil

t()

@type t() :: %Theoria.Env.Constant{
  kind: kind(),
  metadata: metadata(),
  reducible?: boolean(),
  reduction: Theoria.Env.Reduction.t() | nil,
  type: Theoria.Term.t(),
  universe_params: [atom()],
  value: Theoria.Term.t() | nil
}