mathlib documentation

core.init.core

def id_delta {α : Sort u} :
α → α

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) :
α → Sort u

Gadget for optional parameter support.

def out_param  :
Sort uSort u

Gadget for marking output parameters in type classes.

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

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 uType 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

constant false  :
Prop

constant empty  :
Type

def not  :
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} :
α → α → 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 uType vType (max u v)
  • fst : α
  • snd : β

structure pprod  :
Sort uSort vSort (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  :
Prop → 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.

def and.elim_left {a b : Prop} :
a b → a

def and.elim_right {a b : Prop} :
a b → b

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

theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} :
a = bP aP b

theorem eq.trans {α : Sort u} {a b c : α} :
a = bb = ca = c

theorem eq.symm {α : Sort u} {a b : α} :
a = bb = a

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

theorem eq_of_heq {α : Sort u} {a a' : α} :
a == a'a = a'

inductive sum  :
Type uType vType (max u v)
  • inl : Π (α : Type u) (β : Type v), α → α β
  • inr : Π (α : Type u) (β : Type v), β → α β

inductive psum  :
Sort uSort vSort (max 1 u v)
  • inl : Π (α : Sort u) (β : Sort v), α → psum α β
  • inr : Π (α : Sort u) (β : Sort v), β → psum α β

inductive or  :
Prop → 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.

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

def or.intro_right (a : Prop) {b : Prop} :
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} :
(α → Prop)Sort (max 1 u)
  • val : α
  • property : p c.val

@[class]
inductive decidable  :
Prop → Type

Instances
def decidable_eq  :
Sort uSort (max u 1)

Equations
Instances
inductive option  :
Type uType u
  • none : Π (α : Type u), option α
  • some : Π (α : Type u), α → option α

inductive list  :
Type uType 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 uType u
  • zero : α

Instances
@[class]
structure has_add  :
Type uType u
  • add : α → α → α

Instances
@[class]
structure has_dvd  :
Type uType u
  • dvd : α → α → Prop

Instances
@[class]
structure has_andthen  :
Type uType vout_param (Type w)Type (max u v w)
  • andthen : α → β → «σ»

Instances
@[class]
structure has_equiv  :
Sort uSort (max 1 u)
  • equiv : α → α → Prop

Instances
@[class]
structure has_ssubset  :
Type uType u
  • ssubset : α → α → Prop

Instances
@[class]
structure has_insert  :
out_param (Type u)Type vType (max u v)
  • insert : α → γ → γ

Instances
@[class]
structure has_singleton  :
out_param (Type u)Type vType (max u v)
  • singleton : α → β

Instances
@[class]
structure has_sep  :
out_param (Type u)Type vType (max u v)
  • sep : (α → Prop)γ → γ

Instances
def ge {α : Type u} [has_le α] :
α → α → Prop

Equations
def gt {α : Type u} [has_lt α] :
α → α → Prop

Equations
  • a > b = (b < a)
def superset {α : Type u} [has_subset α] :
α → α → Prop

Equations
def ssuperset {α : Type u} [has_ssubset α] :
α → α → Prop

Equations
def bit0 {α : Type u} [s : has_add α] :
α → α

Equations
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] :
α → α

