mathlib docs: 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.

source

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

Sort u

Gadget for optional parameter support.

source

def out_param (α : Sort u) :

Sort u

Gadget for marking output parameters in type classes.

source

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

α

source

inductive punit :

Sort u

star : punit

source

def unit :

Type

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

source

def unit.star :

unit

source

def thunk (α : Type u) :

Type u

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

source

inductive true :

Prop

intro : true

source

constant false :

Prop

source

constant 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

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

a

source

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

b

source

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

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

a ∨ b

source

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

a ∨ b

source

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

Type (max u v)

fst : α
snd : β c.fst

source

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

Sort (max 1 u v)

fst : α
snd : β c.fst

source

inductive bool :

Type

ff : bool
tt : bool

source

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

Sort (max 1 u)

val : α
property : p c.val

source

@[class]

inductive decidable (p : Prop) :

Type

is_false : Π (p : Prop), ¬p → decidable p
is_true : Π (p : Prop), p → decidable p

Instances

source

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

Sort (max u 1)

Equations

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

Instances

source

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

Sort (max u 1)

Equations

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

Instances

source

def decidable_eq (α : Sort u) :

Sort (max u 1)

Equations

decidable_eq α = decidable_rel eq

Instances

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

zero : ℕ
succ : ℕ → ℕ

source

structure unification_constraint :

Type (u+1)

α : Type ?
lhs : c.α
rhs : c.α

source

structure unification_hint :

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

pattern : unification_constraint
constraints : list unification_constraint

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

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

a ≥ b = (b ≤ a)

source

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

Prop

Equations

a > b = (b < a)

source

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

Prop

Equations

a ⊇ b = (b ⊆ a)

source

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

Prop

Equations

a ⊃ b = (b ⊂ a)

source

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

α

Equations

bit0 a = a + a

source

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

α

Equations

bit1 a = bit0 a + 1

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

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

source

@[instance]

def nat.has_zero :

has_zero ℕ

Equations

nat.has_zero = {zero := 0}

source

@[instance]

def nat.has_one :

has_one ℕ

Equations

nat.has_one = {one := 1}

source

@[instance]

def nat.has_add :

has_add ℕ

Equations

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

source

def std.priority.default :

ℕ

Equations

std.priority.default = 1000

source

def std.priority.max :

ℕ

Equations

std.priority.max = 4294967295

source

def nat.prio :

ℕ

Equations

nat.prio = std.priority.default + 100

source

def std.prec.max :

ℕ

Equations

std.prec.max = 1024

source

def std.prec.arrow :

ℕ

Equations

std.prec.arrow = 25

source

def std.prec.max_plus :

ℕ

Equations

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

source

@[class]

structure has_sizeof (α : Sort u) :

Sort (max 1 u)

sizeof : α → ℕ

