Theoria.Env.Recursor (theoria v0.5.0)

Copy Markdown View Source

Lean-style metadata for an admitted inductive recursor.

Summary

Types

t()

@type t() :: %Theoria.Env.Recursor{
  inductives: [atom()],
  k?: boolean(),
  name: atom(),
  num_indices: non_neg_integer(),
  num_minors: non_neg_integer(),
  num_motives: non_neg_integer(),
  num_params: non_neg_integer(),
  rules: [Theoria.Env.RecursorRule.t()],
  type: Theoria.Term.t(),
  universe_params: [atom()]
}

Functions

major_index(recursor)

@spec major_index(t()) :: non_neg_integer()