mathlib documentation

core / init.core

source
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.

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
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
source
inductive false  :
Prop
source
inductive empty  :
Type
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.

source
inductive eq {α : Sort u} (a : α) :
α → Prop
  • refl : ∀ {α : Sort u} (a : α), a = a
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 : β
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.

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.

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), β → α ⊕ β
source
inductive psum (α : Sort u) (β : Sort v) :
Sort (max 1 u v)
  • inl : Π (α : Sort u) (β : Sort v), α → psum α β
  • inr : Π (α : Sort u) (β : Sort v), β → 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.

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
source
structure psigma {α : Sort u} (β : α → Sort v) :
Sort (max 1 u v)
  • fst : α
  • snd : β self.fst
source
inductive bool  :
Type
source
structure subtype {α : Sort u} (p : α → Prop) :
Sort (max 1 u)
  • val : α
  • property : p self.val
source
@[class]
inductive decidable (p : Prop) :
Type
Instances
source
def decidable_pred {α : Sort u} (r : α → Prop) :
Sort (max u 1)
Equations
source
def decidable_rel {α : Sort u} (r : α → α → Prop) :
Sort (max u 1)
Equations
source
def decidable_eq (α : Sort u) :
Sort (max u 1)
Equations
source
inductive option (α : Type u) :
Type u
  • none : Π (α : Type u), option α
  • some : Π (α : Type u), α → option α
source
inductive list (T : Type u) :
Type u
  • nil : Π (T : Type u), list T
  • cons : Π (T : Type u), T → list T → list T
source
inductive nat  :
Type
source
structure unification_constraint  :
Type (u+1)
  • α : Type ?
  • lhs : self.α
  • rhs : self.α
source
structure unification_hint  :
Type (max (u_1+1) (u_2+1))
source
@[ext, class]
structure has_zero (α : Type u) :
Type u
  • zero : α
Instances
source
@[class]
structure has_one (α : Type u) :
Type u
  • one : α
Instances
source
@[class]
structure has_add (α : Type u) :
Type u
  • add : α → α → α
Instances
source
@[class]
structure has_mul (α : Type u) :
Type u
  • mul : α → α → α
Instances
source
@[class]
structure has_inv (α : Type u) :
Type u
  • inv : α → α
Instances
source
@[class]
structure has_neg (α : Type u) :
Type u
  • neg : α → α
Instances
source
@[class]
structure has_sub (α : Type u) :
Type u
  • sub : α → α → α
Instances
source
@[class]
structure has_div (α : Type u) :
Type u
  • div : α → α → α
Instances
source
@[class]
structure has_dvd (α : Type u) :
Type u
  • dvd : α → α → Prop
Instances
source
@[class]
structure has_mod (α : Type u) :
Type u
  • mod : α → α → α
Instances
source
@[ext, class]
structure has_le (α : Type u) :
Type u
  • le : α → α → Prop
Instances
source
@[class]
structure has_lt (α : Type u) :
Type u
  • lt : α → α → Prop
Instances
source
@[class]
structure has_append (α : Type u) :
Type u
  • append : α → α → α
Instances
source
@[class]
structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :
Type (max u v w)
  • andthen : α → β → σ
Instances
source
@[class]
structure has_union (α : Type u) :
Type u
  • union : α → α → α
Instances
source
@[class]
structure has_inter (α : Type u) :
Type u
  • inter : α → α → α
Instances
source
@[class]
structure has_sdiff (α : Type u) :
Type u
  • sdiff : α → α → α
Instances
source
@[class]
structure has_equiv (α : Sort u) :
Sort (max 1 u)
  • equiv : α → α → Prop
Instances
source
@[class]
structure has_subset (α : Type u) :
Type u
  • subset : α → α → Prop
Instances
source
@[class]
structure has_ssubset (α : Type u) :
Type u
  • ssubset : α → α → Prop
Instances
source
@[class]
structure has_emptyc (α : Type u) :
Type u
  • emptyc : α
