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

source

def opt_param (α : Sort u) :

α → Sort u

Gadget for optional parameter support.

source

def out_param :

Sort u → Sort u

Gadget for marking output parameters in type classes.

source

def id_rhs (α : Sort u) :

α → α

source

inductive punit :

Sort u

star : punit

source

def unit :

Type

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

source

def unit.star :

unit

source

def thunk :

Type u → Type u

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

source

inductive true :

Prop

intro : true

source

constant false :

Prop

source

constant empty :

Type

source

def not :

Prop → Prop

source

inductive eq {α : Sort u} :

α → α → Prop

refl : ∀ {α : Sort u} (a : α), a = a

source

inductive heq {α : Sort u} (a : α) {β : Sort u} :

β → Prop

refl : ∀ {α : Sort u} (a : α), a == a

Heterogeneous equality. It's 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.

source

structure prod :

Type u → Type v → Type (max u v)

fst : α
snd : β

source

structure pprod :

Sort u → Sort v → Sort (max 1 u v)

fst : α
snd : β

Similar to prod, but α and β can be propositions. We use this type internally to automatically generate the brec_on recursor.

source

structure and :

Prop → Prop → Prop

left : a
right : b

source

def and.elim_left {a b : Prop} :

a ∧ b → a

Equations

_ = _

source

def and.elim_right {a b : Prop} :

a ∧ b → b

Equations

_ = _

source

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

a = a

Equations

rfl = _

source

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

a = b → P a → P b

source

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

a = b → b = c → a = c

source

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

a = b → b = a

source

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

a == a

Equations

heq.rfl = _

source

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

a == a' → a = a'

source

inductive sum :

Type u → Type v → Type (max u v)

inl : Π (α : Type u) (β : Type v), α → α ⊕ β
inr : Π (α : Type u) (β : Type v), β → α ⊕ β

source

inductive psum :

Sort u → Sort v → Sort (max 1 u v)

inl : Π (α : Sort u) (β : Sort v), α → psum α β
inr : Π (α : Sort u) (β : Sort v), β → psum α β

source

inductive or :

Prop → Prop → Prop

inl : ∀ (a b : Prop), a → a ∨ b
inr : ∀ (a b : Prop), b → a ∨ b

source

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

a → a ∨ b

Equations

_ = _

source

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

b → a ∨ b

Equations

_ = _

source

structure sigma {α : Type u} :

(α → Type v) → Type (max u v)

fst : α
snd : β c.fst

source

structure psigma {α : Sort u} :

(α → Sort v) → Sort (max 1 u v)

fst : α
snd : β c.fst

source

inductive bool :

Type

ff : bool
tt : bool

source

structure subtype {α : Sort u} :

(α → Prop) → Sort (max 1 u)

val : α
property : p c.val

source

@[class]

inductive decidable :

Prop → Type

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

Instances

source

def decidable_pred {α : Sort u} :

(α → Prop) → Sort (max u 1)

Equations

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

Instances

source

def decidable_rel {α : Sort u} :

(α → α → Prop) → Sort (max u 1)

Equations

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

Instances

source

def decidable_eq :

Sort u → Sort (max u 1)

Equations

decidable_eq α = decidable_rel eq

Instances

source

inductive option :

Type u → Type u

none : Π (α : Type u), option α
some : Π (α : Type u), α → option α

source

inductive list :

Type u → Type u

nil : Π (T : Type u), list T
cons : Π (T : Type u), T → list T → list T

source

inductive nat :

Type

zero : ℕ
succ : ℕ → ℕ

source

structure unification_constraint :

Type (u+1)

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

source

structure unification_hint :

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

pattern : unification_constraint
constraints : list unification_constraint

source

@[ext, class]

structure has_zero :

Type u → Type u

zero : α

Instances

source

@[class]

structure has_one :

Type u → Type u

one : α

Instances

source

@[class]

structure has_add :

Type u → Type u

add : α → α → α

Instances

source

@[class]

structure has_mul :

Type u → Type u

mul : α → α → α

Instances

source

@[class]

structure has_inv :

