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

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

Gadget for optional parameter support.

def out_param (α : Sort u) :
Sort u

Gadget for marking output parameters in type classes.

def id_rhs (α : Sort u) (a : α) :
α
inductive punit  :
Sort u
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.

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)

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

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

structure prod (α : Type u) (β : Type v) :
Type (max u v)
  • fst : α
  • snd : β
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.

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.

theorem and.elim_left {a b : Prop} (h : a b) :
a
theorem and.elim_right {a b : Prop} (h : a b) :
b
def rfl {α : Sort u} {a : α} :
a = a
theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :
P b
theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :
a = c
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)
  • inl : Π (α : Type u) (β : Type v), α → α β
  • inr : Π (α : Type u) (β : Type v), β → α β
inductive psum (α : Sort u) (β : Sort v) :
Sort (max 1 u v)
  • inl : Π (α : Sort u) (β : Sort v), α → psum α β
  • inr : Π (α : Sort u) (β : Sort v), β → psum α β
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.

theorem or.intro_left {a : Prop} (b : Prop) (ha : a) :
a b
theorem or.intro_right (a : Prop) {b : Prop} (hb : b) :
a b
structure sigma {α : Type u} (β : α → Type v) :
Type (max u v)
  • fst : α
  • snd : β c.fst
structure psigma {α : Sort u} (β : α → Sort v) :
Sort (max 1 u v)
  • fst : α
  • snd : β c.fst
inductive bool  :
Type
structure subtype {α : Sort u} (p : α → Prop) :
Sort (max 1 u)
  • val : α
  • property : p c.val
@[class]
inductive decidable (p : Prop) :
Type
Instances
def decidable_pred {α : Sort u} (r : α → Prop) :
Sort (max u 1)
Equations
def decidable_rel {α : Sort u} (r : α → α → Prop) :
Sort (max u 1)
Equations
def decidable_eq (α : Sort u) :
Sort (max u 1)
Equations
inductive option (α : Type u) :
Type u
  • none : Π (α : Type u), option α
  • some : Π (α : Type u), α → option α
inductive list (T : Type u) :
Type u
  • nil : Π (T : Type u), list T
  • cons : Π (T : Type u), T → list Tlist T
inductive nat  :
Type
structure unification_constraint  :
Type (u+1)
  • α : Type ?
  • lhs : c.α
  • rhs : c.α
structure unification_hint  :
Type (max (u_1+1) (u_2+1))
@[ext, class]
structure has_zero (α : Type u) :
Type u
  • zero : α
Instances
@[class]
structure has_one (α : Type u) :
Type u
  • one : α
Instances
@[class]
structure has_add (α : Type u) :
Type u
  • add : α → α → α
Instances
@[class]
structure has_mul (α : Type u) :
Type u
  • mul : α → α → α
Instances
@[class]
structure has_dvd (α : Type u) :
Type u
  • dvd : α → α → Prop
Instances
@[class]
structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :
Type (max u v w)
  • andthen : α → β → σ
Instances
@[class]
structure has_equiv (α : Sort u) :
Sort (max 1 u)
  • equiv : α → α → Prop
Instances
@[class]
structure has_ssubset (α : Type u) :
Type u
  • ssubset : α → α → Prop
Instances
@[class]
structure has_sep (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
  • sep : (α → Prop)γ → γ
Instances
def ge {α : Type u} [has_le α] (a b : α) :
Prop
Equations
def gt {α : Type u} [has_lt α] (a b : α) :
Prop
Equations
  • a > b = (b < a)
def superset {α : Type u} [has_subset α] (a b : α) :
Prop
Equations
def ssuperset {α : Type u} [has_ssubset α] (a b : α) :
Prop
Equations
def bit0 {α : Type u} [s : has_add α] (a : α) :
α
Equations
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) :
α
Equations
@[class]
structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β] [has_singleton α β] :
Prop
  • insert_emptyc_eq : ∀ (x : α), {x} = {x}