Equations
@[class]
structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β] [has_singleton α β] :
Type
  • 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 uSort (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
  • decidable_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
  • 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
  • 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
  • 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
  • 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
  • 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
  • add_equiv.has_sizeof_inst
  • mul_equiv.has_sizeof_inst
  • ordered_comm_monoid.has_sizeof_inst
  • ordered_add_comm_monoid.has_sizeof_inst
  • canonically_ordered_add_monoid.has_sizeof_inst
  • canonically_linear_ordered_add_monoid.has_sizeof_inst
  • ordered_cancel_add_comm_monoid.has_sizeof_inst
  • ordered_cancel_comm_monoid.has_sizeof_inst
  • ordered_add_comm_group.has_sizeof_inst
  • ordered_comm_group.has_sizeof_inst
  • decidable_linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
  • decidable_linear_ordered_add_comm_group.has_sizeof_inst
  • nonneg_add_comm_group.has_sizeof_inst
  • ordered_semiring.has_sizeof_inst
  • linear_ordered_semiring.has_sizeof_inst
  • decidable_linear_ordered_semiring.has_sizeof_inst
  • ordered_ring.has_sizeof_inst
  • linear_ordered_ring.has_sizeof_inst
  • linear_ordered_comm_ring.has_sizeof_inst
  • decidable_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
  • linear_ordered_field.has_sizeof_inst
  • discrete_linear_ordered_field.has_sizeof_inst
  • multiset.has_sizeof
  • function.embedding.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
  • 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
  • fintype.has_sizeof_inst
  • has_vadd.has_sizeof_inst
  • has_vsub.has_sizeof_inst
  • add_action.has_sizeof_inst
  • add_torsor.has_sizeof_inst
  • encodable.has_sizeof_inst
  • euclidean_domain.has_sizeof_inst
  • rat.has_sizeof_inst
  • tactic.abel.normalize_mode.has_sizeof_inst
  • submonoid.has_sizeof_inst
  • add_submonoid.has_sizeof_inst
  • subgroup.has_sizeof_inst
  • add_subgroup.has_sizeof_inst
  • has_scalar.has_sizeof_inst
  • mul_action.has_sizeof_inst
  • distrib_mul_action.has_sizeof_inst
  • semimodule.has_sizeof_inst
  • semimodule.core.has_sizeof_inst
  • linear_map.has_sizeof_inst
  • add_con.has_sizeof_inst
  • con.has_sizeof_inst
  • submodule.has_sizeof_inst
  • finsupp.has_sizeof_inst
  • linear_equiv.has_sizeof_inst
  • ring_equiv.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
  • roption.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.ess_surj.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.groupoid.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.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.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
  • 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.wide_pullback_shape.hom.has_sizeof_inst
  • category_theory.limits.wide_pushout_shape.hom.has_sizeof_inst
  • category_theory.regular_mono.has_sizeof_inst
  • category_theory.normal_mono.has_sizeof_inst
  • category_theory.regular_epi.has_sizeof_inst
  • category_theory.normal_epi.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.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
  • 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
  • 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
  • conditionally_complete_lattice.has_sizeof_inst
  • conditionally_complete_linear_order.has_sizeof_inst
  • conditionally_complete_linear_order_bot.has_sizeof_inst
  • filter.has_sizeof_inst
  • denumerable.has_sizeof_inst
  • filter_basis.has_sizeof_inst
  • filter.countable_filter_basis.has_sizeof_inst
  • dfinsupp.pre.has_sizeof_inst
  • free_magma.has_sizeof_inst
  • free_add_magma.has_sizeof_inst
  • normalization_monoid.has_sizeof_inst
  • gcd_monoid.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
  • 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
  • linear_action.has_sizeof_inst
  • initial_seg.has_sizeof_inst
  • principal_seg.has_sizeof_inst
  • Well_order.has_sizeof_inst
  • pequiv.has_sizeof_inst
  • multilinear_map.has_sizeof_inst
  • dual_pair.has_sizeof_inst
  • bilin_form.has_sizeof_inst
  • has_bracket.has_sizeof_inst
  • lie_ring.has_sizeof_inst
  • lie_algebra.has_sizeof_inst
  • lie_algebra.morphism.has_sizeof_inst
  • lie_algebra.equiv.has_sizeof_inst
  • lie_subalgebra.has_sizeof_inst
  • lie_module.has_sizeof_inst
  • lie_submodule.has_sizeof_inst
  • linear_ordered_comm_group_with_zero.has_sizeof_inst
  • linear_recurrence.has_sizeof_inst
  • ordered_semimodule.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
  • tactic.decl_reducibility.has_sizeof_inst
  • topological_space.has_sizeof_inst
  • continuous_map.has_sizeof_inst
  • homeomorph.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
  • complex.has_sizeof_inst
  • affine_subspace.has_sizeof_inst
  • affine_map.has_sizeof_inst
  • has_edist.has_sizeof_inst
  • emetric_space.has_sizeof_inst
  • has_dist.has_sizeof_inst
  • metric_space.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
  • 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
  • normed_add_torsor.has_sizeof_inst
  • enorm.has_sizeof_inst
  • ring_invo.has_sizeof_inst
  • sesq_form.has_sizeof_inst
  • is_R_or_C.has_sizeof_inst
  • has_inner.has_sizeof_inst
  • inner_product_space.has_sizeof_inst
  • inner_product_space.core.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.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.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.reflective.has_sizeof_inst
  • category_theory.monadic_right_adjoint.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.sieve.has_sizeof_inst
  • category_theory.grothendieck_topology.has_sizeof_inst
  • category_theory.is_skeleton_of.has_sizeof_inst
  • simple_graph.has_sizeof_inst
  • partition.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
  • 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
  • preorder_hom.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.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
  • 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
  • subfield.has_sizeof_inst
  • intermediate_field.has_sizeof_inst
  • intermediate_field.insert.has_sizeof_inst
  • perfect_field.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
  • 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
  • side.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
  • 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
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₁} :
α → α

Equations
def combinator.K {α : Type u₁} {β : Type u₂} :
α → β → α

Equations
def combinator.S {α : Type u₁} {β : Type u₂} {γ : Type u₃} :
(α → β → γ)(α → β)α → γ

Equations
inductive bin_tree  :
Type uType 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 {α : Type u} [i : α] :
α

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

Equations