Type u → Type u

inv : α → α

Instances

source

@[class]

structure has_neg :

Type u → Type u

neg : α → α

Instances

source

@[class]

structure has_sub :

Type u → Type u

sub : α → α → α

Instances

source

@[class]

structure has_div :

Type u → Type u

div : α → α → α

Instances

source

@[class]

structure has_dvd :

Type u → Type u

dvd : α → α → Prop

Instances

source

@[class]

structure has_mod :

Type u → Type u

mod : α → α → α

Instances

source

@[class]

structure has_le :

Type u → Type u

le : α → α → Prop

Instances

source

@[class]

structure has_lt :

Type u → Type u

lt : α → α → Prop

Instances

source

@[class]

structure has_append :

Type u → Type u

append : α → α → α

Instances

source

@[class]

structure has_andthen :

Type u → Type v → out_param (Type w) → Type (max u v w)

andthen : α → β → σ

Instances

source

@[class]

structure has_union :

Type u → Type u

union : α → α → α

Instances

source

@[class]

structure has_inter :

Type u → Type u

inter : α → α → α

Instances

source

@[class]

structure has_sdiff :

Type u → Type u

sdiff : α → α → α

Instances

source

@[class]

structure has_equiv :

Sort u → Sort (max 1 u)

equiv : α → α → Prop

Instances

source

@[class]

structure has_subset :

Type u → Type u

subset : α → α → Prop

Instances

source

@[class]

structure has_ssubset :

Type u → Type u

ssubset : α → α → Prop

Instances

source

@[class]

structure has_emptyc :

Type u → Type u

emptyc : α

Instances

source

@[class]

structure has_insert :

out_param (Type u) → Type v → Type (max u v)

insert : α → γ → γ

Instances

source

@[class]

structure has_singleton :

out_param (Type u) → Type v → Type (max u v)

singleton : α → β

Instances

source

@[class]

structure has_sep :

out_param (Type u) → Type v → Type (max u v)

sep : (α → Prop) → γ → γ

Instances

source

@[class]

structure has_mem :

out_param (Type u) → Type v → Type (max u v)

mem : α → γ → Prop

Instances

source

@[class]

structure has_pow :

Type u → Type v → Type (max u v)

pow : α → β → α

Instances

source

def ge {α : Type u} [has_le α] :

α → α → Prop

Equations

a ≥ b = (b ≤ a)

source

def gt {α : Type u} [has_lt α] :

α → α → Prop

Equations

a > b = (b < a)

source

def superset {α : Type u} [has_subset α] :

α → α → Prop

Equations

a ⊇ b = (b ⊆ a)

source

def ssuperset {α : Type u} [has_ssubset α] :

α → α → Prop

Equations

a ⊃ b = (b ⊂ a)

source

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

α → α

Equations

bit0 a = a + a

source

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

α → α

Equations

bit1 a = bit0 a + 1

source

@[class]

structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β] [has_singleton α β] :

Type

insert_emptyc_eq : ∀ (x : α), {x} = {x}

Instances

source

def nat.add :

ℕ → ℕ → ℕ

Equations

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

source

@[instance]

def nat.has_zero :

has_zero ℕ

Equations

nat.has_zero = {zero := 0}

source

@[instance]

def nat.has_one :

has_one ℕ

Equations

nat.has_one = {one := 1}

source

@[instance]

def nat.has_add :

has_add ℕ

Equations

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

source

def std.priority.default :

ℕ

Equations

std.priority.default = 1000

source

def std.priority.max :

ℕ

Equations

std.priority.max = 4294967295

source

def nat.prio :

ℕ

Equations

nat.prio = std.priority.default + 100

source

def std.prec.max :

ℕ

Equations

std.prec.max = 1024

source

def std.prec.arrow :

ℕ

Equations

std.prec.arrow = 25

source

def std.prec.max_plus :

ℕ

Equations

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

source

@[class]

structure has_sizeof :

Sort u → Sort (max 1 u)

sizeof : α → ℕ

Instances

