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
@[nolint]
def rfl {α : Sort u} {a : α} :
a = a
theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :
P b
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 : β self.fst
structure psigma {α : Sort u} (β : α → Sort v) :
Sort (max 1 u v)
  • fst : α
  • snd : β self.fst
inductive bool  :
Type
structure subtype {α : Sort u} (p : α → Prop) :
Sort (max 1 u)
  • val : α
  • property : p self.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 : self.α
  • rhs : self.α
structure unification_hint  :
Type (max (u_1+1) (u_2+1))
@[class]
structure has_dvd (α : Type u) :
Type u
  • dvd : α → α → Prop
Instances
@[class]
structure has_mod (α : Type u) :
Type u
  • mod : α → α → α
Instances
@[class]
structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :
Type (max u v w)
  • andthen : α → β → σ
Instances
@[class]
structure has_union (α : Type u) :
Type u
  • union : α → α → α
Instances
@[class]
structure has_inter (α : Type u) :
Type u
  • inter : α → α → α
Instances
@[class]
structure has_sdiff (α : Type u) :
Type u
  • sdiff : α → α → α
Instances
@[class]
structure has_equiv (α : Sort u) :
Sort (max 1 u)
  • equiv : α → α → Prop
Instances
@[class]
structure has_subset (α : Type u) :
Type u
  • subset : α → α → Prop
Instances
@[class]
structure has_ssubset (α : Type u) :
Type u
  • ssubset : α → α → Prop
Instances
@[class]
structure has_emptyc (α : Type u) :
Type u
  • emptyc : α
Instances
@[class]
structure has_insert (α : out_param (Type u)) (γ : Type v) :
Type (max u v)
  • insert : α → γ → γ
Instances
@[class]
structure has_singleton (α : out_param (Type u)) (β : Type v) :
Type (max u v)
  • singleton : α → β
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
@[protected]
def nat.add  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
Equations
@[protected]
def nat.prio  :
Equations
def std.prec.max  :
Equations
Equations
@[class]
structure has_sizeof (α : Sort u) :
Sort (max 1 u)
  • sizeof : α →
