core / init.core - mathlib3 docs

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

(id_delta t) =?= t
t =?= (id_delta t)
(id_delta t) =?= s IF (unfold_of t) =?= s
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

@[reducible]

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

Sort u

Gadget for optional parameter support.

source

@[reducible]

def out_param (α : Sort u) :

Sort u

Gadget for marking output parameters in type classes.

source

@[reducible]

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

α

id_rhs is an auxiliary declaration used in the equation compiler to address performance issues when proving equational lemmas. The equation compiler uses it as a marker.

source

structure punit :

Sort u

Instances for punit

source

@[reducible]

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

@[reducible]

def unit.star :

unit

source

@[reducible]

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

structure true :

Prop

Instances for true

source

inductive false :

Prop

Instances for false

source

inductive empty :

Type

Instances for empty

source

def not (a : Prop) :

Prop

Logical not.

not P, with notation ¬ P, is the Prop which is true if and only if P is false. It is internally represented as P → false, so one way to prove a goal ⊢ ¬ P is to use intro h, which gives you a new hypothesis h : P and the goal ⊢ false.

A hypothesis h : ¬ P can be used in term mode as a function, so if w : P then h w : false.

Related mathlib tactic: contrapose.

Instances for not

source

inductive eq {α : Sort u} (a : α) :

α → Prop

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

Instances for eq

source

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

β → Prop

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

Heterogeneous equality.

Its purpose is to write down equalities between terms whose types are not definitionally equal. For example, given x : vector α n and y : vector α (0+n), x = y doesn't typecheck but x == y does.

If you have a goal ⊢ x == y, your first instinct should be to ask (either yourself, or on zulip) if something has gone wrong already. If you really do need to follow this route, you may find the lemmas eq_rec_heq and eq_mpr_heq useful.

source

structure prod (α : Type u) (β : Type v) :

Type (max u v)

fst : α
snd : β

Instances for prod

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.

Instances for pprod

source

structure and (a b : Prop) :

Prop

left : a
right : b

Logical and.

and P Q, with notation P ∧ Q, is the Prop which is true precisely when P and Q are both true.

To prove a goal ⊢ P ∧ Q, you can use the tactic split, which gives two separate goals ⊢ P and ⊢ Q.

Given a hypothesis h : P ∧ Q, you can use the tactic cases h with hP hQ to obtain two new hypotheses hP : P and hQ : Q. See also the obtain or rcases tactics in mathlib.

Instances for and

source

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

a

source

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

b

source

@[nolint]

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

a = a

source

theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :

P b

source

@[trans]

theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :

a = c

source

@[symm]

theorem eq.symm {α : Sort u} {a b : α} (h : a = b) :

b = a

source

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

a == a

source

theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') :

a = a'

source

inductive sum (α : Type u) (β : Type v) :

Type (max u v)

inl : Π {α : Type u} {β : Type v}, α → α ⊕ β
inr : Π {α : Type u} {β : Type v}, β → α ⊕ β

Instances for sum

source

inductive psum (α : Sort u) (β : Sort v) :

Sort (max 1 u v)

inl : Π {α : Sort u} {β : Sort v}, α → psum α β
inr : Π {α : Sort u} {β : Sort v}, β → psum α β

Instances for psum

source

inductive or (a b : Prop) :

Prop

inl : ∀ {a b : Prop}, a → a ∨ b
inr : ∀ {a b : Prop}, b → a ∨ b

Logical or.

or P Q, with notation P ∨ Q, is the proposition which is true if and only if P or Q is true.

To prove a goal ⊢ P ∨ Q, if you know which alternative you want to prove, you can use the tactics left (which gives the goal ⊢ P) or right (which gives the goal ⊢ Q).

Given a hypothesis h : P ∨ Q and goal ⊢ R, the tactic cases h will give you two copies of the goal ⊢ R, with the hypothesis h : P in the first, and the hypothesis h : Q in the second.

Instances for or

or.decidable

source

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

a ∨ b

source

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

a ∨ b

source

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

Type (max u v)

fst : α
snd : β self.fst

Instances for sigma

source

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

Sort (max 1 u v)

fst : α
snd : β self.fst

Instances for psigma

source

inductive bool :

Type

ff : bool
tt : bool

Instances for bool

source

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

Sort (max 1 u)

val : α
property : p self.val

Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description.

Instances for subtype