default_has_sizeof
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
fin.has_sizeof_inst
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
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
param_info.has_sizeof_inst
fun_info.has_sizeof_inst
subsingleton_info.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
widget.mouse_event_kind.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
dlist.has_sizeof_inst
doc_category.has_sizeof_inst
tactic_doc_entry.has_sizeof_inst
pempty.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
parse_result.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
unique.has_sizeof_inst
to_additive.value_type.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
units.has_sizeof_inst
add_units.has_sizeof_inst
add_monoid_hom.has_sizeof_inst
monoid_hom.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
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
distrib.has_sizeof_inst
semiring.has_sizeof_inst
ring_hom.has_sizeof_inst
comm_semiring.has_sizeof_inst
ring.has_sizeof_inst
comm_ring.has_sizeof_inst
domain.has_sizeof_inst
integral_domain.has_sizeof_inst
ordered_comm_monoid.has_sizeof_inst
ordered_add_comm_monoid.has_sizeof_inst
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
equiv.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_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
finset.has_sizeof_inst
fintype.has_sizeof_inst
add_equiv.has_sizeof_inst
mul_equiv.has_sizeof_inst
encodable.has_sizeof_inst
euclidean_domain.has_sizeof_inst
rat.has_sizeof_inst
tactic.abel.normalize_mode.has_sizeof_inst
has_vadd.has_sizeof_inst
has_vsub.has_sizeof_inst
add_action.has_sizeof_inst
add_torsor.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
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
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
ring_equiv.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.has_limit.has_sizeof_inst
category_theory.limits.has_limits_of_shape.has_sizeof_inst
category_theory.limits.has_limits.has_sizeof_inst
category_theory.limits.has_colimit.has_sizeof_inst
category_theory.limits.has_colimits_of_shape.has_sizeof_inst
category_theory.limits.has_colimits.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.has_lift.has_sizeof_inst
category_theory.strong_epi.has_sizeof_inst
category_theory.limits.mono_factorisation.has_sizeof_inst
category_theory.limits.is_image.has_sizeof_inst
category_theory.limits.has_image.has_sizeof_inst
category_theory.limits.has_images.has_sizeof_inst
category_theory.limits.has_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_strong_epi_mono_factorisations.has_sizeof_inst
category_theory.limits.has_strong_epi_images.has_sizeof_inst
category_theory.limits.has_zero_morphisms.has_sizeof_inst
category_theory.limits.has_zero_object.has_sizeof_inst
category_theory.limits.has_kernels.has_sizeof_inst
category_theory.limits.has_cokernels.has_sizeof_inst
category_theory.preadditive.has_sizeof_inst
submodule.has_sizeof_inst
finsupp.has_sizeof_inst
linear_equiv.has_sizeof_inst
Module.has_sizeof_inst
add_con.has_sizeof_inst
con.has_sizeof_inst
subsemiring.has_sizeof_inst
algebra.has_sizeof_inst
alg_hom.has_sizeof_inst
alg_equiv.has_sizeof_inst
subalgebra.has_sizeof_inst
Algebra.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
omega.ee.has_sizeof_inst
omega.ee_state.has_sizeof_inst
omega.int.preterm.has_sizeof_inst
omega.int.preform.has_sizeof_inst
omega.nat.preterm.has_sizeof_inst
omega.nat.preform.has_sizeof_inst
CommRing.colimits.prequotient.has_sizeof_inst
AddCommGroup.colimits.prequotient.has_sizeof_inst
category_theory.limits.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.fin_category.has_sizeof_inst
category_theory.limits.bicone.has_sizeof_inst
category_theory.limits.has_biproduct.has_sizeof_inst
category_theory.limits.has_biproducts_of_shape.has_sizeof_inst
category_theory.limits.has_finite_biproducts.has_sizeof_inst
category_theory.limits.binary_bicone.has_sizeof_inst
category_theory.limits.has_binary_biproduct.has_sizeof_inst
category_theory.limits.has_binary_biproducts.has_sizeof_inst
category_theory.non_preadditive_abelian.has_sizeof_inst
category_theory.abelian.has_sizeof_inst
category_theory.monoidal_category.has_sizeof_inst
Mon.colimits.prequotient.has_sizeof_inst
invertible.has_sizeof_inst
linear_action.has_sizeof_inst
denumerable.has_sizeof_inst
initial_seg.has_sizeof_inst
principal_seg.has_sizeof_inst
Well_order.has_sizeof_inst
normalization_monoid.has_sizeof_inst
gcd_monoid.has_sizeof_inst
roption.has_sizeof_inst
unique_factorization_domain.has_sizeof_inst
unique_irreducible_factorization.has_sizeof_inst
pequiv.has_sizeof_inst
bilin_form.has_sizeof_inst
dfinsupp.pre.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
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
filter_basis.has_sizeof_inst
filter.countable_filter_basis.has_sizeof_inst
free_magma.has_sizeof_inst
free_add_magma.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
category_theory.has_shift.has_sizeof_inst
category_theory.differential_object.has_sizeof_inst
category_theory.differential_object.hom.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
linear_ordered_comm_group_with_zero.has_sizeof_inst
linear_recurrence.has_sizeof_inst
ordered_semimodule.has_sizeof_inst
cau_seq.is_complete.has_sizeof_inst
complex.has_sizeof_inst
affine_subspace.has_sizeof_inst
affine_map.has_sizeof_inst
uniform_space.core.has_sizeof_inst
uniform_space.has_sizeof_inst
has_edist.has_sizeof_inst
emetric_space.has_sizeof_inst
tactic.tfae.arrow.has_sizeof_inst
add_group_with_zero_nhd.has_sizeof_inst
has_dist.has_sizeof_inst
metric_space.has_sizeof_inst
continuous_linear_map.has_sizeof_inst
continuous_linear_equiv.has_sizeof_inst
has_norm.has_sizeof_inst
normed_group.has_sizeof_inst
normed_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
local_equiv.has_sizeof_inst
local_homeomorph.has_sizeof_inst
multilinear_map.has_sizeof_inst
continuous_multilinear_map.has_sizeof_inst
path.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
expr_lens.dir.has_sizeof_inst
normed_add_torsor.has_sizeof_inst
enorm.has_sizeof_inst
has_inner.has_sizeof_inst
inner_product_space.has_sizeof_inst
inner_product_space.core.has_sizeof_inst
category_theory.closed.has_sizeof_inst
category_theory.monoidal_closed.has_sizeof_inst
category_theory.lax_monoidal_functor.has_sizeof_inst
category_theory.monoidal_functor.has_sizeof_inst
category_theory.braided_category.has_sizeof_inst
category_theory.symmetric_category.has_sizeof_inst
category_theory.braided_functor.has_sizeof_inst
category_theory.connected.has_sizeof_inst
category_theory.functorial.has_sizeof_inst
category_theory.limits.diagram_of_cones.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
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
simple_graph.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
nzsnum.has_sizeof_inst
snum.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
fin2.has_sizeof_inst
fin2.is_lt.has_sizeof_inst
mvfunctor.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
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
W.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
zsqrtd.has_sizeof_inst
circle_deg1_lift.has_sizeof_inst
perfect_field.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
lie_add_group_morphism.has_sizeof_inst
lie_group_morphism.has_sizeof_inst
affine.simplex.has_sizeof_inst
affine.simplex.points_with_circumcenter_index.has_sizeof_inst
add_submonoid.localization_map.has_sizeof_inst
submonoid.localization_map.has_sizeof_inst
semidirect_product.has_sizeof_inst
dual_pair.has_sizeof_inst
quadratic_form.has_sizeof_inst
quadratic_form.isometry.has_sizeof_inst
ring_invo.has_sizeof_inst
sesq_form.has_sizeof_inst
tensor_algebra.pre.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.simple_func.has_sizeof_inst
preorder_hom.has_sizeof_inst
nonempty_fin_lin_ord.has_sizeof_inst
order.ideal.has_sizeof_inst
order.cofinal.has_sizeof_inst
derivation.has_sizeof_inst
localization_map.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
abstract_completion.has_sizeof_inst
open_add_subgroup.has_sizeof_inst
open_subgroup.has_sizeof_inst
TopCommRing.has_sizeof_inst
CpltSepUniformSpace.has_sizeof_inst
premetric_space.has_sizeof_inst
Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
Top.sheaf.has_sizeof_inst
module_doc_info.has_sizeof_inst
ext_tactic_doc_entry.has_sizeof_inst