Instances
  • default_has_sizeof
  • 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
  • widget.mouse_event_kind.has_sizeof_inst
  • dlist.has_sizeof_inst
  • doc_category.has_sizeof_inst
  • tactic_doc_entry.has_sizeof_inst
  • pempty.has_sizeof_inst
  • rbnode.has_sizeof_inst
  • rbnode.color.has_sizeof_inst
  • random_gen.has_sizeof_inst
  • std_gen.has_sizeof_inst
  • io.error.has_sizeof_inst
  • io.mode.has_sizeof_inst
  • io.process.stdio.has_sizeof_inst
  • io.process.spawn_args.has_sizeof_inst
  • monad_io.has_sizeof_inst
  • monad_io_terminal.has_sizeof_inst
  • monad_io_net_system.has_sizeof_inst
  • monad_io_file_system.has_sizeof_inst
  • monad_io_environment.has_sizeof_inst
  • monad_io_process.has_sizeof_inst
  • monad_io_random.has_sizeof_inst
  • lint_verbosity.has_sizeof_inst
  • function.has_uncurry.has_sizeof_inst
  • to_additive.value_type.has_sizeof_inst
  • parse_result.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
  • unique.has_sizeof_inst
  • equiv.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
  • bounded_order.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
  • has_vadd.has_sizeof_inst
  • has_scalar.has_sizeof_inst
  • semigroup.has_sizeof_inst
  • add_semigroup.has_sizeof_inst
  • comm_semigroup.has_sizeof_inst
  • add_comm_semigroup.has_sizeof_inst
  • left_cancel_semigroup.has_sizeof_inst
  • add_left_cancel_semigroup.has_sizeof_inst
  • right_cancel_semigroup.has_sizeof_inst
  • add_right_cancel_semigroup.has_sizeof_inst
  • mul_one_class.has_sizeof_inst
  • add_zero_class.has_sizeof_inst
  • add_monoid.has_sizeof_inst
  • monoid.has_sizeof_inst
  • add_comm_monoid.has_sizeof_inst
  • comm_monoid.has_sizeof_inst
  • add_left_cancel_monoid.has_sizeof_inst
  • left_cancel_monoid.has_sizeof_inst
  • add_right_cancel_monoid.has_sizeof_inst
  • right_cancel_monoid.has_sizeof_inst
  • add_cancel_monoid.has_sizeof_inst
  • cancel_monoid.has_sizeof_inst
  • add_cancel_comm_monoid.has_sizeof_inst
  • cancel_comm_monoid.has_sizeof_inst
  • div_inv_monoid.has_sizeof_inst
  • sub_neg_monoid.has_sizeof_inst
  • group.has_sizeof_inst
  • add_group.has_sizeof_inst
  • comm_group.has_sizeof_inst
  • add_comm_group.has_sizeof_inst
  • units.has_sizeof_inst
  • add_units.has_sizeof_inst
  • mul_zero_class.has_sizeof_inst
  • semigroup_with_zero.has_sizeof_inst
  • mul_zero_one_class.has_sizeof_inst
  • monoid_with_zero.has_sizeof_inst
  • cancel_monoid_with_zero.has_sizeof_inst
  • comm_monoid_with_zero.has_sizeof_inst
  • cancel_comm_monoid_with_zero.has_sizeof_inst
  • group_with_zero.has_sizeof_inst
  • comm_group_with_zero.has_sizeof_inst
  • fun_like.has_sizeof_inst
  • zero_hom.has_sizeof_inst
  • zero_hom_class.has_sizeof_inst
  • add_hom.has_sizeof_inst
  • add_hom_class.has_sizeof_inst
  • add_monoid_hom.has_sizeof_inst
  • add_monoid_hom_class.has_sizeof_inst
  • one_hom.has_sizeof_inst
  • one_hom_class.has_sizeof_inst
  • mul_hom.has_sizeof_inst
  • mul_hom_class.has_sizeof_inst
  • monoid_hom.has_sizeof_inst
  • monoid_hom_class.has_sizeof_inst
  • monoid_with_zero_hom.has_sizeof_inst
  • monoid_with_zero_hom_class.has_sizeof_inst
  • function.embedding.has_sizeof_inst
  • distrib.has_sizeof_inst
  • non_unital_non_assoc_semiring.has_sizeof_inst
  • non_unital_semiring.has_sizeof_inst
  • non_assoc_semiring.has_sizeof_inst
  • semiring.has_sizeof_inst
  • ring_hom.has_sizeof_inst
  • ring_hom_class.has_sizeof_inst
  • comm_semiring.has_sizeof_inst
  • ring.has_sizeof_inst
  • comm_ring.has_sizeof_inst
  • invertible.has_sizeof_inst
  • has_abs.has_sizeof_inst
  • has_pos_part.has_sizeof_inst
  • has_neg_part.has_sizeof_inst
  • add_equiv.has_sizeof_inst
  • mul_equiv.has_sizeof_inst
  • rel_hom.has_sizeof_inst
  • rel_hom_class.has_sizeof_inst
  • rel_embedding.has_sizeof_inst
  • rel_iso.has_sizeof_inst
  • tactic.interactive.mono_cfg.has_sizeof_inst
  • tactic.interactive.mono_selection.has_sizeof_inst
  • order_hom.has_sizeof_inst
  • 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
  • has_ordered_sub.has_sizeof_inst
  • ordered_add_comm_group.has_sizeof_inst
  • ordered_comm_group.has_sizeof_inst
  • linear_ordered_add_comm_group.has_sizeof_inst
  • linear_ordered_add_comm_group_with_top.has_sizeof_inst
  • linear_ordered_comm_group.has_sizeof_inst
  • add_comm_group.positive_cone.has_sizeof_inst
  • add_comm_group.total_positive_cone.has_sizeof_inst
  • 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
  • ring.positive_cone.has_sizeof_inst
  • ring.total_positive_cone.has_sizeof_inst
  • canonically_ordered_comm_semiring.has_sizeof_inst
  • add_action.has_sizeof_inst
  • mul_action.has_sizeof_inst
  • distrib_mul_action.has_sizeof_inst
  • mul_distrib_mul_action.has_sizeof_inst
  • has_Sup.has_sizeof_inst
  • has_Inf.has_sizeof_inst
  • complete_semilattice_Sup.has_sizeof_inst
  • complete_semilattice_Inf.has_sizeof_inst
  • complete_lattice.has_sizeof_inst
  • complete_linear_order.has_sizeof_inst
  • complete_distrib_lattice.has_sizeof_inst
  • complete_boolean_algebra.has_sizeof_inst
  • directed_order.has_sizeof_inst
  • galois_insertion.has_sizeof_inst
  • galois_coinsertion.has_sizeof_inst
  • multiset.has_sizeof
  • tactic.interactive.rep_arity.has_sizeof_inst
  • division_ring.has_sizeof_inst
  • field.has_sizeof_inst
  • linear_ordered_field.has_sizeof_inst
  • expr_lens.dir.has_sizeof_inst
  • finset.has_sizeof_inst
  • fintype.has_sizeof_inst
  • smul_with_zero.has_sizeof_inst
  • mul_action_with_zero.has_sizeof_inst
  • encodable.has_sizeof_inst
  • euclidean_domain.has_sizeof_inst
  • rat.has_sizeof_inst
  • module.has_sizeof_inst
  • module.core.has_sizeof_inst
  • set_like.has_sizeof_inst
  • submonoid.has_sizeof_inst
  • add_submonoid.has_sizeof_inst
  • conditionally_complete_lattice.has_sizeof_inst
  • conditionally_complete_linear_order.has_sizeof_inst
  • conditionally_complete_linear_order_bot.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
  • ring_equiv.has_sizeof_inst
  • tactic.abel.normalize_mode.has_sizeof_inst
  • floor_semiring.has_sizeof_inst
  • floor_ring.has_sizeof_inst
  • has_star.has_sizeof_inst
  • has_involutive_star.has_sizeof_inst
  • star_monoid.has_sizeof_inst
  • star_add_monoid.has_sizeof_inst
  • star_ring.has_sizeof_inst
  • star_ordered_ring.has_sizeof_inst
  • star_module.has_sizeof_inst
  • absolute_value.has_sizeof_inst
  • cau_seq.is_complete.has_sizeof_inst
  • real.has_sizeof_inst
  • Q1a.X.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
  • tactic.tfae.arrow.has_sizeof_inst
  • locally_finite_order.has_sizeof_inst
  • quiver.has_sizeof_inst
  • prefunctor.has_sizeof_inst
  • quiver.total.has_sizeof_inst
  • quiver.path.has_sizeof_inst
  • quiver.arborescence.has_sizeof_inst
  • quiver.has_reverse.has_sizeof_inst
  • category_theory.category_struct.has_sizeof_inst
  • category_theory.category.has_sizeof_inst
  • equiv_functor.has_sizeof_inst
  • bifunctor.has_sizeof_inst
  • is_lawful_bifunctor.has_sizeof_inst
  • two_sided_inverse.has_sizeof_inst
  • bool2.has_sizeof_inst
  • partition.has_sizeof_inst
  • indexed_partition.has_sizeof_inst
  • X.has_sizeof_inst
  • has_quotient.has_sizeof_inst
  • subgroup.has_sizeof_inst
  • add_subgroup.has_sizeof_inst
  • add_con.has_sizeof_inst
  • con.has_sizeof_inst
  • subsemiring.has_sizeof_inst
  • subring.has_sizeof_inst
  • mul_semiring_action.has_sizeof_inst
  • mul_action_hom.has_sizeof_inst
  • distrib_mul_action_hom.has_sizeof_inst
  • mul_semiring_action_hom.has_sizeof_inst
  • linear_map.has_sizeof_inst
  • linear_map.compatible_smul.has_sizeof_inst
  • linear_equiv.has_sizeof_inst
  • sub_mul_action.has_sizeof_inst
  • submodule.has_sizeof_inst
  • normalization_monoid.has_sizeof_inst
  • gcd_monoid.has_sizeof_inst
  • normalized_gcd_monoid.has_sizeof_inst
  • dfinsupp.pre.has_sizeof_inst
  • finsupp.has_sizeof_inst
  • denumerable.has_sizeof_inst
  • part.has_sizeof_inst
  • omega_complete_partial_order.has_sizeof_inst
  • omega_complete_partial_order.continuous_hom.has_sizeof_inst
  • algebra.has_sizeof_inst
  • alg_hom.has_sizeof_inst
  • alg_equiv.has_sizeof_inst
  • linear_ordered_comm_group_with_zero.has_sizeof_inst
  • mynnreal.has_sizeof_inst
  • module_doc_info.has_sizeof_inst
  • ext_tactic_doc_entry.has_sizeof_inst
def sizeof {α : Sort u} [s : has_sizeof α] :
α →
Equations
@[protected]
def default.sizeof (α : Sort u) :
α →
Equations
@[protected, instance]
def default_has_sizeof (α : Sort u) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof × β)
Equations
@[protected, instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof β)
Equations
@[protected, instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
Equations
@[protected, instance]
def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
@[protected, instance]
def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[protected, instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :
Equations
@[protected, instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :
Equations
theorem nat_add_zero (n : ) :
n + 0 = n
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