Theoria.Env.RecursorRule (theoria v0.3.0)

Copy Markdown View Source

Lean-style iota-reduction rule metadata for a recursor constructor case.

Summary

Types

t()

Types

t()

@type t() :: %Theoria.Env.RecursorRule{
  constructor: atom(),
  field_count: non_neg_integer(),
  index_patterns: [Theoria.Term.t()],
  rhs: Theoria.Term.t()
}