source

def sizeof {α : Sort u} [s : has_sizeof α] :

α → ℕ

Equations

sizeof = has_sizeof.sizeof

source

def default.sizeof (α : Sort u) :

α → ℕ

Equations

default.sizeof α a = 0

source

@[instance]

def default_has_sizeof (α : Sort u) :

has_sizeof α

Equations

default_has_sizeof α = {sizeof := default.sizeof α}

source

@[instance]

def nat.has_sizeof :

has_sizeof ℕ

Equations

nat.has_sizeof = {sizeof := nat.sizeof}

source

@[instance]

def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :

has_sizeof (α × β)

Equations

prod.has_sizeof α β = {sizeof := prod.sizeof _inst_2}

source

@[instance]

def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :

has_sizeof (α ⊕ β)

Equations

sum.has_sizeof α β = {sizeof := sum.sizeof _inst_2}

source

@[instance]

def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :

has_sizeof (psum α β)

Equations

psum.has_sizeof α β = {sizeof := psum.sizeof _inst_2}

source

@[instance]

def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :

has_sizeof (sigma β)

Equations

sigma.has_sizeof α β = {sizeof := sigma.sizeof (λ (a : α), _inst_2 a)}

source

@[instance]

def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :

has_sizeof (psigma β)

Equations

psigma.has_sizeof α β = {sizeof := psigma.sizeof (λ (a : α), _inst_2 a)}

