core / init.core - mathlib docs

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

(id_delta t) =?= t
t =?= (id_delta t)
(id_delta t) =?= s IF (unfold_of t) =?= s
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.

source

def opt_param (α : Sort u) (default : α) :

Sort u

Gadget for optional parameter support.

source

def out_param (α : Sort u) :

Sort u

Gadget for marking output parameters in type classes.

source

def id_rhs (α : Sort u) (a : α) :

α

source

inductive punit :

Sort u

star : punit

Instances for punit

source

def unit :

Type

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

source

def unit.star :

unit

source

def thunk (α : Type u) :

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)

source

inductive true :

Prop

intro : true

Instances for true

source

inductive false :

Prop

Instances for false

source

inductive empty :

Type

Instances for empty

source

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

source

inductive eq {α : Sort u} (a : α) :

α → Prop

refl : ∀ {α : Sort u} (a : α), a = a

Instances for eq

source

inductive heq {α : Sort u} (a : α) {β : Sort u} :

β → Prop

refl : ∀ {α : Sort u} (a : α), a == a

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.

source

structure prod (α : Type u) (β : Type v) :

Type (max u v)

fst : α
snd : β

Instances for prod

source

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

source

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

source

theorem and.elim_left {a b : Prop} (h : a ∧ b) :

a

source

theorem and.elim_right {a b : Prop} (h : a ∧ b) :

b

source

@[nolint]

def rfl {α : Sort u} {a : α} :

a = a

source

theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :

P b

source

theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :

a = c

source

theorem eq.symm {α : Sort u} {a b : α} (h : a = b) :

b = a

source

def heq.rfl {α : Sort u} {a : α} :

a == a

source

theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') :

a = a'

source

inductive sum (α : Type u) (β : Type v) :

Type (max u v)

inl : Π {α : Type u} {β : Type v}, α → α ⊕ β
inr : Π {α : Type u} {β : Type v}, β → α ⊕ β

Instances for sum

source

inductive psum (α : Sort u) (β : Sort v) :

Sort (max 1 u v)

inl : Π {α : Sort u} {β : Sort v}, α → psum α β
inr : Π {α : Sort u} {β : Sort v}, β → psum α β

Instances for psum

source

inductive or (a b : Prop) :

Prop

inl : ∀ {a b : Prop}, a → a ∨ b
inr : ∀ {a b : Prop}, b → a ∨ b

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

source

theorem or.intro_left {a : Prop} (b : Prop) (ha : a) :

a ∨ b

source

theorem or.intro_right (a : Prop) {b : Prop} (hb : b) :

a ∨ b

source

structure sigma {α : Type u} (β : α → Type v) :

Type (max u v)

fst : α
snd : β self.fst

Instances for sigma

source

structure psigma {α : Sort u} (β : α → Sort v) :

Sort (max 1 u v)

fst : α
snd : β self.fst

Instances for psigma

source

inductive bool :

Type

ff : bool
tt : bool

Instances for bool

source

structure subtype {α : Sort u} (p : α → Prop) :

Sort (max 1 u)

val : α
property : p self.val

Instances for subtype

source

@[class]

inductive decidable (p : Prop) :

Type

is_false : Π {p : Prop}, ¬p → decidable p
is_true : Π {p : Prop}, p → decidable p

Instances of this typeclass

Instances of other typeclasses for decidable

source

def decidable_pred {α : Sort u} (r : α → Prop) :

Sort (max u 1)

Equations

decidable_pred r = Π (a : α), decidable (r a)

source

def decidable_rel {α : Sort u} (r : α → α → Prop) :

Sort (max u 1)

Equations

decidable_rel r = Π (a b : α), decidable (r a b)

source

def decidable_eq (α : Sort u) :

Sort (max u 1)

Equations

decidable_eq α = decidable_rel eq

source

inductive option (α : Type u) :

Type u

none : Π {α : Type u}, option α
some : Π {α : Type u}, α → option α

Instances for option

source

inductive list (T : Type u) :

Type u

nil : Π {T : Type u}, list T
cons : Π {T : Type u}, T → list T → list T

Instances for list

source

inductive nat :

Type

zero : ℕ
succ : ℕ → ℕ

Instances for nat

source

structure unification_constraint :

Type (u+1)

α : Type ?
lhs : self.α
rhs : self.α

Instances for unification_constraint

unification_constraint.inhabited

source

structure unification_hint :

Type (max (u_1+1) (u_2+1))

pattern : unification_constraint
constraints : list unification_constraint

Instances for unification_hint

unification_hint.inhabited

source

@[ext, class]

structure has_zero (α : Type u) :

Type u

zero : α

Instances of this typeclass

source

@[class]

structure has_one (α : Type u) :

Type u

one : α

Instances of this typeclass

source

@[class]

structure has_add (α : Type u) :

Type u

add : α → α → α

Instances of this typeclass

source

@[class]

structure has_mul (α : Type u) :

Type u

mul : α → α → α

Instances of this typeclass

source

@[class]

structure has_inv (α : Type u) :

Type u

inv : α → α

