# mathlib3documentation

core / init.core

def id_delta {α : Sort u} (a : α) :
α

The kernel definitional equality test (t =?= s) has special support for id_delta applications. It implements the following rules

1. (id_delta t) =?= t
2. t =?= (id_delta t)
3. (id_delta t) =?= s IF (unfold_of t) =?= s
4. t =?= id_delta s IF t =?= (unfold_of s)

This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.

We use id_delta applications to address performance problems when type checking lemmas generated by the equation compiler.

@[reducible]
def opt_param (α : Sort u) (default : α) :

@[reducible]
def out_param (α : Sort u) :

Gadget for marking output parameters in type classes.

@[reducible]
def id_rhs (α : Sort u) (a : α) :
α

id_rhs is an auxiliary declaration used in the equation compiler to address performance issues when proving equational lemmas. The equation compiler uses it as a marker.

structure punit  :
Instances for `punit`
@[reducible]
def unit  :

An abbreviation for `punit.{0}`, its most common instantiation. This type should be preferred over `punit` where possible to avoid unnecessary universe parameters.

@[reducible]
def unit.star  :
@[reducible]
def thunk (α : Type u) :

Gadget for defining thunks, thunk parameters have special treatment. Example: given def f (s : string) (t : thunk nat) : nat an application f "hello" 10 is converted into f "hello" (λ _, 10)

structure true  :
Prop
Instances for `true`
inductive false  :
Prop
Instances for `false`
inductive empty  :
Instances for `empty`
def not (a : Prop) :
Prop

Logical not.

`not P`, with notation `¬ P`, is the `Prop` which is true if and only if `P` is false. It is internally represented as `P → false`, so one way to prove a goal `⊢ ¬ P` is to use `intro h`, which gives you a new hypothesis `h : P` and the goal `⊢ false`.

A hypothesis `h : ¬ P` can be used in term mode as a function, so if `w : P` then `h w : false`.

Related mathlib tactic: `contrapose`.

Instances for `not`
inductive eq {α : Sort u} (a : α) :
α Prop
• refl : {α : Sort u} (a : α), a = a
Instances for `eq`

Initialize the quotient module, which effectively adds the following definitions:

``````constant quot {α : Sort u} (r : α → α → Prop) : Sort u

constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r

constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → eq (f a) (f b)) → quot r → β

constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
(∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q
``````

Also the reduction rule:

``````quot.lift f _ (quot.mk a) ~~> f a
```
``````
inductive heq {α : Sort u} (a : α) {β : Sort u} :
β Prop

Heterogeneous equality.

Its purpose is to write down equalities between terms whose types are not definitionally equal. For example, given `x : vector α n` and `y : vector α (0+n)`, `x = y` doesn't typecheck but `x == y` does.

If you have a goal `⊢ x == y`, your first instinct should be to ask (either yourself, or on zulip) if something has gone wrong already. If you really do need to follow this route, you may find the lemmas `eq_rec_heq` and `eq_mpr_heq` useful.

structure prod (α : Type u) (β : Type v) :
Type (max u v)
• fst : α
• snd : β
Instances for `prod`
structure pprod (α : Sort u) (β : Sort v) :
Sort (max 1 u v)
• fst : α
• snd : β

Similar to `prod`, but α and β can be propositions. We use this type internally to automatically generate the brec_on recursor.

Instances for `pprod`
structure and (a b : Prop) :
Prop
• left : a
• right : b

Logical and.

`and P Q`, with notation `P ∧ Q`, is the `Prop` which is true precisely when `P` and `Q` are both true.

To prove a goal `⊢ P ∧ Q`, you can use the tactic `split`, which gives two separate goals `⊢ P` and `⊢ Q`.

Given a hypothesis `h : P ∧ Q`, you can use the tactic `cases h with hP hQ` to obtain two new hypotheses `hP : P` and `hQ : Q`. See also the `obtain` or `rcases` tactics in mathlib.

Instances for `and`
theorem and.elim_left {a b : Prop} (h : a b) :
a
theorem and.elim_right {a b : Prop} (h : a b) :
b
@[nolint]
def rfl {α : Sort u} {a : α} :
a = a
theorem eq.subst {α : Sort u} {P : α Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :
P b
@[trans]
theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :
a = c
@[symm]
theorem eq.symm {α : Sort u} {a b : α} (h : a = b) :
b = a
def heq.rfl {α : Sort u} {a : α} :
a == a
theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') :
a = a'
inductive sum (α : Type u) (β : Type v) :
Type (max u v)
Instances for `sum`
inductive psum (α : Sort u) (β : Sort v) :
Sort (max 1 u v)
Instances for `psum`
inductive or (a b : Prop) :
Prop

Logical or.

`or P Q`, with notation `P ∨ Q`, is the proposition which is true if and only if `P` or `Q` is true.

To prove a goal `⊢ P ∨ Q`, if you know which alternative you want to prove, you can use the tactics `left` (which gives the goal `⊢ P`) or `right` (which gives the goal `⊢ Q`).

Given a hypothesis `h : P ∨ Q` and goal `⊢ R`, the tactic `cases h` will give you two copies of the goal `⊢ R`, with the hypothesis `h : P` in the first, and the hypothesis `h : Q` in the second.

Instances for `or`
theorem or.intro_left {a : Prop} (b : Prop) (ha : a) :
a b
theorem or.intro_right (a : Prop) {b : Prop} (hb : b) :
a b
structure sigma {α : Type u} (β : α Type v) :
Type (max u v)
• fst : α
• snd : β self.fst
Instances for `sigma`
structure psigma {α : Sort u} (β : α Sort v) :
Sort (max 1 u v)
• fst : α
• snd : β self.fst
Instances for `psigma`
inductive bool  :
Instances for `bool`
structure subtype {α : Sort u} (p : α Prop) :
Sort (max 1 u)
• val : α
• property : p self.val

Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description.

Instances for `subtype`
@[class]
inductive decidable (p : Prop) :
• is_false : Π {p : Prop}, ¬p
• is_true : Π {p : Prop}, p
Instances of this typeclass
Instances of other typeclasses for `decidable`
@[reducible]
def decidable_pred {α : Sort u} (r : α Prop) :
Sort (max u 1)
Equations
@[reducible]
def decidable_rel {α : Sort u} (r : α α Prop) :
Sort (max u 1)
Equations
@[reducible]
def decidable_eq (α : Sort u) :
Sort (max u 1)
Equations
inductive option (α : Type u) :
Instances for `option`
inductive list (T : Type u) :
Instances for `list`
inductive nat  :
• zero :
• succ :
Instances for `nat`
structure unification_constraint  :
Type (u+1)
• α : Type ?
• lhs : self.α
• rhs : self.α
Instances for `unification_constraint`
structure unification_hint  :
Type (max (u_1+1) (u_2+1))
Instances for `unification_hint`

Declare builtin and reserved notation

@[ext, class]
structure has_zero (α : Type u) :
• zero : α
Instances of this typeclass
@[class]
structure has_one (α : Type u) :
• one : α
Instances of this typeclass
@[class]
structure has_add (α : Type u) :
Instances of this typeclass
@[class]
structure has_mul (α : Type u) :
Instances of this typeclass
@[class]
structure has_inv (α : Type u) :
• inv : α α
Instances of this typeclass
@[class]
structure has_neg (α : Type u) :
• neg : α α
Instances of this typeclass
@[class]
structure has_sub (α : Type u) :
Instances of this typeclass
@[class]
structure has_div (α : Type u) :
Instances of this typeclass
@[class]
structure has_dvd (α : Type u) :
Instances of this typeclass
@[class]
structure has_mod (α : Type u) :
Instances of this typeclass
@[ext, class]
structure has_le (α : Type u) :
Instances of this typeclass
@[class]
structure has_lt (α : Type u) :
Instances of this typeclass
@[class]
structure has_append (α : Type u) :
Instances of this typeclass
@[class]
structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :
Type (max u v w)
Instances of this typeclass
@[class]
structure has_union (α : Type u) :
Instances of this typeclass
@[class]
structure has_inter (α : Type u) :
Instances of this typeclass
@[class]
structure has_sdiff (α : Type u) :
Instances of this typeclass
@[class]
structure has_equiv (α : Sort u) :
Sort (max 1 u)
Instances of this typeclass
@[class]
structure has_subset (α : Type u) :
Instances of this typeclass
@[class]
structure has_ssubset (α : Type u) :
• ssubset : α α Prop
Instances of this typeclass

Type classes `has_emptyc` and `has_insert` are used to implement polymorphic notation for collections. Example: `{a, b, c} = insert a (insert b (singleton c))`.

Note that we use `pair` in the name of lemmas about `{x, y} = insert x (singleton y)`.

@[class]
structure has_emptyc (α : Type u) :
• emptyc : α
Instances of this typeclass
@[class]
structure has_insert (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
Instances of this typeclass
@[class]
structure has_singleton (α : out_param (Type u)) (β : Type v) :
Type (max u v)
• singleton : α β
Instances of this typeclass
@[class]
structure has_sep (α : out_param (Type u)) (γ : Type v) :
Type (max u v)

Type class used to implement the notation { a ∈ c | p a }

Instances of this typeclass
@[class]
structure has_mem (α : out_param (Type u)) (γ : Type v) :
Type (max u v)

Type class for set-like membership

Instances of this typeclass
@[class]
structure has_pow (α : Type u) (β : Type v) :
Type (max u v)
Instances of this typeclass
@[reducible]
def ge {α : Type u} [has_le α] (a b : α) :
Prop
Equations
@[reducible]
def gt {α : Type u} [has_lt α] (a b : α) :
Prop
Equations
• a > b = (b < a)
@[reducible]
def superset {α : Type u} [has_subset α] (a b : α) :
Prop
Equations
@[reducible]
def ssuperset {α : Type u} [has_ssubset α] (a b : α) :
Prop
Equations
def bit0 {α : Type u} [s : has_add α] (a : α) :
α
Equations
Instances for `bit0`
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) :
α
Equations
Instances for `bit1`
@[class]
structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [ β] [ β] :
Prop
• insert_emptyc_eq : (x : α), {x} = {x}
Instances of this typeclass

nat basic instances

@[protected]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.has_one  :
Equations
@[protected, instance]
Equations
Equations
Equations
@[protected]
def nat.prio  :
Equations
def std.prec.max  :
Equations
Equations

This def is "max + 10". It can be used e.g. for postfix operations that should be stronger than application.

Equations
@[class]
structure has_sizeof (α : Sort u) :
Sort (max 1 u)
Instances of this typeclass
• default_has_sizeof
• slim_check.sampleable_ext.wf
• slim_check.sampleable.wf
• nat.has_sizeof
• prod.has_sizeof
• sum.has_sizeof
• psum.has_sizeof
• sigma.has_sizeof
• psigma.has_sizeof
• punit.has_sizeof
• bool.has_sizeof
• option.has_sizeof
• list.has_sizeof
• subtype.has_sizeof
• bin_tree.has_sizeof_inst
• inhabited.has_sizeof_inst
• ulift.has_sizeof_inst
• plift.has_sizeof_inst
• has_well_founded.has_sizeof_inst
• setoid.has_sizeof_inst
• char.has_sizeof_inst
• char.has_sizeof
• string_imp.has_sizeof_inst
• string.iterator_imp.has_sizeof_inst
• string.has_sizeof
• fin.has_sizeof_inst
• has_repr.has_sizeof_inst
• ordering.has_sizeof_inst
• has_lift.has_sizeof_inst
• has_lift_t.has_sizeof_inst
• has_coe.has_sizeof_inst
• has_coe_t.has_sizeof_inst
• has_coe_to_fun.has_sizeof_inst
• has_coe_to_sort.has_sizeof_inst
• has_coe_t_aux.has_sizeof_inst
• has_to_string.has_sizeof_inst
• name.has_sizeof_inst
• functor.has_sizeof_inst
• has_pure.has_sizeof_inst
• has_seq.has_sizeof_inst
• has_seq_left.has_sizeof_inst
• has_seq_right.has_sizeof_inst
• applicative.has_sizeof_inst
• has_orelse.has_sizeof_inst
• alternative.has_sizeof_inst
• has_bind.has_sizeof_inst
• format.color.has_sizeof_inst
• pos.has_sizeof_inst
• binder_info.has_sizeof_inst
• reducibility_hints.has_sizeof_inst
• environment.projection_info.has_sizeof_inst
• environment.implicit_infer_kind.has_sizeof_inst
• tactic.transparency.has_sizeof_inst
• tactic.new_goals.has_sizeof_inst
• tactic.apply_cfg.has_sizeof_inst
• param_info.has_sizeof_inst
• fun_info.has_sizeof_inst
• subsingleton_info.has_sizeof_inst
• occurrences.has_sizeof_inst
• tactic.rewrite_cfg.has_sizeof_inst
• tactic.dsimp_config.has_sizeof_inst
• tactic.dunfold_config.has_sizeof_inst
• tactic.delta_config.has_sizeof_inst
• tactic.unfold_proj_config.has_sizeof_inst
• tactic.simp_config.has_sizeof_inst
• tactic.simp_intros_config.has_sizeof_inst
• interactive.loc.has_sizeof_inst
• cc_config.has_sizeof_inst
• congr_arg_kind.has_sizeof_inst
• tactic.interactive.case_tag.has_sizeof_inst
• tactic.interactive.case_tag.match_result.has_sizeof_inst
• tactic.unfold_config.has_sizeof_inst
• except.has_sizeof_inst
• except_t.has_sizeof_inst
• state_t.has_sizeof_inst
• option_t.has_sizeof_inst
• vm_obj_kind.has_sizeof_inst
• vm_decl_kind.has_sizeof_inst
• ematch_config.has_sizeof_inst
• smt_pre_config.has_sizeof_inst
• smt_config.has_sizeof_inst
• rsimp.config.has_sizeof_inst
• expr.coord.has_sizeof_inst
• preorder.has_sizeof_inst
• partial_order.has_sizeof_inst
• linear_order.has_sizeof_inst
• int.has_sizeof_inst
• d_array.has_sizeof_inst
• widget.mouse_event_kind.has_sizeof_inst
• feature_search.feature_cfg.has_sizeof_inst
• feature_search.predictor_type.has_sizeof_inst
• feature_search.predictor_cfg.has_sizeof_inst
• doc_category.has_sizeof_inst
• tactic_doc_entry.has_sizeof_inst
• dlist.has_sizeof_inst
• pempty.has_sizeof_inst
• rbnode.has_sizeof_inst
• rbnode.color.has_sizeof_inst
• random_gen.has_sizeof_inst
• std_gen.has_sizeof_inst
• io.error.has_sizeof_inst
• io.mode.has_sizeof_inst
• io.process.stdio.has_sizeof_inst
• io.process.spawn_args.has_sizeof_inst
• function.has_uncurry.has_sizeof_inst
• lint_verbosity.has_sizeof_inst
• tactic.explode.status.has_sizeof_inst
• auto.auto_config.has_sizeof_inst
• auto.case_option.has_sizeof_inst
• tactic.itauto.and_kind.has_sizeof_inst
• tactic.itauto.prop.has_sizeof_inst
• tactic.itauto.proof.has_sizeof_inst
• can_lift.has_sizeof_inst
• norm_cast.label.has_sizeof_inst
• _nest_1_1._nest_1_1.tactic.tactic_script._mut_.has_sizeof_inst
• _nest_1_1.tactic.tactic_script.has_sizeof_inst
• _nest_1_1.list.tactic.tactic_script.has_sizeof_inst
• tactic.tactic_script.has_sizeof_inst
• simps_cfg.has_sizeof_inst
• applicative_transformation.has_sizeof_inst
• traversable.has_sizeof_inst
• is_lawful_traversable.has_sizeof_inst
• has_vsub.has_sizeof_inst
• has_smul.has_sizeof_inst
• semigroup.has_sizeof_inst
• comm_semigroup.has_sizeof_inst
• left_cancel_semigroup.has_sizeof_inst
• right_cancel_semigroup.has_sizeof_inst
• mul_one_class.has_sizeof_inst
• monoid.has_sizeof_inst
• comm_monoid.has_sizeof_inst
• left_cancel_monoid.has_sizeof_inst
• right_cancel_monoid.has_sizeof_inst
• cancel_monoid.has_sizeof_inst
• cancel_comm_monoid.has_sizeof_inst
• has_involutive_neg.has_sizeof_inst
• has_involutive_inv.has_sizeof_inst
• div_inv_monoid.has_sizeof_inst
• sub_neg_monoid.has_sizeof_inst
• neg_zero_class.has_sizeof_inst
• sub_neg_zero_monoid.has_sizeof_inst
• inv_one_class.has_sizeof_inst
• div_inv_one_monoid.has_sizeof_inst
• subtraction_monoid.has_sizeof_inst
• division_monoid.has_sizeof_inst
• subtraction_comm_monoid.has_sizeof_inst
• division_comm_monoid.has_sizeof_inst
• group.has_sizeof_inst
• comm_group.has_sizeof_inst
• unique.has_sizeof_inst
• units.has_sizeof_inst
• mul_zero_class.has_sizeof_inst
• semigroup_with_zero.has_sizeof_inst
• mul_zero_one_class.has_sizeof_inst
• monoid_with_zero.has_sizeof_inst
• cancel_monoid_with_zero.has_sizeof_inst
• comm_monoid_with_zero.has_sizeof_inst
• cancel_comm_monoid_with_zero.has_sizeof_inst
• group_with_zero.has_sizeof_inst
• comm_group_with_zero.has_sizeof_inst
• fun_like.has_sizeof_inst
• embedding_like.has_sizeof_inst
• equiv_like.has_sizeof_inst
• equiv.has_sizeof_inst
• has_compl.has_sizeof_inst
• has_sup.has_sizeof_inst
• has_inf.has_sizeof_inst
• zero_hom.has_sizeof_inst
• zero_hom_class.has_sizeof_inst
• one_hom.has_sizeof_inst
• one_hom_class.has_sizeof_inst
• mul_hom.has_sizeof_inst
• mul_hom_class.has_sizeof_inst
• monoid_hom.has_sizeof_inst
• monoid_hom_class.has_sizeof_inst
• monoid_with_zero_hom.has_sizeof_inst
• monoid_with_zero_hom_class.has_sizeof_inst
• function.embedding.has_sizeof_inst
• mul_action.has_sizeof_inst
• smul_zero_class.has_sizeof_inst
• distrib_smul.has_sizeof_inst
• distrib_mul_action.has_sizeof_inst
• mul_distrib_mul_action.has_sizeof_inst
• has_nat_cast.has_sizeof_inst
• has_int_cast.has_sizeof_inst
• distrib.has_sizeof_inst
• left_distrib_class.has_sizeof_inst
• right_distrib_class.has_sizeof_inst
• non_unital_non_assoc_semiring.has_sizeof_inst
• non_unital_semiring.has_sizeof_inst
• non_assoc_semiring.has_sizeof_inst
• semiring.has_sizeof_inst
• non_unital_comm_semiring.has_sizeof_inst
• comm_semiring.has_sizeof_inst
• has_distrib_neg.has_sizeof_inst
• non_unital_non_assoc_ring.has_sizeof_inst
• non_unital_ring.has_sizeof_inst
• non_assoc_ring.has_sizeof_inst
• ring.has_sizeof_inst
• non_unital_comm_ring.has_sizeof_inst
• comm_ring.has_sizeof_inst
• invertible.has_sizeof_inst
• is_nonstrict_strict_order.has_sizeof_inst
• semilattice_sup.has_sizeof_inst
• semilattice_inf.has_sizeof_inst
• lattice.has_sizeof_inst
• distrib_lattice.has_sizeof_inst
• has_top.has_sizeof_inst
• has_bot.has_sizeof_inst
• order_top.has_sizeof_inst
• order_bot.has_sizeof_inst
• bounded_order.has_sizeof_inst
• has_himp.has_sizeof_inst
• has_hnot.has_sizeof_inst
• generalized_heyting_algebra.has_sizeof_inst
• generalized_coheyting_algebra.has_sizeof_inst
• heyting_algebra.has_sizeof_inst
• coheyting_algebra.has_sizeof_inst
• biheyting_algebra.has_sizeof_inst
• generalized_boolean_algebra.has_sizeof_inst
• boolean_algebra.has_sizeof_inst
• non_unital_ring_hom.has_sizeof_inst
• non_unital_ring_hom_class.has_sizeof_inst
• ring_hom.has_sizeof_inst
• ring_hom_class.has_sizeof_inst
• mul_equiv.has_sizeof_inst
• mul_equiv_class.has_sizeof_inst
• equiv_functor.has_sizeof_inst
• rel_hom.has_sizeof_inst
• rel_hom_class.has_sizeof_inst
• rel_embedding.has_sizeof_inst
• rel_iso.has_sizeof_inst
• tactic.interactive.mono_cfg.has_sizeof_inst
• tactic.interactive.mono_selection.has_sizeof_inst
• order_hom.has_sizeof_inst
• order_iso_class.has_sizeof_inst
• ordered_comm_monoid.has_sizeof_inst
• linear_ordered_comm_monoid.has_sizeof_inst
• ordered_cancel_comm_monoid.has_sizeof_inst
• linear_ordered_cancel_comm_monoid.has_sizeof_inst
• ordered_comm_group.has_sizeof_inst
• linear_ordered_comm_group.has_sizeof_inst
• canonically_ordered_monoid.has_sizeof_inst
• canonically_linear_ordered_monoid.has_sizeof_inst
• zero_le_one_class.has_sizeof_inst
• linear_ordered_comm_monoid_with_zero.has_sizeof_inst
• ordered_semiring.has_sizeof_inst
• ordered_comm_semiring.has_sizeof_inst
• ordered_ring.has_sizeof_inst
• ordered_comm_ring.has_sizeof_inst
• strict_ordered_semiring.has_sizeof_inst
• strict_ordered_comm_semiring.has_sizeof_inst
• strict_ordered_ring.has_sizeof_inst
• strict_ordered_comm_ring.has_sizeof_inst
• linear_ordered_semiring.has_sizeof_inst
• linear_ordered_comm_semiring.has_sizeof_inst
• linear_ordered_ring.has_sizeof_inst
• linear_ordered_comm_ring.has_sizeof_inst
• canonically_ordered_comm_semiring.has_sizeof_inst
• has_abs.has_sizeof_inst
• has_pos_part.has_sizeof_inst
• has_neg_part.has_sizeof_inst
• linear_ordered_comm_group_with_zero.has_sizeof_inst
• multiset.has_sizeof
• expr_lens.dir.has_sizeof_inst
• tactic.interactive.rep_arity.has_sizeof_inst
• has_Sup.has_sizeof_inst
• has_Inf.has_sizeof_inst
• complete_semilattice_Sup.has_sizeof_inst
• complete_semilattice_Inf.has_sizeof_inst
• complete_lattice.has_sizeof_inst
• complete_linear_order.has_sizeof_inst
• order.frame.has_sizeof_inst
• order.coframe.has_sizeof_inst
• complete_distrib_lattice.has_sizeof_inst
• complete_boolean_algebra.has_sizeof_inst
• galois_insertion.has_sizeof_inst
• galois_coinsertion.has_sizeof_inst
• finset.has_sizeof_inst
• fintype.has_sizeof_inst
• rat.has_sizeof_inst
• has_rat_cast.has_sizeof_inst
• division_semiring.has_sizeof_inst
• division_ring.has_sizeof_inst
• semifield.has_sizeof_inst
• field.has_sizeof_inst
• linear_ordered_semifield.has_sizeof_inst
• linear_ordered_field.has_sizeof_inst
• nonneg_hom_class.has_sizeof_inst
• submultiplicative_hom_class.has_sizeof_inst
• nonarchimedean_hom_class.has_sizeof_inst
• group_seminorm_class.has_sizeof_inst
• group_norm_class.has_sizeof_inst
• ring_seminorm_class.has_sizeof_inst
• ring_norm_class.has_sizeof_inst
• mul_ring_seminorm_class.has_sizeof_inst
• mul_ring_norm_class.has_sizeof_inst
• tactic.positivity.order_rel.has_sizeof_inst
• top_hom.has_sizeof_inst
• bot_hom.has_sizeof_inst
• bounded_order_hom.has_sizeof_inst
• top_hom_class.has_sizeof_inst
• bot_hom_class.has_sizeof_inst
• bounded_order_hom_class.has_sizeof_inst
• sup_hom.has_sizeof_inst
• inf_hom.has_sizeof_inst
• sup_bot_hom.has_sizeof_inst
• inf_top_hom.has_sizeof_inst
• lattice_hom.has_sizeof_inst
• bounded_lattice_hom.has_sizeof_inst
• sup_hom_class.has_sizeof_inst
• inf_hom_class.has_sizeof_inst
• sup_bot_hom_class.has_sizeof_inst
• inf_top_hom_class.has_sizeof_inst
• lattice_hom_class.has_sizeof_inst
• bounded_lattice_hom_class.has_sizeof_inst
• smul_with_zero.has_sizeof_inst
• mul_action_with_zero.has_sizeof_inst
• tactic.abel.normalize_mode.has_sizeof_inst
• module.has_sizeof_inst
• module.core.has_sizeof_inst
• ring_equiv.has_sizeof_inst
• ring_equiv_class.has_sizeof_inst
• mul_semiring_action.has_sizeof_inst
• mul_action_hom.has_sizeof_inst
• smul_hom_class.has_sizeof_inst
• distrib_mul_action_hom.has_sizeof_inst
• distrib_mul_action_hom_class.has_sizeof_inst
• mul_semiring_action_hom.has_sizeof_inst
• mul_semiring_action_hom_class.has_sizeof_inst
• set_like.has_sizeof_inst
• has_star.has_sizeof_inst
• star_mem_class.has_sizeof_inst
• has_involutive_star.has_sizeof_inst
• star_semigroup.has_sizeof_inst
• star_ring.has_sizeof_inst
• star_hom_class.has_sizeof_inst
• linear_map.has_sizeof_inst
• semilinear_map_class.has_sizeof_inst
• linear_map.compatible_smul.has_sizeof_inst
• linear_equiv.has_sizeof_inst
• semilinear_equiv_class.has_sizeof_inst
• normalization_monoid.has_sizeof_inst
• gcd_monoid.has_sizeof_inst
• normalized_gcd_monoid.has_sizeof_inst
• subsemigroup.has_sizeof_inst
• submonoid.has_sizeof_inst
• encodable.has_sizeof_inst
• subgroup.has_sizeof_inst
• smul_mem_class.has_sizeof_inst
• sub_mul_action.has_sizeof_inst
• submodule.has_sizeof_inst
• dfinsupp.has_sizeof_inst
• conditionally_complete_lattice.has_sizeof_inst
• conditionally_complete_linear_order.has_sizeof_inst
• conditionally_complete_linear_order_bot.has_sizeof_inst
• finsupp.has_sizeof_inst
• absolute_value.has_sizeof_inst
• subsemiring.has_sizeof_inst
• subring.has_sizeof_inst
• algebra.has_sizeof_inst
• alg_hom.has_sizeof_inst
• alg_hom_class.has_sizeof_inst
• alg_equiv.has_sizeof_inst
• alg_equiv_class.has_sizeof_inst
• non_unital_alg_hom.has_sizeof_inst
• non_unital_alg_hom_class.has_sizeof_inst
• locally_finite_order.has_sizeof_inst
• locally_finite_order_top.has_sizeof_inst
• locally_finite_order_bot.has_sizeof_inst
• denumerable.has_sizeof_inst
• flag.has_sizeof_inst
• tactic.tfae.arrow.has_sizeof_inst
• part.has_sizeof_inst
• omega_complete_partial_order.has_sizeof_inst
• omega_complete_partial_order.continuous_hom.has_sizeof_inst
• polynomial.has_sizeof_inst
• tactic.ring.normalize_mode.has_sizeof_inst
• tactic.ring.ring_nf_cfg.has_sizeof_inst
• linarith.ineq.has_sizeof_inst
• linarith.comp.has_sizeof_inst
• linarith.comp_source.has_sizeof_inst
• pos_num.has_sizeof_inst
• num.has_sizeof_inst
• znum.has_sizeof_inst
• tree.has_sizeof_inst
• con.has_sizeof_inst
• tensor_product.compatible_smul.has_sizeof_inst
• Sup_hom.has_sizeof_inst
• Inf_hom.has_sizeof_inst
• frame_hom.has_sizeof_inst
• complete_lattice_hom.has_sizeof_inst
• Sup_hom_class.has_sizeof_inst
• Inf_hom_class.has_sizeof_inst
• frame_hom_class.has_sizeof_inst
• complete_lattice_hom_class.has_sizeof_inst
• idem_semiring.has_sizeof_inst
• idem_comm_semiring.has_sizeof_inst
• has_kstar.has_sizeof_inst
• kleene_algebra.has_sizeof_inst
• succ_order.has_sizeof_inst
• pred_order.has_sizeof_inst
• linear_pmap.has_sizeof_inst
• has_quotient.has_sizeof_inst
• has_bracket.has_sizeof_inst
• basis.has_sizeof_inst
• subalgebra.has_sizeof_inst
• valuation.has_sizeof_inst
• valuation_class.has_sizeof_inst
• submonoid.localization_map.has_sizeof_inst
• submonoid.localization_with_zero_map.has_sizeof_inst
• tactic.ring_exp.coeff.has_sizeof_inst
• tactic.ring_exp.ex_type.has_sizeof_inst
• euclidean_domain.has_sizeof_inst
• ring_con.has_sizeof_inst
• initial_seg.has_sizeof_inst
• principal_seg.has_sizeof_inst
• Well_order.has_sizeof_inst
• pequiv.has_sizeof_inst
• composition.has_sizeof_inst
• composition_as_set.has_sizeof_inst
• nat.partition.has_sizeof_inst
• multilinear_map.has_sizeof_inst
• alternating_map.has_sizeof_inst
• subfield.has_sizeof_inst
• intermediate_field.has_sizeof_inst
• perfect_ring.has_sizeof_inst
• free_algebra.pre.has_sizeof_inst
• power_basis.has_sizeof_inst
• floor_semiring.has_sizeof_inst
• floor_ring.has_sizeof_inst
• intermediate_field.insert.has_sizeof_inst
• lift.subfield_with_hom.has_sizeof_inst
• star_ordered_ring.has_sizeof_inst
• filter.has_sizeof_inst
• filter_basis.has_sizeof_inst
• filter.countable_filter_basis.has_sizeof_inst
• tactic.decl_reducibility.has_sizeof_inst
• ultrafilter.has_sizeof_inst
• topological_space.has_sizeof_inst
• bornology.has_sizeof_inst
• upper_set.has_sizeof_inst
• lower_set.has_sizeof_inst
• compact_exhaustion.has_sizeof_inst
• homeomorph.has_sizeof_inst
• uniform_space.core.has_sizeof_inst
• uniform_space.has_sizeof_inst
• uniform_equiv.has_sizeof_inst
• continuous_map.has_sizeof_inst
• continuous_map_class.has_sizeof_inst
• group_topology.has_sizeof_inst
• ring_topology.has_sizeof_inst
• canonically_linear_ordered_semifield.has_sizeof_inst
• real.has_sizeof_inst
• has_edist.has_sizeof_inst
• pseudo_emetric_space.has_sizeof_inst
• emetric_space.has_sizeof_inst
• has_dist.has_sizeof_inst
• pseudo_metric_space.has_sizeof_inst
• has_nndist.has_sizeof_inst
• metric_space.has_sizeof_inst
• abstract_completion.has_sizeof_inst
• complex.has_sizeof_inst
• group_seminorm.has_sizeof_inst
• group_norm.has_sizeof_inst
• locally_bounded_map.has_sizeof_inst
• locally_bounded_map_class.has_sizeof_inst
• isometry_equiv.has_sizeof_inst
• has_norm.has_sizeof_inst
• has_nnnorm.has_sizeof_inst
• seminormed_group.has_sizeof_inst
• normed_group.has_sizeof_inst
• seminormed_comm_group.has_sizeof_inst
• normed_comm_group.has_sizeof_inst
• non_unital_semi_normed_ring.has_sizeof_inst
• semi_normed_ring.has_sizeof_inst
• non_unital_normed_ring.has_sizeof_inst
• normed_ring.has_sizeof_inst
• normed_division_ring.has_sizeof_inst
• semi_normed_comm_ring.has_sizeof_inst
• normed_comm_ring.has_sizeof_inst
• normed_field.has_sizeof_inst
• nontrivially_normed_field.has_sizeof_inst
• densely_normed_field.has_sizeof_inst
• continuous_linear_map.has_sizeof_inst
• continuous_semilinear_map_class.has_sizeof_inst
• continuous_linear_equiv.has_sizeof_inst
• continuous_semilinear_equiv_class.has_sizeof_inst
• normed_space.has_sizeof_inst
• normed_algebra.has_sizeof_inst
• linear_isometry.has_sizeof_inst
• semilinear_isometry_class.has_sizeof_inst
• linear_isometry_equiv.has_sizeof_inst
• semilinear_isometry_equiv_class.has_sizeof_inst
• non_unital_star_alg_hom.has_sizeof_inst
• non_unital_star_alg_hom_class.has_sizeof_inst
• star_alg_hom.has_sizeof_inst
• star_alg_hom_class.has_sizeof_inst
• star_alg_equiv.has_sizeof_inst
• star_alg_equiv_class.has_sizeof_inst
• star_subalgebra.has_sizeof_inst
• is_R_or_C.has_sizeof_inst
• measurable_space.has_sizeof_inst
• measurable_space.dynkin_system.has_sizeof_inst
• measure_theory.outer_measure.has_sizeof_inst
• measure_theory.measure.has_sizeof_inst
• measure_theory.measure_space.has_sizeof_inst
• measurable_equiv.has_sizeof_inst
• measure_theory.measure.finite_spanning_sets_in.has_sizeof_inst
• has_measurable_pow.has_sizeof_inst
• sign_type.has_sizeof_inst
• topological_lattice.has_sizeof_inst
• matrix.transvection_struct.has_sizeof_inst
• measure_theory.simple_func.has_sizeof_inst
• cocompact_map.has_sizeof_inst
• cocompact_map_class.has_sizeof_inst
• stieltjes_function.has_sizeof_inst
• topological_space.opens.has_sizeof_inst
• topological_space.open_nhds_of.has_sizeof_inst
• topological_space.closeds.has_sizeof_inst
• topological_space.clopens.has_sizeof_inst
• topological_space.compacts.has_sizeof_inst
• topological_space.nonempty_compacts.has_sizeof_inst
• topological_space.positive_compacts.has_sizeof_inst
• topological_space.compact_opens.has_sizeof_inst
• measure_theory.content.has_sizeof_inst
• divisible_by.has_sizeof_inst
• rootable_by.has_sizeof_inst
• direct_sum.decomposition.has_sizeof_inst
• affine_map.has_sizeof_inst
• affine_equiv.has_sizeof_inst
• affine_subspace.has_sizeof_inst
• bilin_form.has_sizeof_inst
• closure_operator.has_sizeof_inst
• affine.simplex.has_sizeof_inst
• affine_basis.has_sizeof_inst
• path.has_sizeof_inst
• normed_ordered_group.has_sizeof_inst
• normed_linear_ordered_group.has_sizeof_inst
• normed_linear_ordered_field.has_sizeof_inst
• affine_isometry.has_sizeof_inst
• affine_isometry_equiv.has_sizeof_inst
• local_equiv.has_sizeof_inst
• local_homeomorph.has_sizeof_inst
• seminorm.has_sizeof_inst
• seminorm_class.has_sizeof_inst
• group_filter_basis.has_sizeof_inst
• ring_filter_basis.has_sizeof_inst
• module_filter_basis.has_sizeof_inst
• continuous_multilinear_map.has_sizeof_inst
• has_inner.has_sizeof_inst
• inner_product_space.has_sizeof_inst
• inner_product_space.core.has_sizeof_inst
• continuous_linear_map.nonlinear_right_inverse.has_sizeof_inst
• bifunctor.has_sizeof_inst
• is_lawful_bifunctor.has_sizeof_inst
• jordan_holder_lattice.has_sizeof_inst
• composition_series.has_sizeof_inst
• has_btw.has_sizeof_inst
• has_sbtw.has_sizeof_inst
• circular_preorder.has_sizeof_inst
• circular_partial_order.has_sizeof_inst
• circular_order.has_sizeof_inst
• orthonormal_basis.has_sizeof_inst
• box_integral.box.has_sizeof_inst
• box_integral.prepartition.has_sizeof_inst
• box_integral.tagged_prepartition.has_sizeof_inst
• box_integral.integration_params.has_sizeof_inst
• urysohns.CU.has_sizeof_inst
• bounded_continuous_function.has_sizeof_inst
• bounded_continuous_map_class.has_sizeof_inst
• convex_cone.has_sizeof_inst
• hahn_series.has_sizeof_inst
• hahn_series.summable_family.has_sizeof_inst
• ratfunc.has_sizeof_inst
• open_subgroup.has_sizeof_inst
• quiver.has_sizeof_inst
• prefunctor.has_sizeof_inst
• category_theory.category_struct.has_sizeof_inst
• category_theory.category.has_sizeof_inst
• lazy_list.has_sizeof_inst
• writer_t.has_sizeof_inst
• uliftable.has_sizeof_inst
• bounded_random.has_sizeof_inst
• random.has_sizeof_inst
• slim_check.sampleable.has_sizeof_inst
• slim_check.sampleable_functor.has_sizeof_inst
• slim_check.sampleable_bifunctor.has_sizeof_inst
• slim_check.sampleable_ext.has_sizeof_inst
• slim_check.test_result.has_sizeof_inst
• slim_check.slim_check_cfg.has_sizeof_inst
• slim_check.printable_prop.has_sizeof_inst
• slim_check.testable.has_sizeof_inst
• parse_result.has_sizeof_inst
• polyrith.poly.has_sizeof_inst
• polyrith.sage_json_success.has_sizeof_inst
• polyrith.sage_json_failure.has_sizeof_inst
• has_variable_names.has_sizeof_inst
• tactic.eliminate.generalization_mode.has_sizeof_inst
• nzsnum.has_sizeof_inst
• snum.has_sizeof_inst
• tactic.ring2.csring_expr.has_sizeof_inst
• tactic.ring2.horner_expr.has_sizeof_inst
• omega.ee.has_sizeof_inst
• omega.ee_state.has_sizeof_inst
• omega.int.preterm.has_sizeof_inst
• omega.int.preform.has_sizeof_inst
• omega.nat.preterm.has_sizeof_inst
• omega.nat.preform.has_sizeof_inst
• category_theory.functor.has_sizeof_inst
• category_theory.nat_trans.has_sizeof_inst
• category_theory.iso.has_sizeof_inst
• category_theory.full.has_sizeof_inst
• category_theory.full_subcategory.has_sizeof_inst
• category_theory.equivalence.has_sizeof_inst
• category_theory.is_equivalence.has_sizeof_inst
• quiver.total.has_sizeof_inst
• quiver.path.has_sizeof_inst
• quiver.push_quiver.has_sizeof_inst
• quiver.has_reverse.has_sizeof_inst
• quiver.has_involutive_reverse.has_sizeof_inst
• prefunctor.map_reverse.has_sizeof_inst
• category_theory.groupoid.has_sizeof_inst
• category_theory.split_mono.has_sizeof_inst
• category_theory.split_epi.has_sizeof_inst
• category_theory.split_mono_category.has_sizeof_inst
• category_theory.split_epi_category.has_sizeof_inst
• category_theory.comma.has_sizeof_inst
• category_theory.comma_morphism.has_sizeof_inst
• category_theory.comm_sq.lift_struct.has_sizeof_inst
• category_theory.discrete.has_sizeof_inst
• category_theory.limits.cone.has_sizeof_inst
• category_theory.limits.cocone.has_sizeof_inst
• category_theory.limits.cone_morphism.has_sizeof_inst
• category_theory.limits.cocone_morphism.has_sizeof_inst
• category_theory.limits.is_limit.has_sizeof_inst
• category_theory.limits.is_colimit.has_sizeof_inst
• category_theory.limits.limit_cone.has_sizeof_inst
• category_theory.limits.colimit_cocone.has_sizeof_inst
• category_theory.limits.wide_pullback_shape.hom.has_sizeof_inst
• category_theory.limits.wide_pushout_shape.hom.has_sizeof_inst
• category_theory.bundled.has_sizeof_inst
• category_theory.bicategory.has_sizeof_inst
• category_theory.is_skeleton_of.has_sizeof_inst
• category_theory.limits.walking_pair.has_sizeof_inst
• category_theory.limits.preserves_limit.has_sizeof_inst
• category_theory.limits.preserves_colimit.has_sizeof_inst
• category_theory.limits.preserves_limits_of_shape.has_sizeof_inst
• category_theory.limits.preserves_colimits_of_shape.has_sizeof_inst
• category_theory.limits.preserves_limits_of_size.has_sizeof_inst
• category_theory.limits.preserves_colimits_of_size.has_sizeof_inst
• category_theory.limits.reflects_limit.has_sizeof_inst
• category_theory.limits.reflects_colimit.has_sizeof_inst
• category_theory.limits.reflects_limits_of_shape.has_sizeof_inst
• category_theory.limits.reflects_colimits_of_shape.has_sizeof_inst
• category_theory.limits.reflects_limits_of_size.has_sizeof_inst
• category_theory.limits.reflects_colimits_of_size.has_sizeof_inst
• category_theory.concrete_category.has_sizeof_inst
• category_theory.has_forget₂.has_sizeof_inst
• tactic.rewrite_search.side.has_sizeof_inst
• tactic.rewrite_search.dir_pair.has_sizeof_inst
• tactic.rewrite_search.using_conv.splice_result.has_sizeof_inst
• side.has_sizeof_inst
• measure_theory.vector_measure.has_sizeof_inst
• measure_theory.jordan_decomposition.has_sizeof_inst
• measure_theory.filtration.has_sizeof_inst
• category_theory.bundled_hom.has_sizeof_inst
• category_theory.bundled_hom.parent_projection.has_sizeof_inst
• category_theory.liftable_cone.has_sizeof_inst
• category_theory.liftable_cocone.has_sizeof_inst
• category_theory.creates_limit.has_sizeof_inst
• category_theory.creates_limits_of_shape.has_sizeof_inst
• category_theory.creates_limits_of_size.has_sizeof_inst
• category_theory.creates_colimit.has_sizeof_inst
• category_theory.creates_colimits_of_shape.has_sizeof_inst
• category_theory.creates_colimits_of_size.has_sizeof_inst
• category_theory.lifts_to_limit.has_sizeof_inst
• category_theory.lifts_to_colimit.has_sizeof_inst
• category_theory.monoidal_category.has_sizeof_inst
• category_theory.lax_monoidal_functor.has_sizeof_inst
• category_theory.monoidal_functor.has_sizeof_inst
• category_theory.free_monoidal_category.has_sizeof_inst
• category_theory.free_monoidal_category.hom.has_sizeof_inst
• category_theory.free_monoidal_category.normal_monoidal_object.has_sizeof_inst
• category_theory.quotient.has_sizeof_inst
• category_theory.prelax_functor.has_sizeof_inst
• category_theory.oplax_functor.has_sizeof_inst
• category_theory.oplax_functor.pseudo_core.has_sizeof_inst
• category_theory.pseudofunctor.has_sizeof_inst
• category_theory.free_bicategory.hom.has_sizeof_inst
• category_theory.free_bicategory.hom₂.has_sizeof_inst
• category_theory.bicategory.lift_hom.has_sizeof_inst
• category_theory.bicategory.lift_hom₂.has_sizeof_inst
• category_theory.bicategory.bicategorical_coherence.has_sizeof_inst
• category_theory.monoidal_category.lift_obj.has_sizeof_inst
• category_theory.monoidal_category.lift_hom.has_sizeof_inst
• category_theory.monoidal_category.monoidal_coherence.has_sizeof_inst
• category_theory.monoidal_nat_trans.has_sizeof_inst
• category_theory.braided_category.has_sizeof_inst
• category_theory.symmetric_category.has_sizeof_inst
• category_theory.lax_braided_functor.has_sizeof_inst
• category_theory.braided_functor.has_sizeof_inst
• category_theory.closed.has_sizeof_inst
• category_theory.monoidal_closed.has_sizeof_inst
• category_theory.exact_pairing.has_sizeof_inst
• category_theory.has_right_dual.has_sizeof_inst
• category_theory.has_left_dual.has_sizeof_inst
• category_theory.right_rigid_category.has_sizeof_inst
• category_theory.left_rigid_category.has_sizeof_inst
• category_theory.rigid_category.has_sizeof_inst
• category_theory.fin_category.has_sizeof_inst
• category_theory.limits.preserves_finite_limits.has_sizeof_inst
• category_theory.limits.preserves_finite_colimits.has_sizeof_inst
• category_theory.limits.walking_parallel_pair.has_sizeof_inst
• category_theory.limits.walking_parallel_pair_hom.has_sizeof_inst
• category_theory.limits.mono_factorisation.has_sizeof_inst
• category_theory.limits.is_image.has_sizeof_inst
• category_theory.limits.image_factorisation.has_sizeof_inst
• category_theory.limits.image_map.has_sizeof_inst
• category_theory.limits.has_image_maps.has_sizeof_inst
• category_theory.limits.strong_epi_mono_factorisation.has_sizeof_inst
• category_theory.limits.has_zero_morphisms.has_sizeof_inst
• category_theory.limits.bicone.has_sizeof_inst
• category_theory.limits.bicone.is_bilimit.has_sizeof_inst
• category_theory.limits.limit_bicone.has_sizeof_inst
• category_theory.limits.binary_bicone.has_sizeof_inst
• category_theory.limits.binary_bicone.is_bilimit.has_sizeof_inst
• category_theory.limits.binary_biproduct_data.has_sizeof_inst
• category_theory.limits.preserves_biproduct.has_sizeof_inst
• category_theory.limits.preserves_biproducts_of_shape.has_sizeof_inst
• category_theory.limits.preserves_finite_biproducts.has_sizeof_inst
• category_theory.limits.preserves_biproducts.has_sizeof_inst
• category_theory.limits.preserves_binary_biproduct.has_sizeof_inst
• category_theory.limits.preserves_binary_biproducts.has_sizeof_inst
• category_theory.linear.has_sizeof_inst
• category_theory.is_split_coequalizer.has_sizeof_inst
• category_theory.regular_mono.has_sizeof_inst
• category_theory.regular_mono_category.has_sizeof_inst
• category_theory.regular_epi.has_sizeof_inst
• category_theory.regular_epi_category.has_sizeof_inst
• category_theory.normal_mono.has_sizeof_inst
• category_theory.normal_mono_category.has_sizeof_inst
• category_theory.normal_epi.has_sizeof_inst
• category_theory.normal_epi_category.has_sizeof_inst
• category_theory.abelian.has_sizeof_inst
• Action.has_sizeof_inst
• Action.hom.has_sizeof_inst
• Module.has_sizeof_inst
• category_theory.reflective.has_sizeof_inst
• category_theory.functor.reflects_exact_sequences.has_sizeof_inst
• Module.colimits.prequotient.has_sizeof_inst
• category_theory.functorial.has_sizeof_inst
• category_theory.lax_monoidal.has_sizeof_inst
• category_theory.projective_presentation.has_sizeof_inst
• complex_shape.has_sizeof_inst
• category_theory.has_shift.has_sizeof_inst
• category_theory.shift_mk_core.has_sizeof_inst
• homological_complex.has_sizeof_inst
• homological_complex.hom.has_sizeof_inst
• chain_complex.mk_struct.has_sizeof_inst
• cochain_complex.mk_struct.has_sizeof_inst
• FinPartOrd.has_sizeof_inst
• nonempty_fin_lin_ord.has_sizeof_inst
• category_theory.idempotents.karoubi.has_sizeof_inst
• category_theory.idempotents.karoubi.hom.has_sizeof_inst
• category_theory.limits.walking_multicospan.has_sizeof_inst
• category_theory.limits.walking_multispan.has_sizeof_inst
• category_theory.limits.walking_multicospan.hom.has_sizeof_inst
• category_theory.limits.walking_multispan.hom.has_sizeof_inst
• category_theory.limits.multicospan_index.has_sizeof_inst
• category_theory.limits.multispan_index.has_sizeof_inst
• homotopy.has_sizeof_inst
• homotopy_equiv.has_sizeof_inst
• simplicial_object.augmented.extra_degeneracy.has_sizeof_inst
• category_theory.ProjectiveResolution.has_sizeof_inst
• Group.surjective_of_epi_auxs.X_with_infinity.has_sizeof_inst
• vitali_family.has_sizeof_inst
• besicovitch.satellite_config.has_sizeof_inst
• besicovitch.ball_package.has_sizeof_inst
• besicovitch.tau_package.has_sizeof_inst
• is_unif_loc_doubling_measure.has_sizeof_inst
• module.oriented.has_sizeof_inst
• category_theory.unbundled_hom.has_sizeof_inst
• continuous_affine_map.has_sizeof_inst
• shrinking_lemma.partial_refinement.has_sizeof_inst
• partition_of_unity.has_sizeof_inst
• bump_covering.has_sizeof_inst
• bundle.total_space.has_sizeof_inst
• pretrivialization.has_sizeof_inst
• trivialization.has_sizeof_inst
• fiber_bundle.has_sizeof_inst
• fiber_bundle_core.has_sizeof_inst
• fiber_prebundle.has_sizeof_inst
• category_theory.glue_data.has_sizeof_inst
• Top.glue_data.has_sizeof_inst
• Top.glue_data.mk_core.has_sizeof_inst
• locally_constant.has_sizeof_inst
• discrete_quotient.has_sizeof_inst
• spectral_map.has_sizeof_inst
• spectral_map_class.has_sizeof_inst
• clopen_upper_set.has_sizeof_inst
• Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
• dilation.has_sizeof_inst
• dilation_class.has_sizeof_inst
• vector_bundle_core.has_sizeof_inst
• vector_prebundle.has_sizeof_inst
• continuous_map.homotopy.has_sizeof_inst
• continuous_map.homotopy_like.has_sizeof_inst
• continuous_map.homotopy_with.has_sizeof_inst
• continuous_map.homotopy_equiv.has_sizeof_inst
• H_space.has_sizeof_inst
• priestley_space.has_sizeof_inst
• continuous_order_hom.has_sizeof_inst
• continuous_order_hom_class.has_sizeof_inst
• pseudo_epimorphism.has_sizeof_inst
• esakia_hom.has_sizeof_inst
• pseudo_epimorphism_class.has_sizeof_inst
• esakia_hom_class.has_sizeof_inst
• continuous_open_map.has_sizeof_inst
• continuous_open_map_class.has_sizeof_inst
• CpltSepUniformSpace.has_sizeof_inst
• TopCommRing.has_sizeof_inst
• CompHaus.has_sizeof_inst
• Profinite.has_sizeof_inst
• valued.has_sizeof_inst
• continuous_monoid_hom.has_sizeof_inst
• continuous_monoid_hom_class.has_sizeof_inst
• with_ideal.has_sizeof_inst
• derivation.has_sizeof_inst
• zero_at_infty_continuous_map.has_sizeof_inst
• zero_at_infty_continuous_map_class.has_sizeof_inst
• category_theory.presieve.functor_pushforward_structure.has_sizeof_inst
• category_theory.sieve.has_sizeof_inst
• category_theory.grothendieck_topology.has_sizeof_inst
• category_theory.grothendieck_topology.cover.arrow.has_sizeof_inst
• category_theory.grothendieck_topology.cover.relation.has_sizeof_inst
• category_theory.pretopology.has_sizeof_inst
• category_theory.SheafOfTypes.has_sizeof_inst
• category_theory.SheafOfTypes.hom.has_sizeof_inst
• category_theory.Sheaf.has_sizeof_inst
• category_theory.Sheaf.hom.has_sizeof_inst
• category_theory.limits.preserves_filtered_colimits.has_sizeof_inst
• category_theory.limits.preserves_cofiltered_limits.has_sizeof_inst
• category_theory.bicone.has_sizeof_inst
• category_theory.bicone_hom.has_sizeof_inst
• category_theory.presieve.cover_by_image_structure.has_sizeof_inst
• category_theory.pairwise.has_sizeof_inst
• category_theory.pairwise.hom.has_sizeof_inst
• CommRing.colimits.prequotient.has_sizeof_inst
• Top.presheaf.submonoid_presheaf.has_sizeof_inst
• Top.prelocal_predicate.has_sizeof_inst
• Top.local_predicate.has_sizeof_inst
• category_theory.grothendieck_topology.subpresheaf.has_sizeof_inst
• category_theory.grothendieck.has_sizeof_inst
• category_theory.grothendieck.hom.has_sizeof_inst
• category_theory.with_terminal.has_sizeof_inst
• category_theory.with_initial.has_sizeof_inst
• category_theory.differential_object.has_sizeof_inst
• category_theory.differential_object.hom.has_sizeof_inst
• category_theory.noetherian.has_sizeof_inst
• category_theory.artinian.has_sizeof_inst
• semidirect_product.has_sizeof_inst
• category_theory.sigma.sigma_hom.has_sizeof_inst
• category_theory.injective_presentation.has_sizeof_inst
• category_theory.InjectiveResolution.has_sizeof_inst
• category_theory.cartesian_closed_functor.has_sizeof_inst
• category_theory.oplax_nat_trans.has_sizeof_inst
• category_theory.oplax_nat_trans.modification.has_sizeof_inst
• category_theory.endofunctor.algebra.has_sizeof_inst
• category_theory.endofunctor.algebra.hom.has_sizeof_inst
• category_theory.endofunctor.coalgebra.has_sizeof_inst
• category_theory.endofunctor.coalgebra.hom.has_sizeof_inst
• category_theory.subgroupoid.has_sizeof_inst
• category_theory.limits.diagram_of_cones.has_sizeof_inst
• category_theory.limits.walking_parallel_family.has_sizeof_inst
• category_theory.limits.walking_parallel_family.hom.has_sizeof_inst
• category_theory.limits.coproduct_disjoint.has_sizeof_inst
• category_theory.limits.coproducts_disjoint.has_sizeof_inst
• category_theory.Mat_.has_sizeof_inst
• Pointed.has_sizeof_inst
• Pointed.hom.has_sizeof_inst
• Bipointed.has_sizeof_inst
• Bipointed.hom.has_sizeof_inst
• two_pointing.has_sizeof_inst
• Twop.has_sizeof_inst
• category_theory.localization.construction.loc_quiver.has_sizeof_inst
• category_theory.localization.strict_universal_property_fixed_target.has_sizeof_inst
• category_theory.localization.lifting.has_sizeof_inst
• category_theory.pretriangulated.triangle.has_sizeof_inst
• category_theory.pretriangulated.triangle_morphism.has_sizeof_inst
• category_theory.pretriangulated.has_sizeof_inst
• category_theory.triangulated.octahedron.has_sizeof_inst
• category_theory.is_triangulated.has_sizeof_inst
• Mon_.has_sizeof_inst
• Mon_.hom.has_sizeof_inst
• Bimod.has_sizeof_inst
• Bimod.hom.has_sizeof_inst
• Mod_.has_sizeof_inst
• Mod_.hom.has_sizeof_inst
• category_theory.half_braiding.has_sizeof_inst
• category_theory.center.hom.has_sizeof_inst
• CommMon_.has_sizeof_inst
• Algebra.has_sizeof_inst
• category_theory.enriched_category.has_sizeof_inst
• category_theory.enriched_functor.has_sizeof_inst
• flow.has_sizeof_inst
• circle_deg1_lift.has_sizeof_inst
• has_fix.has_sizeof_inst
• lawful_fix.has_sizeof_inst
• fin2.has_sizeof_inst
• fin2.is_lt.has_sizeof_inst
• mvfunctor.has_sizeof_inst
• bitraversable.has_sizeof_inst
• is_lawful_bitraversable.has_sizeof_inst
• schwartz_map.has_sizeof_inst
• cont_diff_bump.has_sizeof_inst
• cont_diff_bump_base.has_sizeof_inst
• quaternion_algebra.has_sizeof_inst
• hilbert_basis.has_sizeof_inst
• implicit_function_data.has_sizeof_inst
• picard_lindelof.has_sizeof_inst
• picard_lindelof.fun_space.has_sizeof_inst
• wstar_algebra.has_sizeof_inst
• von_neumann_algebra.has_sizeof_inst
• enorm.has_sizeof_inst
• double_centralizer.has_sizeof_inst
• ring_seminorm.has_sizeof_inst
• ring_norm.has_sizeof_inst
• mul_ring_seminorm.has_sizeof_inst
• mul_ring_norm.has_sizeof_inst
• structure_groupoid.has_sizeof_inst
• pregroupoid.has_sizeof_inst
• charted_space.has_sizeof_inst
• charted_space_core.has_sizeof_inst
• structomorph.has_sizeof_inst
• model_with_corners.has_sizeof_inst
• convex_body.has_sizeof_inst
• geometry.simplicial_complex.has_sizeof_inst
• proper_cone.has_sizeof_inst
• ring_invo.has_sizeof_inst
• ring_invo_class.has_sizeof_inst
• prime_spectrum.has_sizeof_inst
• basis.smith_normal_form.has_sizeof_inst
• maximal_spectrum.has_sizeof_inst
• is_dedekind_domain.height_one_spectrum.has_sizeof_inst
• ideal.filtration.has_sizeof_inst
• non_unital_subsemiring_class.has_sizeof_inst
• non_unital_subsemiring.has_sizeof_inst
• direct_sum.gnon_unital_non_assoc_semiring.has_sizeof_inst
• direct_sum.gsemiring.has_sizeof_inst
• direct_sum.gcomm_semiring.has_sizeof_inst
• direct_sum.gring.has_sizeof_inst
• direct_sum.gcomm_ring.has_sizeof_inst
• direct_sum.galgebra.has_sizeof_inst
• homogeneous_ideal.has_sizeof_inst
• homogeneous_localization.num_denom_same_deg.has_sizeof_inst
• ore_localization.ore_set.has_sizeof_inst
• witt_vector.has_sizeof_inst
• witt_vector.isocrystal.has_sizeof_inst
• witt_vector.isocrystal_hom.has_sizeof_inst
• witt_vector.isocrystal_equiv.has_sizeof_inst
• valuation_subring.has_sizeof_inst
• lie_ring.has_sizeof_inst
• lie_algebra.has_sizeof_inst
• lie_ring_module.has_sizeof_inst
• lie_module.has_sizeof_inst
• lie_hom.has_sizeof_inst
• lie_equiv.has_sizeof_inst
• lie_module_hom.has_sizeof_inst
• lie_module_equiv.has_sizeof_inst
• lie_subalgebra.has_sizeof_inst
• lie_submodule.has_sizeof_inst
• nonempty_interval.has_sizeof_inst
• order.ideal.has_sizeof_inst
• order.cofinal.has_sizeof_inst
• order.pfilter.has_sizeof_inst
• order.ideal.prime_pair.has_sizeof_inst
• concept.has_sizeof_inst
• finpartition.has_sizeof_inst
• heyting_hom.has_sizeof_inst
• coheyting_hom.has_sizeof_inst
• biheyting_hom.has_sizeof_inst
• heyting_hom_class.has_sizeof_inst
• coheyting_hom_class.has_sizeof_inst
• biheyting_hom_class.has_sizeof_inst
• BddOrd.has_sizeof_inst
• SemilatSup.has_sizeof_inst
• SemilatInf.has_sizeof_inst
• BddLat.has_sizeof_inst
• BddDistLat.has_sizeof_inst
• FinBddDistLat.has_sizeof_inst
• FinBoolAlg.has_sizeof_inst
• simplicial_object.splitting.has_sizeof_inst
• simplicial_object.split.has_sizeof_inst
• simplicial_object.split.hom.has_sizeof_inst
• algebraic_topology.dold_kan.morph_components.has_sizeof_inst
• generalized_continued_fraction.pair.has_sizeof_inst
• generalized_continued_fraction.has_sizeof_inst
• generalized_continued_fraction.int_fract_pair.has_sizeof_inst
• zsqrtd.has_sizeof_inst
• mul_char.has_sizeof_inst
• mul_char_class.has_sizeof_inst
• slash_action.has_sizeof_inst
• slash_invariant_form.has_sizeof_inst
• slash_invariant_form_class.has_sizeof_inst
• modular_form.has_sizeof_inst
• cusp_form.has_sizeof_inst
• modular_form_class.has_sizeof_inst
• cusp_form_class.has_sizeof_inst
• diffeomorph.has_sizeof_inst
• smooth_bump_function.has_sizeof_inst
• smooth_monoid_morphism.has_sizeof_inst
• smooth_bump_covering.has_sizeof_inst
• smooth_partition_of_unity.has_sizeof_inst
• cont_mdiff_section.has_sizeof_inst
• left_invariant_derivation.has_sizeof_inst
• euclidean_geometry.sphere.has_sizeof_inst
• affine.simplex.points_with_circumcenter_index.has_sizeof_inst
• lists'.has_sizeof_inst
• lists.has_sizeof
• pgame.has_sizeof_inst
• pgame.relabelling.has_sizeof_inst
• pgame.inv_ty.has_sizeof_inst
• order_monoid_hom.has_sizeof_inst
• order_monoid_hom_class.has_sizeof_inst
• order_monoid_with_zero_hom.has_sizeof_inst
• order_monoid_with_zero_hom_class.has_sizeof_inst
• pSet.has_sizeof_inst
• pSet.definable.has_sizeof_inst
• onote.has_sizeof_inst
• pgame.short.has_sizeof_inst
• pgame.list_short.has_sizeof_inst
• pgame.state.has_sizeof_inst
• ring_quot.has_sizeof_inst
• shelf.has_sizeof_inst
• unital_shelf.has_sizeof_inst
• shelf_hom.has_sizeof_inst
• rack.has_sizeof_inst
• quandle.has_sizeof_inst
• rack.pre_envel_group.has_sizeof_inst
• rack.pre_envel_group_rel'.has_sizeof_inst
• free_magma.has_sizeof_inst
• free_semigroup.has_sizeof_inst
• cubic.has_sizeof_inst
• linear_recurrence.has_sizeof_inst
• quaternion_algebra.basis.has_sizeof_inst
• is_jordan.has_sizeof_inst
• is_comm_jordan.has_sizeof_inst
• boolean_ring.has_sizeof_inst
• category_theory.splitting.has_sizeof_inst
• direct_sum.gdistrib_mul_action.has_sizeof_inst
• direct_sum.gmodule.has_sizeof_inst
• module.Baer.extension_of.has_sizeof_inst
• cartan_matrix.generators.has_sizeof_inst
• is_CHSH_tuple.has_sizeof_inst
• order_ring_hom.has_sizeof_inst
• order_ring_iso.has_sizeof_inst
• order_ring_hom_class.has_sizeof_inst
• order_ring_iso_class.has_sizeof_inst
• conditionally_complete_linear_ordered_field.has_sizeof_inst
• ring.positive_cone.has_sizeof_inst
• ring.total_positive_cone.has_sizeof_inst
• freiman_hom.has_sizeof_inst
• centroid_hom.has_sizeof_inst
• centroid_hom_class.has_sizeof_inst
• Mon.colimits.prequotient.has_sizeof_inst
• clifford_algebra.even_hom.has_sizeof_inst
• projectivization.subspace.has_sizeof_inst
• primcodable.has_sizeof_inst
• DFA.has_sizeof_inst
• NFA.has_sizeof_inst
• ε_NFA.has_sizeof_inst
• regular_expression.has_sizeof_inst
• nat.partrec.code.has_sizeof_inst
• turing.pointed_map.has_sizeof_inst
• turing.tape.has_sizeof_inst
• turing.dir.has_sizeof_inst
• turing.TM0.stmt.has_sizeof_inst
• turing.TM0.cfg.has_sizeof_inst
• turing.TM1.stmt.has_sizeof_inst
• turing.TM1.cfg.has_sizeof_inst
• turing.TM1to1.Λ'.has_sizeof_inst
• turing.TM0to1.Λ'.has_sizeof_inst
• turing.TM2.stmt.has_sizeof_inst
• turing.TM2.cfg.has_sizeof_inst
• turing.TM2to1.st_act.has_sizeof_inst
• turing.TM2to1.Λ'.has_sizeof_inst
• turing.to_partrec.code.has_sizeof_inst
• turing.to_partrec.cont.has_sizeof_inst
• turing.to_partrec.cfg.has_sizeof_inst
• turing.partrec_to_TM2.Γ'.has_sizeof_inst
• turing.partrec_to_TM2.K'.has_sizeof_inst
• turing.partrec_to_TM2.cont'.has_sizeof_inst
• turing.partrec_to_TM2.Λ'.has_sizeof_inst
• computability.encoding.has_sizeof_inst
• computability.fin_encoding.has_sizeof_inst
• computability.Γ'.has_sizeof_inst
• turing.fin_tm2.has_sizeof_inst
• turing.evals_to.has_sizeof_inst
• turing.evals_to_in_time.has_sizeof_inst
• turing.tm2_computable_aux.has_sizeof_inst
• turing.tm2_computable.has_sizeof_inst
• turing.tm2_computable_in_time.has_sizeof_inst
• turing.tm2_computable_in_poly_time.has_sizeof_inst
• slim_check.total_function.has_sizeof_inst
• slim_check.injective_function.has_sizeof_inst
• slim_check.injective_function.has_sizeof
• combinatorics.line.has_sizeof_inst
• combinatorics.line.almost_mono.has_sizeof_inst
• combinatorics.line.color_focused.has_sizeof_inst
• configuration.has_points.has_sizeof_inst
• configuration.has_lines.has_sizeof_inst
• configuration.projective_plane.has_sizeof_inst
• quiver.arborescence.has_sizeof_inst
• simple_graph.has_sizeof_inst
• simple_graph.dart.has_sizeof_inst
• indexed_partition.has_sizeof_inst
• simple_graph.partition.has_sizeof_inst
• simple_graph.subgraph.has_sizeof_inst
• simple_graph.walk.has_sizeof_inst
• has_sups.has_sizeof_inst
• has_infs.has_sizeof_inst
• young_diagram.has_sizeof_inst
• ssyt.has_sizeof_inst
• semiquot.has_sizeof_inst
• hash_map.has_sizeof_inst
• alist.has_sizeof_inst
• finmap.has_sizeof_inst
• fin_enum.has_sizeof_inst
• W_type.has_sizeof_inst
• W_type.nat_α.has_sizeof_inst
• W_type.list_α.has_sizeof_inst
• pfunctor.has_sizeof_inst
• mvpfunctor.has_sizeof_inst
• mvqpf.has_sizeof_inst
• pfunctor.approx.cofix_a.has_sizeof_inst
• pfunctor.M_intl.has_sizeof_inst
• mvpfunctor.M.path.has_sizeof_inst
• mvpfunctor.W_path.has_sizeof_inst
• qpf.has_sizeof_inst
• cfilter.has_sizeof_inst
• filter.realizer.has_sizeof_inst
• ctop.has_sizeof_inst
• ctop.realizer.has_sizeof_inst
• locally_finite.realizer.has_sizeof_inst
• pnat.xgcd_type.has_sizeof_inst
• pnat.xgcd_type.has_sizeof
• ordnode.has_sizeof_inst
• fp.rmode.has_sizeof_inst
• fp.float_cfg.has_sizeof_inst
• fp.float.has_sizeof_inst
• first_order.language.has_sizeof_inst
• first_order.language.Structure.has_sizeof_inst
• first_order.language.hom.has_sizeof_inst
• first_order.language.embedding.has_sizeof_inst
• first_order.language.equiv.has_sizeof_inst
• first_order.language.hom_class.has_sizeof_inst
• first_order.language.strong_hom_class.has_sizeof_inst
• first_order.language.Lhom.has_sizeof_inst
• first_order.language.Lequiv.has_sizeof_inst
• first_order.language.term.has_sizeof_inst
• first_order.language.bounded_formula.has_sizeof_inst
• first_order.language.substructure.has_sizeof_inst
• first_order.language.prestructure.has_sizeof_inst
• first_order.language.elementary_embedding.has_sizeof_inst
• first_order.language.elementary_substructure.has_sizeof_inst
• first_order.language.Theory.Model.has_sizeof_inst
• first_order.language.Theory.complete_type.has_sizeof_inst
• first_order.language.is_ordered.has_sizeof_inst
• algebraic_geometry.PresheafedSpace.has_sizeof_inst
• algebraic_geometry.PresheafedSpace.hom.has_sizeof_inst
• algebraic_geometry.SheafedSpace.has_sizeof_inst
• algebraic_geometry.LocallyRingedSpace.has_sizeof_inst
• algebraic_geometry.LocallyRingedSpace.hom.has_sizeof_inst
• algebraic_geometry.Scheme.has_sizeof_inst
• algebraic_geometry.PresheafedSpace.glue_data.has_sizeof_inst
• algebraic_geometry.SheafedSpace.glue_data.has_sizeof_inst
• algebraic_geometry.LocallyRingedSpace.glue_data.has_sizeof_inst
• algebraic_geometry.Scheme.open_cover.has_sizeof_inst
• algebraic_geometry.Scheme.glue_data.has_sizeof_inst
• projective_spectrum.has_sizeof_inst
• weierstrass_curve.has_sizeof_inst
• elliptic_curve.has_sizeof_inst
• weierstrass_curve.point.has_sizeof_inst
• sylow.has_sizeof_inst
• is_free_group.has_sizeof_inst
• is_free_groupoid.has_sizeof_inst
• free_product.word.has_sizeof_inst
• free_product.word.pair.has_sizeof_inst
• free_product.neword.has_sizeof_inst
• dihedral_group.has_sizeof_inst
• quaternion_group.has_sizeof_inst
• counterexample.F.has_sizeof_inst
• counterexample.foo.has_sizeof_inst
• arithcc.expr.has_sizeof_inst
• arithcc.instruction.has_sizeof_inst
• arithcc.state.has_sizeof_inst
• miu.miu_atom.has_sizeof_inst
• theorems_100.82.cube.has_sizeof_inst
• konigsberg.verts.has_sizeof_inst
• prop_encodable.prop_form.has_sizeof_inst
• imo2019_q2.imo2019q2_cfg.has_sizeof_inst
• module_doc_info.has_sizeof_inst
• ext_tactic_doc_entry.has_sizeof_inst
• slim_check.total_function.has_sizeof
def sizeof {α : Sort u} [s : has_sizeof α] :
α
Equations

Declare sizeof instances and lemmas for types declared before has_sizeof. From now on, the inductive compiler will automatically generate sizeof instances and lemmas.

@[protected]
def default.sizeof (α : Sort u) :
α

Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α`

Equations
• = 0
@[protected, instance]
def default_has_sizeof (α : Sort u) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof × β)
Equations
@[protected, instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof β)
Equations
@[protected, instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
Equations
@[protected, instance]
def sigma.has_sizeof (α : Type u) (β : α Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
• = {sizeof := sigma.sizeof (λ (a : α), _inst_2 a)}
@[protected, instance]
def psigma.has_sizeof (α : Type u) (β : α Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
• = {sizeof := psigma.sizeof (λ (a : α), _inst_2 a)}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[protected, instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[protected, instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α Prop) :
Equations
theorem nat_add_zero (n : ) :
n + 0 = n
inductive bin_tree (α : Type u) :

Auxiliary datatype for #[ ... ] notation. #[1, 2, 3, 4] is notation for

bin_tree.node (bin_tree.node (bin_tree.leaf 1) (bin_tree.leaf 2)) (bin_tree.node (bin_tree.leaf 3) (bin_tree.leaf 4))

We use this notation to input long sequences without exhausting the system stack space. Later, we define a coercion from `bin_tree` into `list`.

Instances for `bin_tree`
@[reducible]
def infer_instance {α : Sort u} [i : α] :
α

Like `by apply_instance`, but not dependent on the tactic framework.

Equations