source

@[instance]

def punit.has_sizeof :

has_sizeof punit

Equations

punit.has_sizeof = {sizeof := punit.sizeof}

source

@[instance]

def bool.has_sizeof :

has_sizeof bool

Equations

bool.has_sizeof = {sizeof := bool.sizeof}

source

@[instance]

def option.has_sizeof (α : Type u) [has_sizeof α] :

has_sizeof (option α)

Equations

option.has_sizeof α = {sizeof := option.sizeof _inst_1}

source

@[instance]

def list.has_sizeof (α : Type u) [has_sizeof α] :

has_sizeof (list α)

Equations

list.has_sizeof α = {sizeof := list.sizeof _inst_1}

source

@[instance]

def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :

has_sizeof (subtype p)

Equations

subtype.has_sizeof p = {sizeof := subtype.sizeof p}

source

theorem nat_add_zero (n : ℕ) :

n + 0 = n

source

def combinator.I {α : Type u₁} :

α → α

Equations

combinator.I a = a

source

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

α → β → α

Equations

combinator.K a b = a

source

def combinator.S {α : Type u₁} {β : Type u₂} {γ : Type u₃} :

(α → β → γ) → (α → β) → α → γ

Equations

combinator.S x y z = x z (y z)

source

inductive bin_tree :

Type u → Type u

empty : Π (α : Type u), bin_tree α
leaf : Π (α : Type u), α → bin_tree α
node : Π (α : Type u), bin_tree α → bin_tree α → bin_tree α

Auxiliary datatype for #[ ... ] notation. #[1, 2, 3, 4] is notation for

bin_tree.node (bin_tree.node (bin_tree.leaf 1) (bin_tree.leaf 2)) (bin_tree.node (bin_tree.leaf 3) (bin_tree.leaf 4))

We use this notation to input long sequences without exhausting the system stack space. Later, we define a coercion from bin_tree into list.

source

def add_succ_defeq_succ_add_hint :

ℕ → ℕ → ℕ → unification_hint

Equations

add_succ_defeq_succ_add_hint x y z = {pattern := x + y.succ =?= z.succ, constraints := [z =?= x + y]}

source

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

α

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

Equations

infer_instance = i

mathlib documentation

core.init.core

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​core

General documentation

Additional documentation

Library

core.init.core