Instances of this typeclass

source

@[class]

structure has_neg (α : Type u) :

Type u

neg : α → α

Instances of this typeclass

source

@[class]

structure has_sub (α : Type u) :

Type u

sub : α → α → α

Instances of this typeclass

source

@[class]

structure has_div (α : Type u) :

Type u

div : α → α → α

Instances of this typeclass

source

@[class]

structure has_dvd (α : Type u) :

Type u

dvd : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_mod (α : Type u) :

Type u

mod : α → α → α

Instances of this typeclass

source

@[ext, class]

structure has_le (α : Type u) :

Type u

le : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_lt (α : Type u) :

Type u

lt : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_append (α : Type u) :

Type u

append : α → α → α

Instances of this typeclass

source

@[class]

structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :

Type (max u v w)

andthen : α → β → σ

Instances of this typeclass

source

@[class]

structure has_union (α : Type u) :

Type u

union : α → α → α

Instances of this typeclass

source

@[class]

structure has_inter (α : Type u) :

Type u

inter : α → α → α

Instances of this typeclass

source

@[class]

structure has_sdiff (α : Type u) :

Type u

sdiff : α → α → α

Instances of this typeclass

source

@[class]

structure has_equiv (α : Sort u) :

Sort (max 1 u)

equiv : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_subset (α : Type u) :

Type u

subset : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_ssubset (α : Type u) :

Type u

ssubset : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_emptyc (α : Type u) :

Type u

emptyc : α

Instances of this typeclass

source

@[class]

