scilib documentation

core / init.core

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

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

Initialize the quotient module, which effectively adds the following definitions:

constant quot {α : Sort u} (r : α → α → Prop) : Sort u

constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r

constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
  (∀ a b : α, r a b → eq (f a) (f b)) → quot r → β

constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
  (∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q

Also the reduction rule:

quot.lift f _ (quot.mk a) ~~> f a
```
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
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
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
Instances of this typeclass
Instances of other typeclasses for decidable
source
@[reducible]
def decidable_pred {α : Sort u} (r : α → Prop) :
Sort (max u 1)
Equations
source
@[reducible]
def decidable_rel {α : Sort u} (r : α → α → Prop) :
Sort (max u 1)
Equations
source
@[reducible]
def decidable_eq (α : Sort u) :
Sort (max u 1)
Equations
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
Instances for nat
source
structure unification_constraint  :
Type (u+1)
  • α : Type ?
  • lhs : self.α
  • rhs : self.α
Instances for unification_constraint
source
structure unification_hint  :
Type (max (u_1+1) (u_2+1))
Instances for unification_hint

Declare builtin and reserved notation

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

Type classes has_emptyc and has_insert are used to implement polymorphic notation for collections. Example: {a, b, c} = insert a (insert b (singleton c)).

Note that we use pair in the name of lemmas about {x, y} = insert x (singleton y).

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
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
source
@[reducible]
def ssuperset {α : Type u} [has_ssubset α] (a b : α) :
Prop
Equations
source
def bit0 {α : Type u} [s : has_add α] (a : α) :
α
Equations
Instances for bit0
source
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) :
α
Equations
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

nat basic instances

source
@[protected]
def nat.add  :
ℕ → ℕ → ℕ
Equations
source
@[protected, instance]
def nat.has_zero  :
has_zero ℕ
Equations
source
@[protected, instance]
def nat.has_one  :
has_one ℕ
Equations
source
@[protected, instance]
def nat.has_add  :
has_add ℕ
Equations
source
def std.priority.default  :
ℕ
Equations
source
def std.priority.max  :
ℕ
Equations
source
@[protected]
def nat.prio  :
ℕ
Equations
source
def std.prec.max  :
ℕ
Equations
source
def std.prec.arrow  :
ℕ
Equations
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
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
  • pempty.has_sizeof_inst
  • function.has_uncurry.has_sizeof_inst
  • dlist.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
  • to_additive.value_type.has_sizeof_inst
  • lint_verbosity.has_sizeof_inst
  • norm_cast.label.has_sizeof_inst
  • fun_like.has_sizeof_inst
  • embedding_like.has_sizeof_inst
  • equiv_like.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
  • _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
  • equiv_functor.has_sizeof_inst
  • function.embedding.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
  • rel_hom.has_sizeof_inst
  • rel_hom_class.has_sizeof_inst
  • rel_embedding.has_sizeof_inst
  • rel_iso.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
  • 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
  • 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
  • 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
  • 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
  • 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
  • add_equiv.has_sizeof_inst
  • add_equiv_class.has_sizeof_inst
  • mul_equiv.has_sizeof_inst
  • mul_equiv_class.has_sizeof_inst
  • units.has_sizeof_inst
  • add_units.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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • canonically_ordered_comm_semiring.has_sizeof_inst
  • conditionally_complete_lattice.has_sizeof_inst
  • conditionally_complete_linear_order.has_sizeof_inst
  • conditionally_complete_linear_order_bot.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
  • 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
  • invertible.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
  • linear_ordered_semifield.has_sizeof_inst
  • linear_ordered_field.has_sizeof_inst
  • expr_lens.dir.has_sizeof_inst
  • tactic.abel.normalize_mode.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
  • 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
  • floor_semiring.has_sizeof_inst
  • floor_ring.has_sizeof_inst
  • euclidean_domain.has_sizeof_inst
  • ring_equiv.has_sizeof_inst
  • ring_equiv_class.has_sizeof_inst
  • mul_semiring_action.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
  • absolute_value.has_sizeof_inst
  • real.has_sizeof_inst
  • multiset.has_sizeof
  • tactic.interactive.rep_arity.has_sizeof_inst
  • finset.has_sizeof_inst
  • fintype.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
  • module.has_sizeof_inst
  • module.core.has_sizeof_inst
  • locally_finite_order.has_sizeof_inst
  • locally_finite_order_top.has_sizeof_inst
  • locally_finite_order_bot.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
  • finsupp.has_sizeof_inst
  • subsemiring.has_sizeof_inst
  • subring.has_sizeof_inst
  • algebra.has_sizeof_inst
  • canonically_linear_ordered_semifield.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
  • denumerable.has_sizeof_inst
  • filter.has_sizeof_inst
  • filter_basis.has_sizeof_inst
  • filter.countable_filter_basis.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
  • tactic.decl_reducibility.has_sizeof_inst
  • flag.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
  • succ_order.has_sizeof_inst
  • pred_order.has_sizeof_inst
  • tactic.tfae.arrow.has_sizeof_inst
  • uniform_space.core.has_sizeof_inst
  • uniform_space.has_sizeof_inst
  • homeomorph.has_sizeof_inst
  • uniform_equiv.has_sizeof_inst
  • has_bracket.has_sizeof_inst
  • has_quotient.has_sizeof_inst
  • add_con.has_sizeof_inst
  • con.has_sizeof_inst
  • add_torsor.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
  • 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
  • ring_topology.has_sizeof_inst
  • subfield.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
  • alg_hom.has_sizeof_inst
  • alg_hom_class.has_sizeof_inst
  • alg_equiv.has_sizeof_inst
  • alg_equiv_class.has_sizeof_inst
  • part.has_sizeof_inst
  • omega_complete_partial_order.has_sizeof_inst
  • omega_complete_partial_order.continuous_hom.has_sizeof_inst
  • non_unital_alg_hom.has_sizeof_inst
  • non_unital_alg_hom_class.has_sizeof_inst
  • tensor_product.compatible_smul.has_sizeof_inst
  • idem_semiring.has_sizeof_inst
  • idem_comm_semiring.has_sizeof_inst
  • has_kstar.has_sizeof_inst
  • kleene_algebra.has_sizeof_inst
  • linear_pmap.has_sizeof_inst
  • basis.has_sizeof_inst
  • subalgebra.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
  • star_ordered_ring.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
  • local_equiv.has_sizeof_inst
  • topological_space.opens.has_sizeof_inst
  • topological_space.open_nhds_of.has_sizeof_inst
  • local_homeomorph.has_sizeof_inst
  • BET.system.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
  • affine_map.has_sizeof_inst
  • affine_equiv.has_sizeof_inst
  • affine_subspace.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
  • linear_isometry.has_sizeof_inst
  • semilinear_isometry_class.has_sizeof_inst
  • linear_isometry_equiv.has_sizeof_inst
  • semilinear_isometry_equiv_class.has_sizeof_inst
  • normed_add_torsor.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
  • ring_con.has_sizeof_inst
  • polynomial.has_sizeof_inst
  • valuation.has_sizeof_inst
  • valuation_class.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
  • normed_add_group_hom.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
  • star_subalgebra.has_sizeof_inst
  • is_R_or_C.has_sizeof_inst
  • fin_enum.has_sizeof_inst
  • has_time.has_sizeof_inst
  • has_length.has_sizeof_inst
  • has_mass.has_sizeof_inst
  • has_amount_of_substance.has_sizeof_inst
  • has_electric_current.has_sizeof_inst
  • has_temperature.has_sizeof_inst
  • has_luminous_intensity.has_sizeof_inst
  • system1.has_sizeof_inst
  • initial_seg.has_sizeof_inst
  • principal_seg.has_sizeof_inst
  • Well_order.has_sizeof_inst
  • complex.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
  • affine_isometry.has_sizeof_inst
  • affine_isometry_equiv.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
  • 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
  • semidirect_product.has_sizeof_inst
  • bilin_form.has_sizeof_inst
  • has_inner.has_sizeof_inst
  • inner_product_space.has_sizeof_inst
  • inner_product_space.core.has_sizeof_inst
  • motion.has_sizeof_inst
  • motion_cont_diff_everywhere.has_sizeof_inst
  • thermo_system.has_sizeof_inst
  • ideal_gas.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

Declare sizeof instances and lemmas for types declared before has_sizeof. From now on, the inductive compiler will automatically generate sizeof instances and lemmas.

source
@[protected]
def default.sizeof (α : Sort u) :
α → ℕ

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

Equations
source
@[protected, instance]
def default_has_sizeof (α : Sort u) :
has_sizeof α
Equations
source
@[protected, instance]
def nat.has_sizeof  :
has_sizeof ℕ
Equations
source
@[protected, instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (α × β)
Equations
source
@[protected, instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (α ⊕ β)
Equations
source
@[protected, instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof (psum α β)
Equations
source
@[protected, instance]
def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
has_sizeof (sigma β)
Equations
source
@[protected, instance]
def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :
has_sizeof (psigma β)
Equations
source
@[protected, instance]
def punit.has_sizeof  :
has_sizeof punit
Equations
source
@[protected, instance]
def bool.has_sizeof  :
has_sizeof bool
Equations
source
@[protected, instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :
has_sizeof (option α)
Equations
source
@[protected, instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :
has_sizeof (list α)
Equations
source
@[protected, instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :
has_sizeof (subtype p)
Equations
source
theorem nat_add_zero (n : ℕ) :
n + 0 = n
source
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.

Instances for bin_tree
source
@[reducible]
def infer_instance {α : Sort u} [i : α] :
α

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

Equations