Instances

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
doc_category.has_sizeof_inst
tactic_doc_entry.has_sizeof_inst
pempty.has_sizeof_inst
dlist.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
to_additive.value_type.has_sizeof_inst
parse_result.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
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
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
monoid.has_sizeof_inst
add_monoid.has_sizeof_inst
comm_monoid.has_sizeof_inst
add_comm_monoid.has_sizeof_inst
add_left_cancel_monoid.has_sizeof_inst
left_cancel_monoid.has_sizeof_inst
add_left_cancel_comm_monoid.has_sizeof_inst
left_cancel_comm_monoid.has_sizeof_inst
add_right_cancel_monoid.has_sizeof_inst
right_cancel_monoid.has_sizeof_inst
add_right_cancel_comm_monoid.has_sizeof_inst
right_cancel_comm_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
unique.has_sizeof_inst
units.has_sizeof_inst
add_units.has_sizeof_inst
mul_zero_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
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
bounded_distrib_lattice.has_sizeof_inst
has_compl.has_sizeof_inst
boolean_algebra.has_sizeof_inst
equiv.has_sizeof_inst
add_equiv.has_sizeof_inst
mul_equiv.has_sizeof_inst
distrib.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
ordered_comm_monoid.has_sizeof_inst
ordered_add_comm_monoid.has_sizeof_inst
linear_ordered_comm_monoid_with_zero.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_comm_group.has_sizeof_inst
nonneg_add_comm_group.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
division_ring.has_sizeof_inst
field.has_sizeof_inst
function.embedding.has_sizeof_inst
has_scalar.has_sizeof_inst
mul_action.has_sizeof_inst
distrib_mul_action.has_sizeof_inst
linear_ordered_field.has_sizeof_inst
multiset.has_sizeof
rel_hom.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
has_Sup.has_sizeof_inst
has_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
galois_insertion.has_sizeof_inst
galois_coinsertion.has_sizeof_inst
directed_order.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
semimodule.has_sizeof_inst
semimodule.core.has_sizeof_inst
submonoid.has_sizeof_inst
add_submonoid.has_sizeof_inst
has_vadd.has_sizeof_inst
has_vsub.has_sizeof_inst
add_action.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
subgroup.has_sizeof_inst
add_subgroup.has_sizeof_inst
mul_semiring_action.has_sizeof_inst
faithful_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
add_con.has_sizeof_inst
con.has_sizeof_inst
sub_mul_action.has_sizeof_inst
submodule.has_sizeof_inst
roption.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
tensor_product.compatible_smul.has_sizeof_inst
subsemiring.has_sizeof_inst
subring.has_sizeof_inst
algebra.has_sizeof_inst
alg_hom.has_sizeof_inst
alg_equiv.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
free_algebra.pre.has_sizeof_inst
category_theory.has_hom.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.is_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.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.reflects_isomorphisms.has_sizeof_inst
category_theory.groupoid.has_sizeof_inst
category_theory.unbundled_hom.has_sizeof_inst
category_theory.representable.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_pair.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.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
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
dfinsupp.pre.has_sizeof_inst
tactic.ring_exp.coeff.has_sizeof_inst
tactic.ring_exp.ex_type.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
CommRing.colimits.prequotient.has_sizeof_inst
AddCommGroup.colimits.prequotient.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
tactic.tfae.arrow.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.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
Mon.colimits.prequotient.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
filter.has_sizeof_inst
denumerable.has_sizeof_inst
filter_basis.has_sizeof_inst
filter.countable_filter_basis.has_sizeof_inst
free_magma.has_sizeof_inst
free_add_magma.has_sizeof_inst
normalization_monoid.has_sizeof_inst
gcd_monoid.has_sizeof_inst
category_theory.has_shift.has_sizeof_inst
category_theory.differential_object.has_sizeof_inst
category_theory.differential_object.hom.has_sizeof_inst
invertible.has_sizeof_inst
has_bracket.has_sizeof_inst
initial_seg.has_sizeof_inst
principal_seg.has_sizeof_inst
Well_order.has_sizeof_inst
tactic.decl_reducibility.has_sizeof_inst
ultrafilter.has_sizeof_inst
topological_space.has_sizeof_inst
homeomorph.has_sizeof_inst
pequiv.has_sizeof_inst
multilinear_map.has_sizeof_inst
alternating_map.has_sizeof_inst
dual_pair.has_sizeof_inst
bilin_form.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_algebra.morphism.has_sizeof_inst
lie_algebra.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
linear_ordered_comm_group_with_zero.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
star_algebra.has_sizeof_inst
continuous_map.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
add_group_with_zero_nhd.has_sizeof_inst
TopCommRing.has_sizeof_inst
uniform_space.core.has_sizeof_inst
uniform_space.has_sizeof_inst
continuous_linear_map.has_sizeof_inst
continuous_linear_equiv.has_sizeof_inst
local_equiv.has_sizeof_inst
local_homeomorph.has_sizeof_inst
Top.prelocal_predicate.has_sizeof_inst
Top.local_predicate.has_sizeof_inst
add_submonoid.localization_map.has_sizeof_inst
submonoid.localization_map.has_sizeof_inst
localization_map.has_sizeof_inst
algebraic_geometry.Scheme.has_sizeof_inst
cau_seq.is_complete.has_sizeof_inst
has_edist.has_sizeof_inst
emetric_space.has_sizeof_inst
has_dist.has_sizeof_inst
metric_space.has_sizeof_inst
has_continuous_inv'.has_sizeof_inst
complex.has_sizeof_inst
affine_map.has_sizeof_inst
has_norm.has_sizeof_inst
normed_group.has_sizeof_inst
normed_ring.has_sizeof_inst
normed_comm_ring.has_sizeof_inst
normed_field.has_sizeof_inst
nondiscrete_normed_field.has_sizeof_inst
normed_space.has_sizeof_inst
normed_algebra.has_sizeof_inst
isometric.has_sizeof_inst
continuous_multilinear_map.has_sizeof_inst
normed_linear_ordered_group.has_sizeof_inst
normed_linear_ordered_field.has_sizeof_inst
affine_equiv.has_sizeof_inst
normed_add_torsor.has_sizeof_inst
path.has_sizeof_inst
measurable_space.has_sizeof_inst
measurable_equiv.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.finite_spanning_sets_in.has_sizeof_inst
measure_theory.measure_space.has_sizeof_inst
composition.has_sizeof_inst
composition_as_set.has_sizeof_inst
implicit_function_data.has_sizeof_inst
linear_pmap.has_sizeof_inst
convex_cone.has_sizeof_inst
measure_theory.simple_func.has_sizeof_inst
is_R_or_C.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
enorm.has_sizeof_inst
quaternion_algebra.has_sizeof_inst
seminorm.has_sizeof_inst
category_theory.is_skeleton_of.has_sizeof_inst
category_theory.reflective.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.is_split_coequalizer.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.functorial.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.Monad.has_sizeof_inst
category_theory.Comonad.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.lax_monoidal.has_sizeof_inst
category_theory.simple.has_sizeof_inst
category_theory.quotient.has_sizeof_inst
category_theory.sigma.sigma_hom.has_sizeof_inst
category_theory.sieve.has_sizeof_inst
category_theory.grothendieck_topology.has_sizeof_inst
category_theory.pretopology.has_sizeof_inst
preorder_hom.has_sizeof_inst
closure_operator.has_sizeof_inst
partition.has_sizeof_inst
simple_graph.has_sizeof_inst
simple_graph.dart.has_sizeof_inst
simple_graph.matching.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
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
omega_complete_partial_order.has_sizeof_inst
omega_complete_partial_order.continuous_hom.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
valuation.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
zsqrtd.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
power_basis.has_sizeof_inst
perfect_ring.has_sizeof_inst
affine_subspace.has_sizeof_inst
affine.simplex.has_sizeof_inst
affine.simplex.points_with_circumcenter_index.has_sizeof_inst
bundle_trivialization.has_sizeof_inst
topological_fiber_bundle_core.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
smooth_add_monoid_morphism.has_sizeof_inst
smooth_monoid_morphism.has_sizeof_inst
lie_add_group_morphism.has_sizeof_inst
lie_group_morphism.has_sizeof_inst
times_cont_mdiff_map.has_sizeof_inst
times_diffeomorph.has_sizeof_inst
dihedral.has_sizeof_inst
semidirect_product.has_sizeof_inst
quadratic_form.has_sizeof_inst
quadratic_form.isometry.has_sizeof_inst
nonempty_fin_lin_ord.has_sizeof_inst
order.ideal.has_sizeof_inst
order.cofinal.has_sizeof_inst
derivation.has_sizeof_inst
pgame.has_sizeof_inst
pgame.restricted.has_sizeof_inst
pgame.relabelling.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
pgame.inv_ty.has_sizeof_inst
pSet.has_sizeof_inst
pSet.definable.has_sizeof_inst
bounded_random.has_sizeof_inst
random.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
abstract_completion.has_sizeof_inst
open_add_subgroup.has_sizeof_inst
open_subgroup.has_sizeof_inst
CompHaus.has_sizeof_inst
Profinite.has_sizeof_inst
CpltSepUniformSpace.has_sizeof_inst
premetric_space.has_sizeof_inst
Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
module_doc_info.has_sizeof_inst
ext_tactic_doc_entry.has_sizeof_inst
slim_check.total_function.has_sizeof