Instances
source
@[class]
structure has_insert (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
  • insert : α → γ → γ
Instances
source
@[class]
structure has_singleton (α : out_param (Type u)) (β : Type v) :
Type (max u v)
  • singleton : α → β
Instances
source
@[class]
structure has_sep (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
  • sep : (α → Prop) → γ → γ
Instances
source
@[class]
structure has_mem (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
  • mem : α → γ → Prop
Instances
source
@[class]
structure has_pow (α : Type u) (β : Type v) :
Type (max u v)
  • pow : α → β → α
Instances
source
def ge {α : Type u} [has_le α] (a b : α) :
Prop
Equations
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
source
def ssuperset {α : Type u} [has_ssubset α] (a b : α) :
Prop
Equations
source
def bit0 {α : Type u} [s : has_add α] (a : α) :
α
Equations
source
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) :
α
Equations
source
@[class]
structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β] [has_singleton α β] :
Prop
  • insert_emptyc_eq : ∀ (x : α), {x} = {x}
Instances
source
def nat.add  :
ℕ → ℕ → ℕ
Equations
source
@[instance]
def nat.has_zero  :
has_zero ℕ
Equations
source
@[instance]
def nat.has_one  :
has_one ℕ
Equations
source
@[instance]
def nat.has_add  :
has_add ℕ
Equations
source
def std.priority.default  :
ℕ
Equations
source
def std.priority.max  :
ℕ
Equations
source
def nat.prio  :
ℕ
Equations
source
def std.prec.max  :
ℕ
Equations
source
def std.prec.arrow  :
ℕ
Equations
source
def std.prec.max_plus  :
ℕ
Equations
source
@[class]
structure has_sizeof (α : Sort u) :
Sort (max 1 u)
  • sizeof : α → ℕ
Instances
  • 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
  • rbnode.has_sizeof_inst
  • rbnode.color.has_sizeof_inst
  • widget.mouse_event_kind.has_sizeof_inst
  • dlist.has_sizeof_inst
  • parse_result.has_sizeof_inst
  • doc_category.has_sizeof_inst
  • tactic_doc_entry.has_sizeof_inst
  • pempty.has_sizeof_inst
  • function.has_uncurry.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
  • 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
  • to_additive.value_type.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
  • unique.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
  • semilattice_sup_top.has_sizeof_inst
  • semilattice_sup_bot.has_sizeof_inst
  • semilattice_inf_top.has_sizeof_inst
  • semilattice_inf_bot.has_sizeof_inst
  • bounded_lattice.has_sizeof_inst
  • distrib_lattice_bot.has_sizeof_inst
  • bounded_distrib_lattice.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
  • equiv.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
  • div_inv_monoid.has_sizeof_inst
  • sub_neg_monoid.has_sizeof_inst
  • group.has_sizeof_inst
  • add_group.has_sizeof_inst
  • comm_group.has_sizeof_inst
  • add_comm_group.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
  • comm_cancel_monoid_with_zero.has_sizeof_inst
  • group_with_zero.has_sizeof_inst
  • comm_group_with_zero.has_sizeof_inst
  • zero_hom.has_sizeof_inst
  • add_hom.has_sizeof_inst
  • add_monoid_hom.has_sizeof_inst
  • one_hom.has_sizeof_inst
  • mul_hom.has_sizeof_inst
  • monoid_hom.has_sizeof_inst
  • monoid_with_zero_hom.has_sizeof_inst
  • function.embedding.has_sizeof_inst
  • distrib.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
  • ring_hom.has_sizeof_inst
  • comm_semiring.has_sizeof_inst
  • ring.has_sizeof_inst
  • comm_ring.has_sizeof_inst
  • domain.has_sizeof_inst
  • integral_domain.has_sizeof_inst
  • division_ring.has_sizeof_inst
  • field.has_sizeof_inst
  • has_vadd.has_sizeof_inst
  • has_scalar.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
  • add_equiv.has_sizeof_inst
  • mul_equiv.has_sizeof_inst
  • invertible.has_sizeof_inst
  • rel_hom.has_sizeof_inst
  • rel_embedding.has_sizeof_inst
  • rel_iso.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_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
  • 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
  • nonneg_add_comm_group.has_sizeof_inst
  • has_ordered_sub.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
  • nonneg_ring.has_sizeof_inst
  • linear_nonneg_ring.has_sizeof_inst
  • canonically_ordered_comm_semiring.has_sizeof_inst
  • tactic.interactive.mono_cfg.has_sizeof_inst
  • tactic.interactive.mono_selection.has_sizeof_inst
  • multiset.has_sizeof
  • linear_ordered_field.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
  • complete_distrib_lattice.has_sizeof_inst
  • complete_boolean_algebra.has_sizeof_inst
  • directed_order.has_sizeof_inst
  • galois_insertion.has_sizeof_inst
  • galois_coinsertion.has_sizeof_inst
  • tactic.interactive.rep_arity.has_sizeof_inst
  • expr_lens.dir.has_sizeof_inst
  • finset.has_sizeof_inst
  • encodable.has_sizeof_inst
  • euclidean_domain.has_sizeof_inst
  • rat.has_sizeof_inst
  • fintype.has_sizeof_inst
  • tactic.abel.normalize_mode.has_sizeof_inst
  • smul_with_zero.has_sizeof_inst
  • mul_action_with_zero.has_sizeof_inst
  • module.has_sizeof_inst
  • module.core.has_sizeof_inst
  • set_like.has_sizeof_inst
  • submonoid.has_sizeof_inst
  • add_submonoid.has_sizeof_inst
  • has_vsub.has_sizeof_inst
  • add_torsor.has_sizeof_inst
  • ring_equiv.has_sizeof_inst
  • has_star.has_sizeof_inst
  • has_involutive_star.has_sizeof_inst
  • star_monoid.has_sizeof_inst
  • star_ring.has_sizeof_inst
  • star_ordered_ring.has_sizeof_inst
  • subgroup.has_sizeof_inst
  • add_subgroup.has_sizeof_inst
  • subsemiring.has_sizeof_inst
  • subring.has_sizeof_inst
  • mul_semiring_action.has_sizeof_inst
  • mul_action_hom.has_sizeof_inst
  • distrib_mul_action_hom.has_sizeof_inst
  • mul_semiring_action_hom.has_sizeof_inst
  • linear_map.has_sizeof_inst
  • linear_map.compatible_smul.has_sizeof_inst
  • linear_equiv.has_sizeof_inst
  • sub_mul_action.has_sizeof_inst
  • submodule.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
  • denumerable.has_sizeof_inst
  • preorder_hom.has_sizeof_inst
  • part.has_sizeof_inst
  • tactic.tfae.arrow.has_sizeof_inst
  • omega_complete_partial_order.has_sizeof_inst
  • omega_complete_partial_order.continuous_hom.has_sizeof_inst
  • algebra.has_sizeof_inst
  • alg_hom.has_sizeof_inst
  • alg_equiv.has_sizeof_inst
  • add_con.has_sizeof_inst
  • con.has_sizeof_inst
  • tensor_product.compatible_smul.has_sizeof_inst
  • subalgebra.has_sizeof_inst
  • tactic.ring.normalize_mode.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
  • floor_ring.has_sizeof_inst
  • absolute_value.has_sizeof_inst
  • non_unital_alg_hom.has_sizeof_inst
  • quiver.has_sizeof_inst
  • prefunctor.has_sizeof_inst
  • quiver.total.has_sizeof_inst
  • quiver.path.has_sizeof_inst
  • quiver.arborescence.has_sizeof_inst
  • quiver.has_reverse.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.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
  • category_theory.unbundled_hom.has_sizeof_inst
  • free_algebra.pre.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.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.has_images.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.has_zero_object.has_sizeof_inst
  • category_theory.preadditive.has_sizeof_inst
  • category_theory.linear.has_sizeof_inst
  • Module.has_sizeof_inst
  • Algebra.has_sizeof_inst
  • category_theory.fin_category.has_sizeof_inst
  • bifunctor.has_sizeof_inst
  • is_lawful_bifunctor.has_sizeof_inst
  • equiv_functor.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.has_sizeof_inst
  • category_theory.limits.preserves_colimits.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.has_sizeof_inst
  • category_theory.limits.reflects_colimits.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.has_sizeof_inst
  • category_theory.creates_colimit.has_sizeof_inst
  • category_theory.creates_colimits_of_shape.has_sizeof_inst
  • category_theory.creates_colimits.has_sizeof_inst
  • category_theory.lifts_to_limit.has_sizeof_inst
  • category_theory.lifts_to_colimit.has_sizeof_inst
  • linear_pmap.has_sizeof_inst
  • basis.has_sizeof_inst
  • polynomial.has_sizeof_inst
  • CommRing.colimits.prequotient.has_sizeof_inst
  • category_theory.limits.preserves_filtered_colimits.has_sizeof_inst
  • category_theory.limits.preserves_cofiltered_limits.has_sizeof_inst
  • category_theory.monoidal_category.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
  • initial_seg.has_sizeof_inst
  • principal_seg.has_sizeof_inst
  • Well_order.has_sizeof_inst
  • normalization_monoid.has_sizeof_inst
  • gcd_monoid.has_sizeof_inst
  • linear_ordered_comm_group_with_zero.has_sizeof_inst
  • valuation.has_sizeof_inst
  • tactic.decl_reducibility.has_sizeof_inst
  • filter.has_sizeof_inst
  • filter_basis.has_sizeof_inst
  • filter.countable_filter_basis.has_sizeof_inst
  • ultrafilter.has_sizeof_inst
  • topological_space.has_sizeof_inst
  • compact_exhaustion.has_sizeof_inst
  • homeomorph.has_sizeof_inst
  • dual_pair.has_sizeof_inst
  • category_theory.lax_monoidal_functor.has_sizeof_inst
  • category_theory.monoidal_functor.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
  • AddCommGroup.colimits.prequotient.has_sizeof_inst
  • category_theory.functorial.has_sizeof_inst
  • category_theory.lax_monoidal.has_sizeof_inst
  • category_theory.limits.bicone.has_sizeof_inst
  • category_theory.limits.limit_bicone.has_sizeof_inst
  • category_theory.limits.binary_bicone.has_sizeof_inst
  • category_theory.limits.binary_biproduct_data.has_sizeof_inst
  • category_theory.regular_mono.has_sizeof_inst
  • category_theory.regular_epi.has_sizeof_inst
  • category_theory.normal_mono.has_sizeof_inst
  • category_theory.normal_epi.has_sizeof_inst
  • category_theory.non_preadditive_abelian.has_sizeof_inst
  • category_theory.abelian.has_sizeof_inst
  • category_theory.reflective.has_sizeof_inst
  • category_theory.is_skeleton_of.has_sizeof_inst
  • Module.colimits.prequotient.has_sizeof_inst
  • category_theory.projective_presentation.has_sizeof_inst
  • Mon.colimits.prequotient.has_sizeof_inst
  • tactic.ring_exp.coeff.has_sizeof_inst
  • tactic.ring_exp.ex_type.has_sizeof_inst
  • add_submonoid.localization_map.has_sizeof_inst
  • submonoid.localization_map.has_sizeof_inst
  • ring_quot.has_sizeof_inst
  • lazy_list.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
  • add_group_with_zero_nhd.has_sizeof_inst
  • direct_sum.ghas_one.has_sizeof_inst
  • direct_sum.ghas_mul.has_sizeof_inst
  • direct_sum.gmonoid.has_sizeof_inst
  • direct_sum.gcomm_monoid.has_sizeof_inst
  • direct_sum.galgebra.has_sizeof_inst
  • free_magma.has_sizeof_inst
  • free_add_magma.has_sizeof_inst
  • complex_shape.has_sizeof_inst
  • category_theory.has_shift.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
  • category_theory.differential_object.has_sizeof_inst
  • category_theory.differential_object.hom.has_sizeof_inst
  • homotopy.has_sizeof_inst
  • homotopy_equiv.has_sizeof_inst
  • category_theory.quotient.has_sizeof_inst
  • has_bracket.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
  • cartan_matrix.generators.has_sizeof_inst
  • power_basis.has_sizeof_inst
  • lift.subfield_with_hom.has_sizeof_inst
  • pequiv.has_sizeof_inst
  • composition.has_sizeof_inst
  • composition_as_set.has_sizeof_inst
  • partition.has_sizeof_inst
  • multilinear_map.has_sizeof_inst
  • alternating_map.has_sizeof_inst
  • bilin_form.has_sizeof_inst
  • matrix.transvection_struct.has_sizeof_inst
  • linear_recurrence.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
  • boolean_ring.has_sizeof_inst
  • star_algebra.has_sizeof_inst
  • uniform_space.core.has_sizeof_inst
  • uniform_space.has_sizeof_inst
  • abstract_completion.has_sizeof_inst
  • cau_seq.is_complete.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
  • ring_topology.has_sizeof_inst
  • continuous_linear_map.has_sizeof_inst
  • continuous_linear_equiv.has_sizeof_inst
  • has_continuous_inv'.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
  • semi_normed_ring.has_sizeof_inst
  • normed_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
  • semi_normed_space.has_sizeof_inst
  • normed_space.has_sizeof_inst
  • semi_normed_algebra.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
  • closure_operator.has_sizeof_inst
  • lower_adjoint.has_sizeof_inst
  • linear_isometry.has_sizeof_inst
  • linear_isometry_equiv.has_sizeof_inst
  • continuous_multilinear_map.has_sizeof_inst
  • affine_equiv.has_sizeof_inst
  • semi_normed_add_torsor.has_sizeof_inst
  • normed_add_torsor.has_sizeof_inst
  • affine_subspace.has_sizeof_inst
  • affine_isometry.has_sizeof_inst
  • affine_isometry_equiv.has_sizeof_inst
  • continuous_map.has_sizeof_inst
  • path.has_sizeof_inst
  • is_R_or_C.has_sizeof_inst
  • continuous_linear_map.nonlinear_right_inverse.has_sizeof_inst
  • complex.has_sizeof_inst
  • is_CHSH_tuple.has_sizeof_inst
  • EllipticCurve.has_sizeof_inst
  • algebraic_geometry.PresheafedSpace.has_sizeof_inst
  • algebraic_geometry.PresheafedSpace.hom.has_sizeof_inst
  • Top.sheaf.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
  • nonempty_fin_lin_ord.has_sizeof_inst
  • ring_invo.has_sizeof_inst
  • sesq_form.has_sizeof_inst
  • has_inner.has_sizeof_inst
  • inner_product_space.has_sizeof_inst
  • inner_product_space.core.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
  • implicit_function_data.has_sizeof_inst
  • normed_group_hom.has_sizeof_inst
  • measure_theory.simple_func.has_sizeof_inst
  • bounded_continuous_function.has_sizeof_inst
  • times_cont_diff_bump_of_inner.has_sizeof_inst
  • times_cont_diff_bump.has_sizeof_inst
  • affine.simplex.has_sizeof_inst
  • convex_cone.has_sizeof_inst
  • urysohns.CU.has_sizeof_inst
  • measure_theory.content.has_sizeof_inst
  • enorm.has_sizeof_inst
  • seminorm.has_sizeof_inst
  • stieltjes_function.has_sizeof_inst
  • basis.smith_normal_form.has_sizeof_inst
  • category_theory.ProjectiveResolution.has_sizeof_inst
  • category_theory.is_split_coequalizer.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.pairwise.has_sizeof_inst
  • category_theory.pairwise.hom.has_sizeof_inst
  • category_theory.closed.has_sizeof_inst
  • category_theory.monoidal_closed.has_sizeof_inst
  • category_theory.cartesian_closed_functor.has_sizeof_inst
  • category_theory.sigma.sigma_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.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.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.monoidal_preadditive.has_sizeof_inst
  • category_theory.Mat_.has_sizeof_inst
  • category_theory.sieve.has_sizeof_inst
  • category_theory.grothendieck_topology.has_sizeof_inst
  • category_theory.pretopology.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
  • combinatorics.line.has_sizeof_inst
  • combinatorics.line.almost_mono.has_sizeof_inst
  • combinatorics.line.color_focused.has_sizeof_inst
  • simple_graph.has_sizeof_inst
  • simple_graph.dart.has_sizeof_inst
  • simple_graph.matching.has_sizeof_inst
  • simple_graph.subgraph.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
  • W_type.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
  • fin_enum.has_sizeof_inst
  • alist.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
  • pfunctor.approx.cofix_a.has_sizeof_inst
  • pfunctor.M_intl.has_sizeof_inst
  • mvpfunctor.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
  • indexed_partition.has_sizeof_inst
  • circle_deg1_lift.has_sizeof_inst
  • flow.has_sizeof_inst
  • subfield.has_sizeof_inst
  • intermediate_field.has_sizeof_inst
  • intermediate_field.insert.has_sizeof_inst
  • perfect_ring.has_sizeof_inst
  • affine.simplex.points_with_circumcenter_index.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
  • 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_bundle_core.has_sizeof_inst
  • times_cont_mdiff_map.has_sizeof_inst
  • smooth_add_monoid_morphism.has_sizeof_inst
  • smooth_monoid_morphism.has_sizeof_inst
  • derivation.has_sizeof_inst
  • left_invariant_derivation.has_sizeof_inst
  • diffeomorph.has_sizeof_inst
  • smooth_bump_function.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
  • free_product.word.has_sizeof_inst
  • free_product.word.pair.has_sizeof_inst
  • is_free_group.has_sizeof_inst
  • is_free_groupoid.has_sizeof_inst
  • dihedral_group.has_sizeof_inst
  • quaternion_group.has_sizeof_inst
  • quadratic_form.has_sizeof_inst
  • quadratic_form.isometry.has_sizeof_inst
  • measure_theory.vector_measure.has_sizeof_inst
  • measure_theory.jordan_decomposition.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.substructure.has_sizeof_inst
  • absolute_value.is_admissible.has_sizeof_inst
  • zsqrtd.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
  • hahn_series.has_sizeof_inst
  • hahn_series.summable_family.has_sizeof_inst
  • witt_vector.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
  • bounded_random.has_sizeof_inst
  • random.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
  • open_add_subgroup.has_sizeof_inst
  • open_subgroup.has_sizeof_inst
  • CompHaus.has_sizeof_inst
  • locally_constant.has_sizeof_inst
  • Profinite.has_sizeof_inst
  • discrete_quotient.has_sizeof_inst
  • CpltSepUniformSpace.has_sizeof_inst
  • continuous_map.homotopy.has_sizeof_inst
  • Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
  • topological_vector_bundle.trivialization.has_sizeof_inst
  • topological_vector_bundle_core.has_sizeof_inst
  • module_doc_info.has_sizeof_inst
  • ext_tactic_doc_entry.has_sizeof_inst
  • slim_check.total_function.has_sizeof
source
def sizeof {α : Sort u} [s : has_sizeof α] :
α → ℕ
Equations
source
def default.sizeof (α : Sort u) :
α → ℕ
Equations
source
@[instance]
def default_has_sizeof (α : Sort u) :
has_sizeof α
Equations
source
@[instance]
def nat.has_sizeof  :
has_sizeof ℕ
Equations
source
@[instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (α × β)
Equations
source
@[instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (α ⊕ β)
Equations
source
@[instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (psum α β)
Equations
source
@[instance]
def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
has_sizeof (sigma β)
Equations
source
@[instance]
def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
has_sizeof (psigma β)
Equations
source
@[instance]
def punit.has_sizeof  :
has_sizeof punit
Equations
source
@[instance]
def bool.has_sizeof  :
has_sizeof bool
Equations
source
@[instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :
has_sizeof (option α)
Equations
source
@[instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :
has_sizeof (list α)
Equations
source
@[instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :
has_sizeof (subtype p)
Equations
source
theorem nat_add_zero (n : ℕ) :
n + 0 = n
source
def combinator.I {α : Type u₁} (a : α) :
α
Equations
source
def combinator.K {α : Type u₁} {β : Type u₂} (a : α) (b : β) :
α
Equations
source
def combinator.S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) :
γ
Equations
source
inductive bin_tree (α : Type u) :
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.

source
def infer_instance {α : Sort u} [i : α] :
α

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

Equations