source

@[class]

inductive decidable (p : Prop) :

Type

is_false : Π {p : Prop}, ¬p → decidable p
is_true : Π {p : Prop}, p → decidable p

Instances of this typeclass

Instances of other typeclasses for decidable

source

@[reducible]

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

Sort (max u 1)

Equations

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

source

@[reducible]

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

Sort (max u 1)

Equations

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

source

@[reducible]

def decidable_eq (α : Sort u) :

Sort (max u 1)

Equations

decidable_eq α = decidable_rel eq

source

inductive option (α : Type u) :

Type u

none : Π {α : Type u}, option α
some : Π {α : Type u}, α → option α

Instances for option

source

inductive list (T : Type u) :

Type u

nil : Π {T : Type u}, list T
cons : Π {T : Type u}, T → list T → list T

Instances for list

source

inductive nat :

Type

zero : ℕ
succ : ℕ → ℕ

Instances for nat

source

structure unification_constraint :

Type (u+1)

α : Type ?
lhs : self.α
rhs : self.α

Instances for unification_constraint

unification_constraint.inhabited

source

structure unification_hint :

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

pattern : unification_constraint
constraints : list unification_constraint

Instances for unification_hint

unification_hint.inhabited

source

@[ext, class]

structure has_zero (α : Type u) :

Type u

zero : α

Instances of this typeclass

source

@[class]

structure has_one (α : Type u) :

Type u

one : α

Instances of this typeclass

source

@[class]

structure has_add (α : Type u) :

Type u

add : α → α → α

Instances of this typeclass

source

@[class]

structure has_mul (α : Type u) :

Type u

mul : α → α → α

Instances of this typeclass

source

@[class]

structure has_inv (α : Type u) :

Type u

inv : α → α

Instances of this typeclass

source

@[class]

structure has_neg (α : Type u) :

Type u

neg : α → α

Instances of this typeclass

source

@[class]

structure has_sub (α : Type u) :

Type u

sub : α → α → α

Instances of this typeclass

source

@[class]

structure has_div (α : Type u) :

Type u

div : α → α → α

Instances of this typeclass

source

@[class]

structure has_dvd (α : Type u) :

Type u

dvd : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_mod (α : Type u) :

Type u

mod : α → α → α

Instances of this typeclass

source

@[ext, class]

structure has_le (α : Type u) :

Type u

le : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_lt (α : Type u) :

Type u

lt : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_append (α : Type u) :

Type u

append : α → α → α

Instances of this typeclass

source

@[class]

structure has_andthen (α : Type u) (β : Type v) (σ : out_param (Type w)) :

Type (max u v w)

andthen : α → β → σ

Instances of this typeclass

source

@[class]

structure has_union (α : Type u) :

Type u

union : α → α → α

Instances of this typeclass

source

@[class]

structure has_inter (α : Type u) :

Type u

inter : α → α → α

Instances of this typeclass

source

@[class]

structure has_sdiff (α : Type u) :

Type u

sdiff : α → α → α

Instances of this typeclass

source

@[class]

structure has_equiv (α : Sort u) :

Sort (max 1 u)

equiv : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_subset (α : Type u) :

Type u

subset : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_ssubset (α : Type u) :

Type u

ssubset : α → α → Prop

Instances of this typeclass

source

@[class]

structure has_emptyc (α : Type u) :

Type u

emptyc : α

Instances of this typeclass

source

@[class]

