mathlib3 documentation

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 : α) :

Gadget for optional parameter support.

@[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.

@[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)

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 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) :
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 nat  :
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_neg (α : Type u) :
  • neg : α α
Instances of this typeclass
@[class]
structure has_sub (α : Type u) :
Instances of this typeclass
@[class]
structure has_dvd (α : 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_equiv (α : Sort u) :
Sort (max 1 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_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_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 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 β] [has_insert α β] [has_singleton α β] :
Prop
  • insert_emptyc_eq : (x : α), {x} = {x}
Instances of this typeclass

nat basic instances

@[protected]
def nat.add  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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
  • 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
  • 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
  • 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
  • function.has_uncurry.has_sizeof_inst
  • to_additive.value_type.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_smul.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
  • 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
  • add_group.has_sizeof_inst
  • comm_group.has_sizeof_inst
  • add_comm_group.has_sizeof_inst
  • unique.has_sizeof_inst
  • units.has_sizeof_inst
  • add_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
  • 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
  • function.embedding.has_sizeof_inst
  • add_action.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
  • add_monoid_with_one.has_sizeof_inst
  • add_comm_monoid_with_one.has_sizeof_inst
  • has_int_cast.has_sizeof_inst
  • add_group_with_one.has_sizeof_inst
  • add_comm_group_with_one.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
  • 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
  • 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
  • linear_ordered_add_comm_monoid_with_top.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
  • 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
  • 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
  • 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
  • subadditive_hom_class.has_sizeof_inst
  • submultiplicative_hom_class.has_sizeof_inst
  • mul_le_add_hom_class.has_sizeof_inst
  • nonarchimedean_hom_class.has_sizeof_inst
  • add_group_seminorm_class.has_sizeof_inst
  • group_seminorm_class.has_sizeof_inst
  • add_group_norm_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_add_monoid.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
  • add_subsemigroup.has_sizeof_inst
  • submonoid.has_sizeof_inst
  • add_submonoid.has_sizeof_inst
  • encodable.has_sizeof_inst
  • subgroup.has_sizeof_inst
  • add_subgroup.has_sizeof_inst
  • smul_mem_class.has_sizeof_inst
  • vadd_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
  • add_con.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
  • 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
  • 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
  • add_torsor.has_sizeof_inst
  • continuous_map.has_sizeof_inst
  • continuous_map_class.has_sizeof_inst
  • add_group_with_zero_nhd.has_sizeof_inst
  • group_topology.has_sizeof_inst
  • add_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
  • add_group_seminorm.has_sizeof_inst
  • group_seminorm.has_sizeof_inst
  • nonarch_add_group_seminorm.has_sizeof_inst
  • add_group_norm.has_sizeof_inst
  • group_norm.has_sizeof_inst
  • nonarch_add_group_norm.has_sizeof_inst
  • nonarch_add_group_seminorm_class.has_sizeof_inst
  • nonarch_add_group_norm_class.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_add_group.has_sizeof_inst
  • seminormed_group.has_sizeof_inst
  • normed_add_group.has_sizeof_inst
  • normed_group.has_sizeof_inst
  • seminormed_add_comm_group.has_sizeof_inst
  • seminormed_comm_group.has_sizeof_inst
  • normed_add_comm_group.has_sizeof_inst
  • normed_comm_group.has_sizeof_inst
  • normed_add_group_hom.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
  • lower_adjoint.has_sizeof_inst
  • affine.simplex.has_sizeof_inst
  • affine_basis.has_sizeof_inst
  • path.has_sizeof_inst
  • normed_ordered_add_group.has_sizeof_inst
  • normed_ordered_group.has_sizeof_inst
  • normed_linear_ordered_add_group.has_sizeof_inst
  • normed_linear_ordered_group.has_sizeof_inst
  • normed_linear_ordered_field.has_sizeof_inst
  • normed_add_torsor.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
  • add_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
  • box_integral.box_additive_map.has_sizeof_inst
  • normed_lattice_add_comm_group.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_add_subgroup.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
  • 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
  • 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.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.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
  • _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
  • side.has_sizeof_inst
  • measure_theory.vector_measure.has_sizeof_inst
  • measure_theory.jordan_decomposition.has_sizeof_inst
  • measure_theory.filtration.has_sizeof_inst
  • upgraded_polish_space.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.preadditive.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.non_preadditive_abelian.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
  • 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
  • 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
  • category_theory.monadic_right_adjoint.has_sizeof_inst
  • category_theory.comonadic_left_adjoint.has_sizeof_inst
  • CpltSepUniformSpace.has_sizeof_inst
  • TopCommRing.has_sizeof_inst
  • CompHaus.has_sizeof_inst
  • Profinite.has_sizeof_inst
  • valued.has_sizeof_inst
  • 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
  • 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
  • category_theory.graded_nat_trans.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
  • is_adjoin_root.has_sizeof_inst
  • is_adjoin_root_monic.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
  • 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.gring.has_sizeof_inst
  • direct_sum.gcomm_ring.has_sizeof_inst
  • direct_sum.galgebra.has_sizeof_inst
  • graded_ring.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
  • grade_order.has_sizeof_inst
  • grade_min_order.has_sizeof_inst
  • grade_max_order.has_sizeof_inst
  • grade_bounded_order.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
  • absolute_value.is_admissible.has_sizeof_inst
  • diffeomorph.has_sizeof_inst
  • smooth_bump_function.has_sizeof_inst
  • smooth_add_monoid_morphism.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_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
  • 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_add_magma.has_sizeof_inst
  • free_add_semigroup.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
  • graded_monoid.ghas_smul.has_sizeof_inst
  • graded_monoid.gmul_action.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
  • add_freiman_hom.has_sizeof_inst
  • freiman_hom.has_sizeof_inst
  • centroid_hom.has_sizeof_inst
  • centroid_hom_class.has_sizeof_inst
  • AddCommGroup.colimits.prequotient.has_sizeof_inst
  • Mon.colimits.prequotient.has_sizeof_inst
  • quadratic_form.has_sizeof_inst
  • quadratic_form.isometry.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
  • counterexample.phillips_1940.bounded_additive_measure.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
@[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
@[protected, instance]
def psigma.has_sizeof (α : Type u) (β : α Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
@[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