Instances
def nat.add  :
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
Equations
def std.prec.max  :
Equations
Equations
@[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
  • 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
  • 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
  • unique.has_sizeof_inst
  • units.has_sizeof_inst
  • add_units.has_sizeof_inst
  • mul_zero_class.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
  • 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
  • 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
  • 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
  • division_ring.has_sizeof_inst
  • field.has_sizeof_inst
  • function.embedding.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
  • 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_comm_group.has_sizeof_inst
  • nonneg_add_comm_group.has_sizeof_inst
  • invertible.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
  • linear_ordered_field.has_sizeof_inst
  • multiset.has_sizeof
  • 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
  • rel_hom.has_sizeof_inst
  • rel_embedding.has_sizeof_inst
  • rel_iso.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
  • smul_with_zero.has_sizeof_inst
  • mul_action_with_zero.has_sizeof_inst
  • semimodule.has_sizeof_inst
  • semimodule.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
  • 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
  • dfinsupp.pre.has_sizeof_inst
  • denumerable.has_sizeof_inst
  • preorder_hom.has_sizeof_inst
  • tactic.tfae.arrow.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.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.unbundled_hom.has_sizeof_inst
  • category_theory.groupoid.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.comma.has_sizeof_inst
  • category_theory.comma_morphism.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.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
  • tactic.ring_exp.coeff.has_sizeof_inst
  • tactic.ring_exp.ex_type.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
  • 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.reflective.has_sizeof_inst
  • category_theory.monadic_right_adjoint.has_sizeof_inst
  • category_theory.comonadic_left_adjoint.has_sizeof_inst
  • category_theory.is_skeleton_of.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
  • category_theory.functorial.has_sizeof_inst
  • category_theory.lax_monoidal.has_sizeof_inst
  • Module.colimits.prequotient.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
  • filter_basis.has_sizeof_inst
  • filter.countable_filter_basis.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
  • tactic.decl_reducibility.has_sizeof_inst
  • ultrafilter.has_sizeof_inst
  • topological_space.has_sizeof_inst
  • compact_exhaustion.has_sizeof_inst
  • homeomorph.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
  • 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
  • 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
  • linear_pmap.has_sizeof_inst
  • initial_seg.has_sizeof_inst
  • principal_seg.has_sizeof_inst
  • Well_order.has_sizeof_inst
  • linear_ordered_comm_group_with_zero.has_sizeof_inst
  • valuation.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
  • 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
  • boolean_ring.has_sizeof_inst
  • star_algebra.has_sizeof_inst
  • cau_seq.is_complete.has_sizeof_inst
  • real.has_sizeof_inst
  • uniform_space.core.has_sizeof_inst
  • uniform_space.has_sizeof_inst
  • has_edist.has_sizeof_inst
  • pseudo_emetric_space.has_sizeof_inst
  • emetric_space.has_sizeof_inst
  • shrinking_lemma.partial_refinement.has_sizeof_inst
  • has_dist.has_sizeof_inst
  • pseudo_metric_space.has_sizeof_inst
  • metric_space.has_sizeof_inst
  • continuous_linear_map.has_sizeof_inst
  • continuous_linear_equiv.has_sizeof_inst
  • has_continuous_inv'.has_sizeof_inst
  • complex.has_sizeof_inst
  • affine_map.has_sizeof_inst
  • has_norm.has_sizeof_inst
  • semi_normed_group.has_sizeof_inst
  • normed_group.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
  • isometric.has_sizeof_inst
  • linear_isometry.has_sizeof_inst
  • linear_isometry_equiv.has_sizeof_inst
  • normed_group_hom.has_sizeof_inst
  • local_equiv.has_sizeof_inst
  • local_homeomorph.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
  • semi_normed_add_torsor.has_sizeof_inst
  • normed_add_torsor.has_sizeof_inst
  • path.has_sizeof_inst
  • is_R_or_C.has_sizeof_inst
  • continuous_linear_map.nonlinear_right_inverse.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_space.has_sizeof_inst
  • measure_theory.measure.finite_spanning_sets_in.has_sizeof_inst
  • has_measurable_pow.has_sizeof_inst
  • is_CHSH_tuple.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
  • TopCommRing.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
  • nonempty_fin_lin_ord.has_sizeof_inst
  • composition.has_sizeof_inst
  • composition_as_set.has_sizeof_inst
  • implicit_function_data.has_sizeof_inst
  • ring_invo.has_sizeof_inst
  • sesq_form.has_sizeof_inst
  • measure_theory.simple_func.has_sizeof_inst
  • has_inner.has_sizeof_inst
  • inner_product_space.has_sizeof_inst
  • inner_product_space.core.has_sizeof_inst
  • times_cont_diff_bump_of_inner.has_sizeof_inst
  • times_cont_diff_bump.has_sizeof_inst
  • power_basis.has_sizeof_inst
  • convex_cone.has_sizeof_inst
  • bounded_continuous_function.has_sizeof_inst
  • enorm.has_sizeof_inst
  • quaternion_algebra.has_sizeof_inst
  • seminorm.has_sizeof_inst
  • semidirect_product.has_sizeof_inst
  • category_theory.additive_category.has_sizeof_inst
  • category_theory.is_kernel_pair.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.sigma.sigma_hom.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
  • Mon_.has_sizeof_inst
  • Mon_.hom.has_sizeof_inst
  • CommMon_.has_sizeof_inst
  • Mod.has_sizeof_inst
  • Mod.hom.has_sizeof_inst
  • category_theory.quotient.has_sizeof_inst
  • category_theory.sieve.has_sizeof_inst
  • category_theory.grothendieck_topology.has_sizeof_inst
  • category_theory.pretopology.has_sizeof_inst
  • closure_operator.has_sizeof_inst
  • category_theory.triangulated.triangle.has_sizeof_inst
  • category_theory.triangulated.triangle_morphism.has_sizeof_inst
  • category_theory.with_terminal.has_sizeof_inst
  • category_theory.with_initial.has_sizeof_inst
  • partition.has_sizeof_inst
  • quiver.has_sizeof_inst
  • quiver.total.has_sizeof_inst
  • quiver.path.has_sizeof_inst
  • quiver.arborescence.has_sizeof_inst
  • quiver.has_reverse.has_sizeof_inst
  • simple_graph.has_sizeof_inst
  • simple_graph.dart.has_sizeof_inst
  • simple_graph.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
  • ε_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
  • 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
  • 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
  • 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
  • times_cont_mdiff_map.has_sizeof_inst
  • diffeomorph.has_sizeof_inst
  • smooth_bump_function.has_sizeof_inst
  • smooth_bump_covering.has_sizeof_inst
  • is_free_group.has_sizeof_inst
  • dihedral_group.has_sizeof_inst
  • quaternion_group.has_sizeof_inst
  • quadratic_form.has_sizeof_inst
  • quadratic_form.isometry.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
  • derivation.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.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
  • locally_constant.has_sizeof_inst
  • Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
  • urysohns.CU.has_sizeof_inst
  • topological_vector_bundle.trivialization.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
def default.sizeof (α : Sort u) :
α →
Equations
@[instance]
def default_has_sizeof (α : Sort u) :
Equations
@[instance]
Equations
@[instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof × β)
Equations
@[instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof β)
Equations
@[instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
Equations
@[instance]
def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
@[instance]
def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :
Equations
theorem nat_add_zero (n : ) :
n + 0 = n
def combinator.I {α : Type u₁} (a : α) :
α
Equations
def combinator.K {α : Type u₁} {β : Type u₂} (a : α) (b : β) :
α
Equations
def combinator.S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) :
γ
Equations
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.

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

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

Equations