structure has_insert (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

insert : α → γ → γ

Instances of this typeclass

source

@[class]

structure has_singleton (α : out_param (Type u)) (β : Type v) :

Type (max u v)

singleton : α → β

Instances of this typeclass

source

@[class]

structure has_sep (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

sep : (α → Prop) → γ → γ

Instances of this typeclass

source

@[class]

structure has_mem (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

mem : α → γ → Prop

Instances of this typeclass

source

@[class]

structure has_pow (α : Type u) (β : Type v) :

Type (max u v)

pow : α → β → α

Instances of this typeclass

source

def ge {α : Type u} [has_le α] (a b : α) :

Prop

Equations

a ≥ b = (b ≤ a)

source

def gt {α : Type u} [has_lt α] (a b : α) :

Prop

Equations

a > b = (b < a)

source

def superset {α : Type u} [has_subset α] (a b : α) :

Prop

Equations

a ⊇ b = (b ⊆ a)

source

def ssuperset {α : Type u} [has_ssubset α] (a b : α) :

Prop

Equations

a ⊃ b = (b ⊂ a)

source

def bit0 {α : Type u} [s : has_add α] (a : α) :

α

Equations

bit0 a = a + a

Instances for bit0

source

def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) :

α

Equations

bit1 a = bit0 a + 1

Instances for bit1

source

@[class]

structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β] [has_singleton α β] :

Prop

insert_emptyc_eq : ∀ (x : α), {x} = {x}

Instances of this typeclass

source

@[protected]

def nat.add :

ℕ → ℕ → ℕ

Equations

a.add b.succ = (a.add b).succ
a.add 0 = a

source

@[protected, instance]

def nat.has_zero :

has_zero ℕ

Equations

nat.has_zero = {zero := 0}

source

@[protected, instance]

def nat.has_one :

has_one ℕ

Equations

nat.has_one = {one := 1}

source

@[protected, instance]

def nat.has_add :

has_add ℕ

Equations

nat.has_add = {add := nat.add}

source

def std.priority.default :

ℕ

Equations

std.priority.default = 1000

source

def std.priority.max :

ℕ

Equations

std.priority.max = 4294967295

source

@[protected]

def nat.prio :

ℕ

Equations

nat.prio = std.priority.default + 100

source

def std.prec.max :

ℕ

Equations

std.prec.max = 1024

source

def std.prec.arrow :

ℕ

Equations

std.prec.arrow = 25

source

def std.prec.max_plus :

ℕ

Equations

std.prec.max_plus = std.prec.max + 10

source

@[class]

structure has_sizeof (α : Sort u) :

Sort (max 1 u)

sizeof : α → ℕ

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
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
monad.has_sizeof_inst
has_monad_lift.has_sizeof_inst
has_monad_lift_t.has_sizeof_inst
monad_functor.has_sizeof_inst
monad_functor_t.has_sizeof_inst
monad_run.has_sizeof_inst
format.color.has_sizeof_inst
monad_fail.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
monad_except.has_sizeof_inst
monad_except_adapter.has_sizeof_inst
state_t.has_sizeof_inst
monad_state.has_sizeof_inst
monad_state_adapter.has_sizeof_inst
reader_t.has_sizeof_inst
monad_reader.has_sizeof_inst
monad_reader_adapter.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
has_abs.has_sizeof_inst
has_pos_part.has_sizeof_inst
has_neg_part.has_sizeof_inst
dlist.has_sizeof_inst
doc_category.has_sizeof_inst
tactic_doc_entry.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
monad_io.has_sizeof_inst
monad_io_terminal.has_sizeof_inst
monad_io_net_system.has_sizeof_inst
monad_io_file_system.has_sizeof_inst
monad_io_environment.has_sizeof_inst
monad_io_process.has_sizeof_inst
monad_io_random.has_sizeof_inst
to_additive.value_type.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
tactic.suggest.head_symbol_match.has_sizeof_inst
has_vadd.has_sizeof_inst
has_vsub.has_sizeof_inst
has_scalar.has_sizeof_inst
semigroup.has_sizeof_inst
add_semigroup.has_sizeof_inst
comm_semigroup.has_sizeof_inst
add_comm_semigroup.has_sizeof_inst
left_cancel_semigroup.has_sizeof_inst
add_left_cancel_semigroup.has_sizeof_inst
right_cancel_semigroup.has_sizeof_inst
add_right_cancel_semigroup.has_sizeof_inst
mul_one_class.has_sizeof_inst
add_zero_class.has_sizeof_inst
add_monoid.has_sizeof_inst
monoid.has_sizeof_inst
add_comm_monoid.has_sizeof_inst
comm_monoid.has_sizeof_inst
add_left_cancel_monoid.has_sizeof_inst
left_cancel_monoid.has_sizeof_inst
add_right_cancel_monoid.has_sizeof_inst
right_cancel_monoid.has_sizeof_inst
add_cancel_monoid.has_sizeof_inst
cancel_monoid.has_sizeof_inst
add_cancel_comm_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
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
add_group.has_sizeof_inst
comm_group.has_sizeof_inst
add_comm_group.has_sizeof_inst
unique.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
has_bracket.has_sizeof_inst
units.has_sizeof_inst
add_units.has_sizeof_inst
fun_like.has_sizeof_inst
zero_hom.has_sizeof_inst
zero_hom_class.has_sizeof_inst
add_hom.has_sizeof_inst
add_hom_class.has_sizeof_inst
add_monoid_hom.has_sizeof_inst
add_monoid_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
embedding_like.has_sizeof_inst
equiv_like.has_sizeof_inst
equiv.has_sizeof_inst
is_nonstrict_strict_order.has_sizeof_inst
has_sup.has_sizeof_inst
has_inf.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
generalized_boolean_algebra.has_sizeof_inst
has_compl.has_sizeof_inst
boolean_algebra.core.has_sizeof_inst
boolean_algebra.has_sizeof_inst
function.embedding.has_sizeof_inst
add_action.has_sizeof_inst
mul_action.has_sizeof_inst
distrib_mul_action.has_sizeof_inst
mul_distrib_mul_action.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
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
add_equiv.has_sizeof_inst
add_equiv_class.has_sizeof_inst
mul_equiv.has_sizeof_inst
mul_equiv_class.has_sizeof_inst
equiv_functor.has_sizeof_inst
has_set_prod.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
ordered_add_comm_monoid.has_sizeof_inst
linear_ordered_add_comm_monoid.has_sizeof_inst
linear_ordered_comm_monoid.has_sizeof_inst
zero_le_one_class.has_sizeof_inst
linear_ordered_comm_monoid_with_zero.has_sizeof_inst
linear_ordered_add_comm_monoid_with_top.has_sizeof_inst
canonically_ordered_add_monoid.has_sizeof_inst
canonically_ordered_monoid.has_sizeof_inst
canonically_linear_ordered_add_monoid.has_sizeof_inst
canonically_linear_ordered_monoid.has_sizeof_inst
ordered_cancel_add_comm_monoid.has_sizeof_inst
ordered_cancel_comm_monoid.has_sizeof_inst
linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
linear_ordered_cancel_comm_monoid.has_sizeof_inst
has_ordered_sub.has_sizeof_inst
ordered_add_comm_group.has_sizeof_inst
ordered_comm_group.has_sizeof_inst
linear_ordered_add_comm_group.has_sizeof_inst
linear_ordered_add_comm_group_with_top.has_sizeof_inst
linear_ordered_comm_group.has_sizeof_inst
add_comm_group.positive_cone.has_sizeof_inst
add_comm_group.total_positive_cone.has_sizeof_inst
ordered_semiring.has_sizeof_inst
ordered_comm_semiring.has_sizeof_inst
linear_ordered_semiring.has_sizeof_inst
ordered_ring.has_sizeof_inst
ordered_comm_ring.has_sizeof_inst
linear_ordered_ring.has_sizeof_inst
linear_ordered_comm_ring.has_sizeof_inst
ring.positive_cone.has_sizeof_inst
ring.total_positive_cone.has_sizeof_inst
canonically_ordered_comm_semiring.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
invertible.has_sizeof_inst
multiset.has_sizeof
tactic.interactive.rep_arity.has_sizeof_inst
expr_lens.dir.has_sizeof_inst
finset.has_sizeof_inst
fintype.has_sizeof_inst
smul_with_zero.has_sizeof_inst
mul_action_with_zero.has_sizeof_inst
division_ring.has_sizeof_inst
field.has_sizeof_inst
linear_ordered_field.has_sizeof_inst
euclidean_domain.has_sizeof_inst
encodable.has_sizeof_inst
rat.has_sizeof_inst
module.has_sizeof_inst
module.core.has_sizeof_inst
set_like.has_sizeof_inst
mul_mem_class.has_sizeof_inst
add_mem_class.has_sizeof_inst
subsemigroup.has_sizeof_inst
add_subsemigroup.has_sizeof_inst
one_mem_class.has_sizeof_inst
zero_mem_class.has_sizeof_inst
submonoid.has_sizeof_inst
submonoid_class.has_sizeof_inst
add_submonoid.has_sizeof_inst
add_submonoid_class.has_sizeof_inst
add_torsor.has_sizeof_inst
ring_equiv.has_sizeof_inst
ring_equiv_class.has_sizeof_inst
inv_mem_class.has_sizeof_inst
neg_mem_class.has_sizeof_inst
subgroup_class.has_sizeof_inst
add_subgroup_class.has_sizeof_inst
subgroup.has_sizeof_inst
add_subgroup.has_sizeof_inst
subsemiring_class.has_sizeof_inst
subsemiring.has_sizeof_inst
subring_class.has_sizeof_inst
subring.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
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
has_star.has_sizeof_inst
has_involutive_star.has_sizeof_inst
star_semigroup.has_sizeof_inst
star_add_monoid.has_sizeof_inst
star_ring.has_sizeof_inst
star_ordered_ring.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
has_quotient.has_sizeof_inst
add_con.has_sizeof_inst
con.has_sizeof_inst
sub_mul_action.has_sizeof_inst
submodule.has_sizeof_inst
normalization_monoid.has_sizeof_inst
gcd_monoid.has_sizeof_inst
normalized_gcd_monoid.has_sizeof_inst
dfinsupp.pre.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
tactic.tfae.arrow.has_sizeof_inst
part.has_sizeof_inst
denumerable.has_sizeof_inst
flag.has_sizeof_inst
omega_complete_partial_order.has_sizeof_inst
omega_complete_partial_order.continuous_hom.has_sizeof_inst
tactic.abel.normalize_mode.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
absolute_value.has_sizeof_inst
succ_order.has_sizeof_inst
pred_order.has_sizeof_inst
linear_pmap.has_sizeof_inst
basis.has_sizeof_inst
tensor_product.compatible_smul.has_sizeof_inst
subalgebra.has_sizeof_inst
non_unital_alg_hom.has_sizeof_inst
non_unital_alg_hom_class.has_sizeof_inst
polynomial.has_sizeof_inst
locally_finite_order.has_sizeof_inst
locally_finite_order_top.has_sizeof_inst
locally_finite_order_bot.has_sizeof_inst
linear_ordered_comm_group_with_zero.has_sizeof_inst
valuation.has_sizeof_inst
valuation_class.has_sizeof_inst
add_submonoid.localization_map.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
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
quiver.has_sizeof_inst
prefunctor.has_sizeof_inst
category_theory.category_struct.has_sizeof_inst
category_theory.category.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.equivalence.has_sizeof_inst
category_theory.is_equivalence.has_sizeof_inst
category_theory.adjunction.has_sizeof_inst
category_theory.is_left_adjoint.has_sizeof_inst
category_theory.is_right_adjoint.has_sizeof_inst
category_theory.adjunction.core_hom_equiv.has_sizeof_inst
category_theory.adjunction.core_unit_counit.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.concrete_category.has_sizeof_inst
category_theory.has_forget₂.has_sizeof_inst
category_theory.bundled.has_sizeof_inst
category_theory.bundled_hom.has_sizeof_inst
category_theory.bundled_hom.parent_projection.has_sizeof_inst
power_basis.has_sizeof_inst
perfect_ring.has_sizeof_inst
lift.subfield_with_hom.has_sizeof_inst
W_type.has_sizeof_inst
free_algebra.pre.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.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.limits.walking_parallel_pair.has_sizeof_inst
category_theory.limits.walking_parallel_pair_hom.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.comma.has_sizeof_inst
category_theory.comma_morphism.has_sizeof_inst
category_theory.limits.walking_pair.has_sizeof_inst
category_theory.arrow.lift_struct.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.bicategory.has_sizeof_inst
category_theory.limits.has_zero_morphisms.has_sizeof_inst
category_theory.preadditive.has_sizeof_inst
category_theory.linear.has_sizeof_inst
category_theory.fin_category.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
Module.has_sizeof_inst
Algebra.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
bifunctor.has_sizeof_inst
is_lawful_bifunctor.has_sizeof_inst
category_theory.reflective.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
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
boolean_ring.has_sizeof_inst
Pointed.has_sizeof_inst
Pointed.hom.has_sizeof_inst
Bipointed.has_sizeof_inst
Bipointed.hom.has_sizeof_inst
BoundedOrder.has_sizeof_inst
SemilatticeSup.has_sizeof_inst
SemilatticeInf.has_sizeof_inst
BoundedLattice.has_sizeof_inst
BoundedDistribLattice.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
quiver.path.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.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.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.monoidal_category.monoidal_predicate.has_sizeof_inst
dual_pair.has_sizeof_inst
category_theory.monoidal_preadditive.has_sizeof_inst
category_theory.monoidal_linear.has_sizeof_inst
category_theory.is_split_coequalizer.has_sizeof_inst
category_theory.limits.preserves_finite_limits.has_sizeof_inst
category_theory.limits.preserves_finite_colimits.has_sizeof_inst
AddCommGroup.colimits.prequotient.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.non_preadditive_abelian.has_sizeof_inst
category_theory.abelian.has_sizeof_inst
category_theory.is_skeleton_of.has_sizeof_inst
category_theory.functor.reflects_exact_sequences.has_sizeof_inst
category_theory.limits.preserves_filtered_colimits.has_sizeof_inst
category_theory.limits.preserves_cofiltered_limits.has_sizeof_inst
category_theory.functorial.has_sizeof_inst
category_theory.lax_monoidal.has_sizeof_inst
category_theory.splitting.has_sizeof_inst
Module.colimits.prequotient.has_sizeof_inst
category_theory.projective_presentation.has_sizeof_inst
Mon.colimits.prequotient.has_sizeof_inst
CommRing.colimits.prequotient.has_sizeof_inst
lazy_list.has_sizeof_inst
generalized_continued_fraction.pair.has_sizeof_inst
generalized_continued_fraction.has_sizeof_inst
floor_semiring.has_sizeof_inst
floor_ring.has_sizeof_inst
generalized_continued_fraction.int_fract_pair.has_sizeof_inst
filter.has_sizeof_inst
filter_basis.has_sizeof_inst
filter.countable_filter_basis.has_sizeof_inst
ultrafilter.has_sizeof_inst
tactic.decl_reducibility.has_sizeof_inst
topological_space.has_sizeof_inst
bornology.has_sizeof_inst
compact_exhaustion.has_sizeof_inst
homeomorph.has_sizeof_inst
continuous_map.has_sizeof_inst
continuous_map_class.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
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
add_group_with_zero_nhd.has_sizeof_inst
group_topology.has_sizeof_inst
add_group_topology.has_sizeof_inst
cubic.has_sizeof_inst
graded_monoid.ghas_one.has_sizeof_inst
graded_monoid.ghas_mul.has_sizeof_inst
graded_monoid.gmonoid.has_sizeof_inst
graded_monoid.gcomm_monoid.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.galgebra.has_sizeof_inst
direct_sum.decomposition.has_sizeof_inst
free_magma.has_sizeof_inst
free_add_magma.has_sizeof_inst
add_freiman_hom.has_sizeof_inst
freiman_hom.has_sizeof_inst
add_freiman_hom_class.has_sizeof_inst
freiman_hom_class.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
homotopy.has_sizeof_inst
homotopy_equiv.has_sizeof_inst
category_theory.differential_object.has_sizeof_inst
category_theory.differential_object.hom.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
ring_quot.has_sizeof_inst
cartan_matrix.generators.has_sizeof_inst
bilin_form.has_sizeof_inst
linear_recurrence.has_sizeof_inst
is_dedekind_domain.height_one_spectrum.has_sizeof_inst
basis.smith_normal_form.has_sizeof_inst
graded_algebra.has_sizeof_inst
order_add_monoid_hom.has_sizeof_inst
order_add_monoid_hom_class.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
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
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
quaternion_algebra.has_sizeof_inst
quaternion_algebra.basis.has_sizeof_inst
real.has_sizeof_inst
uniform_space.core.has_sizeof_inst
uniform_space.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
ring_topology.has_sizeof_inst
complex.has_sizeof_inst
locally_bounded_map.has_sizeof_inst
locally_bounded_map_class.has_sizeof_inst
isometric.has_sizeof_inst
has_norm.has_sizeof_inst
semi_normed_group.has_sizeof_inst
normed_group.has_sizeof_inst
has_nnnorm.has_sizeof_inst
continuous_linear_map.has_sizeof_inst
continuous_linear_equiv.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
nondiscrete_normed_field.has_sizeof_inst
normed_space.has_sizeof_inst
normed_algebra.has_sizeof_inst
local_equiv.has_sizeof_inst
local_homeomorph.has_sizeof_inst
normed_linear_ordered_group.has_sizeof_inst
normed_linear_ordered_field.has_sizeof_inst
affine_map.has_sizeof_inst
affine_equiv.has_sizeof_inst
normed_add_torsor.has_sizeof_inst
affine_subspace.has_sizeof_inst
linear_isometry.has_sizeof_inst
linear_isometry_equiv.has_sizeof_inst
affine_isometry.has_sizeof_inst
affine_isometry_equiv.has_sizeof_inst
closure_operator.has_sizeof_inst
lower_adjoint.has_sizeof_inst
normed_group_hom.has_sizeof_inst
is_R_or_C.has_sizeof_inst
is_CHSH_tuple.has_sizeof_inst
star_subalgebra.has_sizeof_inst
algebraic_geometry.PresheafedSpace.has_sizeof_inst
algebraic_geometry.PresheafedSpace.hom.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.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
algebraic_geometry.SheafedSpace.has_sizeof_inst
algebraic_geometry.LocallyRingedSpace.has_sizeof_inst
TopCommRing.has_sizeof_inst
Top.prelocal_predicate.has_sizeof_inst
Top.local_predicate.has_sizeof_inst
algebraic_geometry.Scheme.has_sizeof_inst
algebraic_geometry.Scheme.open_cover.has_sizeof_inst
EllipticCurve.has_sizeof_inst
category_theory.glue_data.has_sizeof_inst
Top.glue_data.has_sizeof_inst
Top.glue_data.mk_core.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.glue_data.has_sizeof_inst
homogeneous_ideal.has_sizeof_inst
homogeneous_localization.num_denom_same_deg.has_sizeof_inst
nonempty_fin_lin_ord.has_sizeof_inst
continuous_map.homotopy.has_sizeof_inst
continuous_map.homotopy_like.has_sizeof_inst
continuous_map.homotopy_with.has_sizeof_inst
path.has_sizeof_inst
continuous_map.homotopy_equiv.has_sizeof_inst
affine.simplex.has_sizeof_inst
affine_basis.has_sizeof_inst
continuous_multilinear_map.has_sizeof_inst
continuous_linear_map.nonlinear_right_inverse.has_sizeof_inst
has_inner.has_sizeof_inst
inner_product_space.has_sizeof_inst
inner_product_space.core.has_sizeof_inst
convex_cone.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
matrix.transvection_struct.has_sizeof_inst
has_measurable_pow.has_sizeof_inst
topological_lattice.has_sizeof_inst
urysohns.CU.has_sizeof_inst
normed_lattice_add_comm_group.has_sizeof_inst
bounded_continuous_function.has_sizeof_inst
bounded_continuous_map_class.has_sizeof_inst
measure_theory.simple_func.has_sizeof_inst
stieltjes_function.has_sizeof_inst
measure_theory.content.has_sizeof_inst
picard_lindelof.has_sizeof_inst
picard_lindelof.fun_space.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
box_integral.box_additive_map.has_sizeof_inst
continuous_affine_map.has_sizeof_inst
implicit_function_data.has_sizeof_inst
orthonormal_basis.has_sizeof_inst
cont_diff_bump_of_inner.has_sizeof_inst
cont_diff_bump.has_sizeof_inst
topological_fiber_bundle.pretrivialization.has_sizeof_inst
topological_fiber_bundle.trivialization.has_sizeof_inst
topological_fiber_bundle_core.has_sizeof_inst
topological_fiber_prebundle.has_sizeof_inst
abstract_completion.has_sizeof_inst
group_filter_basis.has_sizeof_inst
add_group_filter_basis.has_sizeof_inst
ring_filter_basis.has_sizeof_inst
module_filter_basis.has_sizeof_inst
add_group_seminorm.has_sizeof_inst
seminorm.has_sizeof_inst
geometry.simplicial_complex.has_sizeof_inst
hilbert_basis.has_sizeof_inst
derivation.has_sizeof_inst
module.oriented.has_sizeof_inst
enorm.has_sizeof_inst
wstar_algebra.has_sizeof_inst
von_neumann_algebra.has_sizeof_inst
category_theory.ProjectiveResolution.has_sizeof_inst
category_theory.injective_presentation.has_sizeof_inst
category_theory.InjectiveResolution.has_sizeof_inst
semidirect_product.has_sizeof_inst
category_theory.additive_category.has_sizeof_inst
category_theory.limits.walking_parallel_family.has_sizeof_inst
category_theory.limits.walking_parallel_family.hom.has_sizeof_inst
category_theory.is_kernel_pair.has_sizeof_inst
category_theory.monad.has_sizeof_inst
category_theory.comonad.has_sizeof_inst
category_theory.monad_hom.has_sizeof_inst
category_theory.comonad_hom.has_sizeof_inst
category_theory.monad.algebra.has_sizeof_inst
category_theory.monad.algebra.hom.has_sizeof_inst
category_theory.comonad.coalgebra.has_sizeof_inst
category_theory.comonad.coalgebra.hom.has_sizeof_inst
category_theory.monadic_right_adjoint.has_sizeof_inst
category_theory.comonadic_left_adjoint.has_sizeof_inst
category_theory.oplax_nat_trans.has_sizeof_inst
category_theory.oplax_nat_trans.modification.has_sizeof_inst
two_pointing.has_sizeof_inst
Twop.has_sizeof_inst
category_theory.cartesian_closed_functor.has_sizeof_inst
category_theory.unbundled_hom.has_sizeof_inst
category_theory.sigma.sigma_hom.has_sizeof_inst
category_theory.endofunctor.algebra.has_sizeof_inst
category_theory.endofunctor.algebra.hom.has_sizeof_inst
category_theory.half_braiding.has_sizeof_inst
category_theory.center.hom.has_sizeof_inst
category_theory.enriched_category.has_sizeof_inst
category_theory.enriched_functor.has_sizeof_inst
category_theory.graded_nat_trans.has_sizeof_inst
category_theory.grothendieck.has_sizeof_inst
category_theory.grothendieck.hom.has_sizeof_inst
category_theory.idempotents.karoubi.has_sizeof_inst
category_theory.idempotents.karoubi.hom.has_sizeof_inst
category_theory.limits.diagram_of_cones.has_sizeof_inst
category_theory.limits.coproduct_disjoint.has_sizeof_inst
category_theory.limits.coproducts_disjoint.has_sizeof_inst
Mon_.has_sizeof_inst
Mon_.hom.has_sizeof_inst
CommMon_.has_sizeof_inst
Mod.has_sizeof_inst
Mod.hom.has_sizeof_inst
category_theory.noetherian.has_sizeof_inst
category_theory.artinian.has_sizeof_inst
category_theory.Mat_.has_sizeof_inst
category_theory.triangulated.triangle.has_sizeof_inst
category_theory.triangulated.triangle_morphism.has_sizeof_inst
category_theory.triangulated.pretriangulated.has_sizeof_inst
category_theory.triangulated.pretriangulated.triangulated_functor_struct.has_sizeof_inst
category_theory.triangulated.pretriangulated.triangulated_functor.has_sizeof_inst
category_theory.with_terminal.has_sizeof_inst
category_theory.with_initial.has_sizeof_inst
configuration.has_points.has_sizeof_inst
configuration.has_lines.has_sizeof_inst
configuration.projective_plane.has_sizeof_inst
combinatorics.line.has_sizeof_inst
combinatorics.line.almost_mono.has_sizeof_inst
combinatorics.line.color_focused.has_sizeof_inst
quiver.total.has_sizeof_inst
quiver.arborescence.has_sizeof_inst
quiver.has_reverse.has_sizeof_inst
simple_graph.has_sizeof_inst
simple_graph.dart.has_sizeof_inst
simple_graph.subgraph.has_sizeof_inst
alist.has_sizeof_inst
simple_graph.walk.has_sizeof_inst
finpartition.has_sizeof_inst
indexed_partition.has_sizeof_inst
simple_graph.partition.has_sizeof_inst
DFA.has_sizeof_inst
NFA.has_sizeof_inst
nzsnum.has_sizeof_inst
snum.has_sizeof_inst
computability.encoding.has_sizeof_inst
computability.fin_encoding.has_sizeof_inst
computability.Γ'.has_sizeof_inst
ε_NFA.has_sizeof_inst
primcodable.has_sizeof_inst
nat.partrec.code.has_sizeof_inst
regular_expression.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.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
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
bitraversable.has_sizeof_inst
is_lawful_bitraversable.has_sizeof_inst
has_fix.has_sizeof_inst
fin2.has_sizeof_inst
fin2.is_lt.has_sizeof_inst
mvfunctor.has_sizeof_inst
lawful_fix.has_sizeof_inst
writer_t.has_sizeof_inst
monad_writer.has_sizeof_inst
monad_writer_adapter.has_sizeof_inst
monad_cont.label.has_sizeof_inst
monad_cont.has_sizeof_inst
is_lawful_monad_cont.has_sizeof_inst
uliftable.has_sizeof_inst
bounded_random.has_sizeof_inst
random.has_sizeof_inst
W_type.nat_α.has_sizeof_inst
W_type.list_α.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
parse_result.has_sizeof_inst
fin_enum.has_sizeof_inst
finmap.has_sizeof_inst
semiquot.has_sizeof_inst
fp.rmode.has_sizeof_inst
fp.float_cfg.has_sizeof_inst
fp.float.has_sizeof_inst
hash_map.has_sizeof_inst
ordnode.has_sizeof_inst
pfunctor.has_sizeof_inst
mvpfunctor.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
pnat.xgcd_type.has_sizeof_inst
pnat.xgcd_type.has_sizeof
mvqpf.has_sizeof_inst
qpf.has_sizeof_inst
has_finite_inter.has_sizeof_inst
sign_type.has_sizeof_inst
circle_deg1_lift.has_sizeof_inst
flow.has_sizeof_inst
subfield_class.has_sizeof_inst
subfield.has_sizeof_inst
intermediate_field.has_sizeof_inst
intermediate_field.insert.has_sizeof_inst
open_add_subgroup.has_sizeof_inst
open_subgroup.has_sizeof_inst
hahn_series.has_sizeof_inst
hahn_series.summable_family.has_sizeof_inst
ratfunc.has_sizeof_inst
affine.simplex.points_with_circumcenter_index.has_sizeof_inst
topological_vector_bundle.pretrivialization.has_sizeof_inst
topological_vector_bundle.trivialization.has_sizeof_inst
topological_vector_bundle.has_sizeof_inst
topological_vector_bundle_core.has_sizeof_inst
topological_vector_prebundle.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
basic_smooth_vector_bundle_core.has_sizeof_inst
cont_mdiff_map.has_sizeof_inst
smooth_add_monoid_morphism.has_sizeof_inst
smooth_monoid_morphism.has_sizeof_inst
left_invariant_derivation.has_sizeof_inst
smooth_bump_function.has_sizeof_inst
diffeomorph.has_sizeof_inst
shrinking_lemma.partial_refinement.has_sizeof_inst
partition_of_unity.has_sizeof_inst
bump_covering.has_sizeof_inst
smooth_bump_covering.has_sizeof_inst
smooth_partition_of_unity.has_sizeof_inst
is_free_group.has_sizeof_inst
free_product.word.has_sizeof_inst
free_product.word.pair.has_sizeof_inst
free_product.neword.has_sizeof_inst
is_free_groupoid.has_sizeof_inst
sylow.has_sizeof_inst
dihedral_group.has_sizeof_inst
quaternion_group.has_sizeof_inst
quadratic_form.has_sizeof_inst
quadratic_form.isometry.has_sizeof_inst
upgraded_polish_space.has_sizeof_inst
vitali_family.has_sizeof_inst
measure_theory.vector_measure.has_sizeof_inst
measure_theory.jordan_decomposition.has_sizeof_inst
besicovitch.satellite_config.has_sizeof_inst
besicovitch.ball_package.has_sizeof_inst
besicovitch.tau_package.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.elementary_embedding.has_sizeof_inst
first_order.language.elementary_substructure.has_sizeof_inst
first_order.language.Theory.Model.has_sizeof_inst
first_order.language.prestructure.has_sizeof_inst
first_order.language.is_ordered.has_sizeof_inst
absolute_value.is_admissible.has_sizeof_inst
valued.has_sizeof_inst
zsqrtd.has_sizeof_inst
FinPartialOrder.has_sizeof_inst
FinBoolAlg.has_sizeof_inst
CompHaus.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
concept.has_sizeof_inst
upper_set.has_sizeof_inst
lower_set.has_sizeof_inst
order.ideal.has_sizeof_inst
order.cofinal.has_sizeof_inst
grade_order.has_sizeof_inst
grade_min_order.has_sizeof_inst
grade_max_order.has_sizeof_inst
grade_bounded_order.has_sizeof_inst
jordan_holder_lattice.has_sizeof_inst
composition_series.has_sizeof_inst
order.pfilter.has_sizeof_inst
order.ideal.prime_pair.has_sizeof_inst
measure_theory.filtration.has_sizeof_inst
Action.has_sizeof_inst
Action.hom.has_sizeof_inst
valuation_subring.has_sizeof_inst
ring_invo.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
pgame.has_sizeof_inst
pgame.restricted.has_sizeof_inst
pgame.relabelling.has_sizeof_inst
pgame.inv_ty.has_sizeof_inst
pgame.short.has_sizeof_inst
pgame.list_short.has_sizeof_inst
pgame.state.has_sizeof_inst
lists'.has_sizeof_inst
lists.has_sizeof
onote.has_sizeof_inst
pSet.has_sizeof_inst
pSet.definable.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
has_variable_names.has_sizeof_inst
tactic.eliminate.generalization_mode.has_sizeof_inst
side.has_sizeof_inst
tactic.rewrite_search.side.has_sizeof_inst
tactic.rewrite_search.dir_pair.has_sizeof_inst
_nest_2_2.tactic.rewrite_search.using_conv.app_addr._mut_.has_sizeof_inst
_nest_2_2.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
_nest_2_2.option.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
_nest_2_1.tactic.rewrite_search._nest_1_1.tactic.rewrite_search.using_conv.app_addr.dir_pair.has_sizeof_inst
_nest_1_1.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
_nest_1_1.option.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
tactic.rewrite_search.using_conv.splice_result.has_sizeof_inst
tactic.ring2.csring_expr.has_sizeof_inst
tactic.ring2.horner_expr.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
slim_check.total_function.has_sizeof_inst
slim_check.injective_function.has_sizeof_inst
slim_check.injective_function.has_sizeof
continuous_add_monoid_hom.has_sizeof_inst
continuous_monoid_hom.has_sizeof_inst
continuous_add_monoid_hom_class.has_sizeof_inst
continuous_monoid_hom_class.has_sizeof_inst
with_ideal.has_sizeof_inst
locally_constant.has_sizeof_inst
Profinite.has_sizeof_inst
discrete_quotient.has_sizeof_inst
CpltSepUniformSpace.has_sizeof_inst
cocompact_map.has_sizeof_inst
cocompact_map_class.has_sizeof_inst
zero_at_infty_continuous_map.has_sizeof_inst
zero_at_infty_continuous_map_class.has_sizeof_inst
continuous_open_map.has_sizeof_inst
continuous_open_map_class.has_sizeof_inst
Gromov_Hausdorff.aux_gluing_struct.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
priestley_space.has_sizeof_inst
clopen_upper_set.has_sizeof_inst
spectral_map.has_sizeof_inst
spectral_map_class.has_sizeof_inst
uniform_equiv.has_sizeof_inst
module_doc_info.has_sizeof_inst
ext_tactic_doc_entry.has_sizeof_inst
slim_check.total_function.has_sizeof