Lean-style metadata for an admitted inductive type former.
Summary
Types
@type t() :: %Theoria.Env.Inductive{ constructors: [atom()], inductives: [atom()], name: atom(), num_indices: non_neg_integer(), num_nested: non_neg_integer(), num_params: non_neg_integer(), recursive?: boolean(), reflexive?: boolean(), type: Theoria.Term.t(), universe_params: [atom()] }