structure has_insert (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

insert : α → γ → γ

Instances of this typeclass

source

@[class]

structure has_singleton (α : out_param (Type u)) (β : Type v) :

Type (max u v)

singleton : α → β

Instances of this typeclass

source

@[class]

structure has_sep (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

sep : (α → Prop) → γ → γ

Type class used to implement the notation { a ∈ c | p a }

Instances of this typeclass

source

@[class]

structure has_mem (α : out_param (Type u)) (γ : Type v) :

Type (max u v)

mem : α → γ → Prop

Type class for set-like membership

Instances of this typeclass

source

@[class]

structure has_pow (α : Type u) (β : Type v) :

Type (max u v)

pow : α → β → α

Instances of this typeclass

source

@[reducible]

def ge {α : Type u} [has_le α] (a b : α) :

Prop

Equations

a ≥ b = (b ≤ a)

source

@[reducible]

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

Prop

Equations

a > b = (b < a)

source

@[reducible]

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

Prop

Equations

a ⊇ b = (b ⊆ a)

source

@[reducible]

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

Prop

Equations

a ⊃ b = (b ⊂ a)

source

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

α

Equations

bit0 a = a + a

Instances for bit0

source

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

α

Equations

bit1 a = bit0 a + 1

Instances for bit1

source

@[class]

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

Prop

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

Instances of this typeclass

source

@[protected]

def nat.add :

ℕ → ℕ → ℕ

Equations

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

source

@[protected, instance]

def nat.has_zero :

has_zero ℕ

Equations

nat.has_zero = {zero := 0}

source

@[protected, instance]

def nat.has_one :

has_one ℕ

Equations

nat.has_one = {one := 1}

source

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

@[protected]

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 :

ℕ

This def is "max + 10". It can be used e.g. for postfix operations that should be stronger than application.

Equations

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

source

@[class]

structure has_sizeof (α : Sort u) :

Sort (max 1 u)

sizeof : α → ℕ

Instances of this typeclass

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
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
feature_search.feature_cfg.has_sizeof_inst
feature_search.predictor_type.has_sizeof_inst
feature_search.predictor_cfg.has_sizeof_inst
doc_category.has_sizeof_inst
tactic_doc_entry.has_sizeof_inst
dlist.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
function.has_uncurry.has_sizeof_inst
to_additive.value_type.has_sizeof_inst
lint_verbosity.has_sizeof_inst
tactic.explode.status.has_sizeof_inst
auto.auto_config.has_sizeof_inst
auto.case_option.has_sizeof_inst
tactic.itauto.and_kind.has_sizeof_inst
tactic.itauto.prop.has_sizeof_inst
tactic.itauto.proof.has_sizeof_inst
can_lift.has_sizeof_inst
norm_cast.label.has_sizeof_inst
_nest_1_1._nest_1_1.tactic.tactic_script._mut_.has_sizeof_inst
_nest_1_1.tactic.tactic_script.has_sizeof_inst
_nest_1_1.list.tactic.tactic_script.has_sizeof_inst
tactic.tactic_script.has_sizeof_inst
simps_cfg.has_sizeof_inst
applicative_transformation.has_sizeof_inst
traversable.has_sizeof_inst
is_lawful_traversable.has_sizeof_inst
tactic.suggest.head_symbol_match.has_sizeof_inst
has_vadd.has_sizeof_inst
has_vsub.has_sizeof_inst
has_smul.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
has_involutive_neg.has_sizeof_inst
has_involutive_inv.has_sizeof_inst
div_inv_monoid.has_sizeof_inst
sub_neg_monoid.has_sizeof_inst
neg_zero_class.has_sizeof_inst
sub_neg_zero_monoid.has_sizeof_inst
inv_one_class.has_sizeof_inst
div_inv_one_monoid.has_sizeof_inst
subtraction_monoid.has_sizeof_inst
division_monoid.has_sizeof_inst
subtraction_comm_monoid.has_sizeof_inst
division_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
has_nat_cast.has_sizeof_inst
add_monoid_with_one.has_sizeof_inst
add_comm_monoid_with_one.has_sizeof_inst
has_int_cast.has_sizeof_inst
add_group_with_one.has_sizeof_inst
add_comm_group_with_one.has_sizeof_inst
unique.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
embedding_like.has_sizeof_inst
equiv_like.has_sizeof_inst
equiv.has_sizeof_inst
add_equiv.has_sizeof_inst
add_equiv_class.has_sizeof_inst
mul_equiv.has_sizeof_inst
mul_equiv_class.has_sizeof_inst
distrib.has_sizeof_inst
left_distrib_class.has_sizeof_inst
right_distrib_class.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
non_unital_comm_semiring.has_sizeof_inst
comm_semiring.has_sizeof_inst
has_distrib_neg.has_sizeof_inst
non_unital_non_assoc_ring.has_sizeof_inst
non_unital_ring.has_sizeof_inst
non_assoc_ring.has_sizeof_inst
ring.has_sizeof_inst
non_unital_comm_ring.has_sizeof_inst
comm_ring.has_sizeof_inst
has_compl.has_sizeof_inst
has_sup.has_sizeof_inst
has_inf.has_sizeof_inst
is_nonstrict_strict_order.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
has_himp.has_sizeof_inst
has_hnot.has_sizeof_inst
generalized_heyting_algebra.has_sizeof_inst
generalized_coheyting_algebra.has_sizeof_inst
heyting_algebra.has_sizeof_inst
coheyting_algebra.has_sizeof_inst
biheyting_algebra.has_sizeof_inst
generalized_boolean_algebra.has_sizeof_inst
boolean_algebra.has_sizeof_inst
non_unital_ring_hom.has_sizeof_inst
non_unital_ring_hom_class.has_sizeof_inst
ring_hom.has_sizeof_inst
ring_hom_class.has_sizeof_inst
ring_equiv.has_sizeof_inst
ring_equiv_class.has_sizeof_inst
rat.has_sizeof_inst
has_rat_cast.has_sizeof_inst
division_semiring.has_sizeof_inst
division_ring.has_sizeof_inst
semifield.has_sizeof_inst
field.has_sizeof_inst
function.embedding.has_sizeof_inst
add_action.has_sizeof_inst
mul_action.has_sizeof_inst
smul_zero_class.has_sizeof_inst
distrib_smul.has_sizeof_inst
distrib_mul_action.has_sizeof_inst
mul_distrib_mul_action.has_sizeof_inst
invertible.has_sizeof_inst
equiv_functor.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
order_iso_class.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_add_comm_monoid_with_top.has_sizeof_inst
ordered_cancel_add_comm_monoid.has_sizeof_inst
ordered_cancel_comm_monoid.has_sizeof_inst
linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
linear_ordered_cancel_comm_monoid.has_sizeof_inst
ordered_add_comm_group.has_sizeof_inst
ordered_comm_group.has_sizeof_inst
linear_ordered_add_comm_group.has_sizeof_inst
linear_ordered_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
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
zero_le_one_class.has_sizeof_inst
linear_ordered_comm_monoid_with_zero.has_sizeof_inst
ordered_semiring.has_sizeof_inst
ordered_comm_semiring.has_sizeof_inst
ordered_ring.has_sizeof_inst
ordered_comm_ring.has_sizeof_inst
strict_ordered_semiring.has_sizeof_inst
strict_ordered_comm_semiring.has_sizeof_inst
strict_ordered_ring.has_sizeof_inst
strict_ordered_comm_ring.has_sizeof_inst
linear_ordered_semiring.has_sizeof_inst
linear_ordered_comm_semiring.has_sizeof_inst
linear_ordered_ring.has_sizeof_inst
linear_ordered_comm_ring.has_sizeof_inst
canonically_ordered_comm_semiring.has_sizeof_inst
has_abs.has_sizeof_inst
has_pos_part.has_sizeof_inst
has_neg_part.has_sizeof_inst
linear_ordered_comm_group_with_zero.has_sizeof_inst
mul_semiring_action.has_sizeof_inst
linear_ordered_semifield.has_sizeof_inst
linear_ordered_field.has_sizeof_inst
expr_lens.dir.has_sizeof_inst
set_like.has_sizeof_inst
has_star.has_sizeof_inst
star_mem_class.has_sizeof_inst
has_involutive_star.has_sizeof_inst
star_semigroup.has_sizeof_inst
star_add_monoid.has_sizeof_inst
star_ring.has_sizeof_inst
star_hom_class.has_sizeof_inst
multiset.has_sizeof
tactic.interactive.rep_arity.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
order.frame.has_sizeof_inst
order.coframe.has_sizeof_inst
complete_distrib_lattice.has_sizeof_inst
complete_boolean_algebra.has_sizeof_inst
galois_insertion.has_sizeof_inst
galois_coinsertion.has_sizeof_inst
finset.has_sizeof_inst
fintype.has_sizeof_inst
nonneg_hom_class.has_sizeof_inst
subadditive_hom_class.has_sizeof_inst
submultiplicative_hom_class.has_sizeof_inst
mul_le_add_hom_class.has_sizeof_inst
nonarchimedean_hom_class.has_sizeof_inst
add_group_seminorm_class.has_sizeof_inst
group_seminorm_class.has_sizeof_inst
add_group_norm_class.has_sizeof_inst
group_norm_class.has_sizeof_inst
ring_seminorm_class.has_sizeof_inst
ring_norm_class.has_sizeof_inst
mul_ring_seminorm_class.has_sizeof_inst
mul_ring_norm_class.has_sizeof_inst
tactic.positivity.order_rel.has_sizeof_inst
top_hom.has_sizeof_inst
bot_hom.has_sizeof_inst
bounded_order_hom.has_sizeof_inst
top_hom_class.has_sizeof_inst
bot_hom_class.has_sizeof_inst
bounded_order_hom_class.has_sizeof_inst
sup_hom.has_sizeof_inst
inf_hom.has_sizeof_inst
sup_bot_hom.has_sizeof_inst
inf_top_hom.has_sizeof_inst
lattice_hom.has_sizeof_inst
bounded_lattice_hom.has_sizeof_inst
sup_hom_class.has_sizeof_inst
inf_hom_class.has_sizeof_inst
sup_bot_hom_class.has_sizeof_inst
inf_top_hom_class.has_sizeof_inst
lattice_hom_class.has_sizeof_inst
bounded_lattice_hom_class.has_sizeof_inst
smul_with_zero.has_sizeof_inst
mul_action_with_zero.has_sizeof_inst
tactic.abel.normalize_mode.has_sizeof_inst
module.has_sizeof_inst
module.core.has_sizeof_inst
mul_action_hom.has_sizeof_inst
smul_hom_class.has_sizeof_inst
distrib_mul_action_hom.has_sizeof_inst
distrib_mul_action_hom_class.has_sizeof_inst
mul_semiring_action_hom.has_sizeof_inst
mul_semiring_action_hom_class.has_sizeof_inst
linear_map.has_sizeof_inst
semilinear_map_class.has_sizeof_inst
linear_map.compatible_smul.has_sizeof_inst
linear_equiv.has_sizeof_inst
semilinear_equiv_class.has_sizeof_inst
normalization_monoid.has_sizeof_inst
gcd_monoid.has_sizeof_inst
normalized_gcd_monoid.has_sizeof_inst
subsemigroup.has_sizeof_inst
add_subsemigroup.has_sizeof_inst
submonoid.has_sizeof_inst
add_submonoid.has_sizeof_inst
encodable.has_sizeof_inst
subgroup.has_sizeof_inst
add_subgroup.has_sizeof_inst
smul_mem_class.has_sizeof_inst
vadd_mem_class.has_sizeof_inst
sub_mul_action.has_sizeof_inst
submodule.has_sizeof_inst
dfinsupp.has_sizeof_inst
conditionally_complete_lattice.has_sizeof_inst
conditionally_complete_linear_order.has_sizeof_inst
conditionally_complete_linear_order_bot.has_sizeof_inst
finsupp.has_sizeof_inst
absolute_value.has_sizeof_inst
subsemiring.has_sizeof_inst
subring.has_sizeof_inst
algebra.has_sizeof_inst
alg_hom.has_sizeof_inst
alg_hom_class.has_sizeof_inst
non_unital_alg_hom.has_sizeof_inst
non_unital_alg_hom_class.has_sizeof_inst
non_unital_star_alg_hom.has_sizeof_inst
non_unital_star_alg_hom_class.has_sizeof_inst
star_alg_hom.has_sizeof_inst
star_alg_hom_class.has_sizeof_inst
star_alg_equiv.has_sizeof_inst
star_alg_equiv_class.has_sizeof_inst
locally_finite_order.has_sizeof_inst
locally_finite_order_top.has_sizeof_inst
locally_finite_order_bot.has_sizeof_inst
denumerable.has_sizeof_inst
flag.has_sizeof_inst
tactic.tfae.arrow.has_sizeof_inst
part.has_sizeof_inst
omega_complete_partial_order.has_sizeof_inst
omega_complete_partial_order.continuous_hom.has_sizeof_inst
add_con.has_sizeof_inst
con.has_sizeof_inst
tensor_product.compatible_smul.has_sizeof_inst
alg_equiv.has_sizeof_inst
alg_equiv_class.has_sizeof_inst
Sup_hom.has_sizeof_inst
Inf_hom.has_sizeof_inst
frame_hom.has_sizeof_inst
complete_lattice_hom.has_sizeof_inst
Sup_hom_class.has_sizeof_inst
Inf_hom_class.has_sizeof_inst
frame_hom_class.has_sizeof_inst
complete_lattice_hom_class.has_sizeof_inst
idem_semiring.has_sizeof_inst
idem_comm_semiring.has_sizeof_inst
has_kstar.has_sizeof_inst
kleene_algebra.has_sizeof_inst
tactic.ring.normalize_mode.has_sizeof_inst
tactic.ring.ring_nf_cfg.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
succ_order.has_sizeof_inst
pred_order.has_sizeof_inst
linear_pmap.has_sizeof_inst
has_quotient.has_sizeof_inst
has_bracket.has_sizeof_inst
basis.has_sizeof_inst
subalgebra.has_sizeof_inst
star_subalgebra.has_sizeof_inst
ring_con.has_sizeof_inst
euclidean_domain.has_sizeof_inst
valuation.has_sizeof_inst
valuation_class.has_sizeof_inst
initial_seg.has_sizeof_inst
principal_seg.has_sizeof_inst
Well_order.has_sizeof_inst
direct_sum.decomposition.has_sizeof_inst
add_torsor.has_sizeof_inst
affine_map.has_sizeof_inst
affine_equiv.has_sizeof_inst
affine_subspace.has_sizeof_inst
bilin_form.has_sizeof_inst
star_ordered_ring.has_sizeof_inst
filter.has_sizeof_inst
filter_basis.has_sizeof_inst
filter.countable_filter_basis.has_sizeof_inst
tactic.decl_reducibility.has_sizeof_inst
ultrafilter.has_sizeof_inst
topological_space.has_sizeof_inst
bornology.has_sizeof_inst
upper_set.has_sizeof_inst
lower_set.has_sizeof_inst
compact_exhaustion.has_sizeof_inst
homeomorph.has_sizeof_inst
floor_semiring.has_sizeof_inst
floor_ring.has_sizeof_inst
uniform_space.core.has_sizeof_inst
uniform_space.has_sizeof_inst
uniform_equiv.has_sizeof_inst
continuous_map.has_sizeof_inst
continuous_map_class.has_sizeof_inst
add_group_with_zero_nhd.has_sizeof_inst
group_topology.has_sizeof_inst
add_group_topology.has_sizeof_inst
ring_topology.has_sizeof_inst
subfield.has_sizeof_inst
canonically_linear_ordered_semifield.has_sizeof_inst
real.has_sizeof_inst
has_edist.has_sizeof_inst
pseudo_emetric_space.has_sizeof_inst
emetric_space.has_sizeof_inst
has_dist.has_sizeof_inst
pseudo_metric_space.has_sizeof_inst
has_nndist.has_sizeof_inst
metric_space.has_sizeof_inst
abstract_completion.has_sizeof_inst
complex.has_sizeof_inst
add_group_seminorm.has_sizeof_inst
group_seminorm.has_sizeof_inst
nonarch_add_group_seminorm.has_sizeof_inst
add_group_norm.has_sizeof_inst
group_norm.has_sizeof_inst
nonarch_add_group_norm.has_sizeof_inst
nonarch_add_group_seminorm_class.has_sizeof_inst
nonarch_add_group_norm_class.has_sizeof_inst
locally_bounded_map.has_sizeof_inst
locally_bounded_map_class.has_sizeof_inst
isometry_equiv.has_sizeof_inst
has_norm.has_sizeof_inst
has_nnnorm.has_sizeof_inst
seminormed_add_group.has_sizeof_inst
seminormed_group.has_sizeof_inst
normed_add_group.has_sizeof_inst
normed_group.has_sizeof_inst
seminormed_add_comm_group.has_sizeof_inst
seminormed_comm_group.has_sizeof_inst
normed_add_comm_group.has_sizeof_inst
normed_comm_group.has_sizeof_inst
normed_add_group_hom.has_sizeof_inst
non_unital_semi_normed_ring.has_sizeof_inst
semi_normed_ring.has_sizeof_inst
non_unital_normed_ring.has_sizeof_inst
normed_ring.has_sizeof_inst
normed_division_ring.has_sizeof_inst
semi_normed_comm_ring.has_sizeof_inst
normed_comm_ring.has_sizeof_inst
normed_field.has_sizeof_inst
nontrivially_normed_field.has_sizeof_inst
densely_normed_field.has_sizeof_inst
continuous_linear_map.has_sizeof_inst
continuous_semilinear_map_class.has_sizeof_inst
continuous_linear_equiv.has_sizeof_inst
continuous_semilinear_equiv_class.has_sizeof_inst
normed_space.has_sizeof_inst
normed_algebra.has_sizeof_inst
linear_isometry.has_sizeof_inst
semilinear_isometry_class.has_sizeof_inst
linear_isometry_equiv.has_sizeof_inst
semilinear_isometry_equiv_class.has_sizeof_inst
is_R_or_C.has_sizeof_inst
closure_operator.has_sizeof_inst
lower_adjoint.has_sizeof_inst
sign_type.has_sizeof_inst
affine.simplex.has_sizeof_inst
affine_basis.has_sizeof_inst
path.has_sizeof_inst
normed_ordered_add_group.has_sizeof_inst
normed_ordered_group.has_sizeof_inst
normed_linear_ordered_add_group.has_sizeof_inst
normed_linear_ordered_group.has_sizeof_inst
normed_linear_ordered_field.has_sizeof_inst
normed_add_torsor.has_sizeof_inst
affine_isometry.has_sizeof_inst
affine_isometry_equiv.has_sizeof_inst
local_equiv.has_sizeof_inst
topological_space.opens.has_sizeof_inst
topological_space.open_nhds_of.has_sizeof_inst
local_homeomorph.has_sizeof_inst
seminorm.has_sizeof_inst
seminorm_class.has_sizeof_inst
group_filter_basis.has_sizeof_inst
add_group_filter_basis.has_sizeof_inst
ring_filter_basis.has_sizeof_inst
module_filter_basis.has_sizeof_inst
multilinear_map.has_sizeof_inst
continuous_multilinear_map.has_sizeof_inst
has_inner.has_sizeof_inst
inner_product_space.has_sizeof_inst
inner_product_space.core.has_sizeof_inst
topological_space.closeds.has_sizeof_inst
topological_space.clopens.has_sizeof_inst
topological_space.compacts.has_sizeof_inst
topological_space.nonempty_compacts.has_sizeof_inst
topological_space.positive_compacts.has_sizeof_inst
topological_space.compact_opens.has_sizeof_inst
continuous_linear_map.nonlinear_right_inverse.has_sizeof_inst
bifunctor.has_sizeof_inst
is_lawful_bifunctor.has_sizeof_inst
jordan_holder_lattice.has_sizeof_inst
composition_series.has_sizeof_inst
pequiv.has_sizeof_inst
composition.has_sizeof_inst
composition_as_set.has_sizeof_inst
nat.partition.has_sizeof_inst
alternating_map.has_sizeof_inst
polynomial.has_sizeof_inst
add_submonoid.localization_map.has_sizeof_inst
submonoid.localization_map.has_sizeof_inst
submonoid.localization_with_zero_map.has_sizeof_inst
tactic.ring_exp.coeff.has_sizeof_inst
tactic.ring_exp.ex_type.has_sizeof_inst
divisible_by.has_sizeof_inst
rootable_by.has_sizeof_inst
has_btw.has_sizeof_inst
has_sbtw.has_sizeof_inst
circular_preorder.has_sizeof_inst
circular_partial_order.has_sizeof_inst
circular_order.has_sizeof_inst
orthonormal_basis.has_sizeof_inst
convex_cone.has_sizeof_inst
quadratic_form.has_sizeof_inst
normed_add_comm_group_of_ring.has_sizeof_inst
quantum_set.has_sizeof_inst
wstar_algebra.has_sizeof_inst
von_neumann_algebra.has_sizeof_inst
qam_iso.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

@[protected]

def default.sizeof (α : Sort u) :

α → ℕ

Every type α has a default has_sizeof instance that just returns 0 for every element of α

Equations

default.sizeof α a = 0

source

@[protected, instance]

def default_has_sizeof (α : Sort u) :

has_sizeof α

Equations

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

source

@[protected, instance]

def nat.has_sizeof :

has_sizeof ℕ

Equations

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

source

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

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

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

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

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

@[protected, instance]

def punit.has_sizeof :

has_sizeof punit

Equations

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

source

@[protected, instance]

def bool.has_sizeof :

has_sizeof bool

Equations

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

source

@[protected, instance]

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

has_sizeof (option α)

Equations

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

source

@[protected, instance]

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

has_sizeof (list α)

Equations

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

source

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

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.

Instances for bin_tree

bin_tree.has_sizeof_inst
list.bin_tree_to_list
bin_tree.inhabited

source

@[reducible]

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

α

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

Equations

infer_instance = i