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.
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
.
- 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.
- 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.
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
- eq.decidable
- classical.prop_decidable
- has_lt.lt.decidable
- has_le.le.decidable
- list.decidable_forall_mem
- decidable.true
- decidable.false
- and.decidable
- or.decidable
- not.decidable
- implies.decidable
- iff.decidable
- xor.decidable
- exists_prop_decidable
- forall_prop_decidable
- ne.decidable
- ite.decidable
- dite.decidable
- prod_has_decidable_lt
- nat.decidable_le
- nat.decidable_lt
- list.decidable_mem
- list.has_decidable_lt
- list.has_decidable_le
- char.decidable_lt
- char.decidable_le
- string.has_decidable_lt
- fin.decidable_lt
- fin.decidable_le
- coe_decidable_eq
- local_context.has_mem.mem.decidable
- list.decidable_bex
- list.decidable_ball
- int.decidable_le
- int.decidable_lt
- option.decidable_forall_mem
- option.decidable_exists_mem
- list.decidable_pairwise
- list.decidable_chain
- list.decidable_chain'
- list.nodup_decidable
- bool.decidable_forall_bool
- bool.decidable_exists_bool
- set.decidable_mem
- set.compl.decidable_mem
- nat.decidable_ball_lt
- nat.decidable_forall_fin
- nat.decidable_ball_le
- nat.decidable_lo_hi
- nat.decidable_lo_hi_le
- list.decidable_sublist
- list.decidable_exists_mem
- list.decidable_prefix
- list.decidable_suffix
- list.decidable_infix
- list.decidable_perm
- multiset.decidable_mem
- multiset.decidable_dforall_multiset
- multiset.decidable_dexists_multiset
- multiset.nodup_decidable
- finset.decidable_mem
- finset.decidable_mem'
- finset.decidable_dforall_finset
- finset.decidable_dexists_finset
- finset.decidable_disjoint
- nat.coprime.decidable
- rat.decidable_nonneg
- fintype.decidable_forall_fintype
- fintype.decidable_exists_fintype
- fintype.decidable_left_inverse_fintype
- fintype.decidable_right_inverse_fintype
- roption.none_decidable
- roption.some_decidable
- roption.of_option_decidable
- enat.dom.decidable
- enat.decidable_le
- int.decidable_le_lt
- int.decidable_le_le
- int.decidable_lt_lt
- int.decidable_lt_le
- list.decidable_sorted
- polynomial.monic.decidable
- polynomial.is_root.decidable
- nat.decidable_prime
- nat.modeq.decidable
- int.modeq.decidable
- seq.terminated_at_decidable
- generalized_continued_fraction.terminated_at_decidable
- function.is_fixed_pt.decidable
- function.fixed_points.decidable
- polynomial.trailing_monic.decidable
- real.decidable_lt
- real.decidable_le
- real.decidable_eq
- sym.decidable_mem
- sym2.mem.decidable
- simple_graph.mem_edge_set_decidable
- simple_graph.mem_incidence_set_decidable
- bitvec.ult.decidable
- bitvec.ugt.decidable
- alist.has_mem.mem.decidable
- finmap.has_mem.mem.decidable
- fp.dec_valid_finite
- lazy_list.mem.decidable
- palindrome.decidable
- ordnode.all.decidable
- ordnode.any.decidable
- ordnode.emem.decidable
- ordnode.amem.decidable
- ordnode.mem.decidable
- irrational.decidable
- zsqrtd.decidable_nonnegg
- zsqrtd.decidable_nonneg
- zsqrtd.decidable_le
- function.is_periodic_pt.decidable
- decidable_list_all
- pgame.le_decidable
- pgame.lt_decidable
- pgame.equiv_decidable
- lists.equiv.decidable
- lists.subset.decidable
- lists.mem.decidable
Equations
- decidable_pred r = Π (a : α), decidable (r a)
Instances
- char.decidable_is_whitespace
- char.decidable_is_upper
- char.decidable_is_lower
- char.decidable_is_alpha
- char.decidable_is_digit
- char.decidable_is_alphanum
- char.decidable_is_punctuation
- set.decidable_set_of
- set.univ_decidable
- fintype.decidable_injective_fintype
- fintype.decidable_surjective_fintype
- fintype.decidable_bijective_fintype
- monoid_hom.decidable_mem_range
- add_monoid_hom.decidable_mem_range
- dfinsupp.decidable_zero
- decidable_gpowers
- nat.squarefree.decidable_pred
- nat.even.decidable_pred
- nat.decidable_pred_odd
- sym2.is_diag.decidable_pred
- sym2.from_rel.decidable_as_set
- sym2.from_rel.decidable_pred
- regular_expression.matches.decidable_pred
- int.even.decidable_pred
- int.decidable_pred_odd
- pos_num.decidable_prime
- num.decidable_prime
- ordnode.balanced.dec
- ordset.empty.decidable_pred
- mv_polynomial.decidable_restrict_degree
- lucas_lehmer.lucas_lehmer_test.decidable_pred
- onote.decidable_NF
Equations
- decidable_rel r = Π (a b : α), decidable (r a b)
Instances
- decidable_lt_of_decidable_le
- name.lt.decidable_rel
- expr.lt_prop.decidable_rel
- local_context.decidable_rel
- nat.decidable_dvd
- native.float.decidable_lt
- native.float.decidable_le
- prod.lex.decidable
- order.preimage.decidable
- with_bot.decidable_le
- with_bot.decidable_lt
- with_top.decidable_le
- with_top.decidable_lt
- list.lex.decidable_rel
- int.decidable_dvd
- rat.decidable_le
- quotient_group.left_rel_decidable
- quotient_add_group.left_rel_decidable
- finsupp.decidable_le
- pos_num.decidable_lt
- pos_num.decidable_le
- num.decidable_lt
- num.decidable_le
- znum.decidable_lt
- znum.decidable_le
- string.decidable_lt
- string.decidable_le
- free_group.red.decidable_rel
- equiv.perm.r.decidable_rel
- multiplicity.decidable_nat
- multiplicity.decidable_int
- sym2.rel.decidable_rel
- complete_graph_adj_decidable
- num.decidable_dvd
- pos_num.decidable_dvd
- znum.has_dvd.dvd.decidable_rel
- finmap.disjoint.decidable_rel
- ordnode.equiv.decidable_rel
- ordnode.balanced_sz.dec
- equiv.perm.same_cycle.decidable_rel
- onote.decidable_top_below
Equations
Instances
- decidable_eq_of_decidable_le
- decidable_eq_of_subsingleton
- fin_enum.dec_eq
- bool.decidable_eq
- prod.decidable_eq
- nat.decidable_eq
- quotient.decidable_eq
- list.decidable_eq
- char.decidable_eq
- string.has_decidable_eq
- fin.decidable_eq
- unsigned.decidable_eq
- ordering.decidable_eq
- name.has_decidable_eq
- option.decidable_eq
- options.has_decidable_eq
- level.has_decidable_eq
- pos.decidable_eq
- expr.has_decidable_eq
- local_context.has_decidable_eq
- punit.decidable_eq
- tactic.binder_info.has_decidable_eq
- vm_obj_kind.decidable_eq
- expr.coord.has_dec_eq
- expr.address.has_dec_eq
- int.decidable_eq
- subtype.decidable_eq
- d_array.decidable_eq
- array.decidable_eq
- rbnode.color.decidable_eq
- native.float.dec_eq
- widget.filter_type.decidable_eq
- widget.local_collection.decidable_eq
- doc_category.decidable_eq
- empty.decidable_eq
- pempty.decidable_eq
- binder_info.decidable_eq
- congr_arg_kind.decidable_eq
- binder.decidable_eq
- pexpr.decidable_eq
- function.decidable_eq_pfun
- widget_override.filter_type.decidable_eq
- widget_override.local_collection.decidable_eq
- tactic.transparency.decidable_eq
- lint_verbosity.decidable_eq
- sum.decidable_eq
- auto.auto_config.decidable_eq
- auto.case_option.decidable_eq
- norm_cast.label.decidable_eq
- tactic.simp_arg_type.decidable_eq
- tactic.suggest.head_symbol_match.decidable_eq
- units.decidable_eq
- add_units.decidable_eq
- ulift.decidable_eq
- plift.decidable_eq
- sigma.decidable_eq
- psigma.decidable_eq
- multiset.has_decidable_eq
- multiset.decidable_eq_pi_multiset
- tactic.interactive.mono_selection.decidable_eq
- tactic.interactive.mono_function.decidable_eq
- expr_lens.dir.decidable_eq
- finset.has_decidable_eq
- finset.decidable_eq_pi_finset
- pnat.decidable_eq
- ulower.decidable_eq
- rat.decidable_eq
- vector.decidable_eq
- fintype.decidable_pi_fintype
- fintype.decidable_eq_equiv_fintype
- con.quotient.decidable_eq
- add_con.quotient.decidable_eq
- finsupp.finsupp.decidable_eq
- linarith.ineq.decidable_eq
- pos_num.decidable_eq
- num.decidable_eq
- znum.decidable_eq
- tree.decidable_eq
- category_theory.limits.walking_pair.decidable_eq
- category_theory.limits.walking_parallel_pair.decidable_eq
- category_theory.limits.walking_parallel_pair_hom.decidable_eq
- category_theory.limits.wide_pullback_shape.hom.decidable_eq
- category_theory.limits.wide_pushout_shape.hom.decidable_eq
- dfinsupp.decidable_eq
- tactic.ring_exp.coeff.decidable_eq
- tactic.ring_exp.ex_type.decidable_eq
- mv_polynomial.decidable_eq_mv_polynomial
- free_group.decidable_eq
- omega.nat.preterm.decidable_eq
- free_magma.decidable_eq
- free_add_magma.decidable_eq
- free_semigroup.decidable_eq
- free_add_semigroup.decidable_eq
- tactic.decl_reducibility.decidable_eq
- zmod.decidable_eq
- complex.decidable_eq
- adjoin_root.decidable_eq
- partition.decidable_eq
- simple_graph.dart.decidable_eq
- nzsnum.decidable_eq
- snum.decidable_eq
- computability.Γ'.decidable_eq
- turing.dir.decidable_eq
- turing.fin_tm2.K.decidable_eq
- turing.partrec_to_TM2.Γ'.decidable_eq
- turing.partrec_to_TM2.K'.decidable_eq
- buffer.decidable_eq
- alist.decidable_eq
- finmap.has_decidable_eq
- thunk.decidable_eq
- lazy_list.decidable_eq
- zsqrtd.decidable_eq
- dihedral.decidable_eq
- semidirect_product.decidable_eq
- uchange.decidable_eq
- lucas_lehmer.X.decidable_eq
- lex.decidable_eq
- lists'.decidable_eq
- lists.decidable_eq
- finsets.decidable_eq
- onote.decidable_eq
- nonote.decidable_eq
- side.decidable_eq
- tactic.rewrite_search.side.decidable_eq
- tactic.ring2.horner_expr.decidable_eq
- pattern : unification_constraint
- constraints : list unification_constraint
- zero : α
Instances
- add_monoid.to_has_zero
- mul_zero_class.to_has_zero
- nat.has_zero
- int.has_zero
- fin.has_zero
- unsigned.has_zero
- native.float.has_zero
- pi.has_zero
- zero_hom.has_zero
- add_hom.has_zero
- add_monoid_hom.has_zero
- additive.has_zero
- prod.has_zero
- with_zero.has_zero
- with_top.has_zero
- with_bot.has_zero
- opposite.has_zero
- multiset.has_zero
- rat.has_zero
- set.has_zero
- add_submonoid.has_zero
- add_subgroup.has_zero
- matrix.has_zero
- sub_mul_action.has_zero
- submodule.has_zero
- enat.has_zero
- finsupp.has_zero
- linear_map.has_zero
- submodule.quotient.has_zero
- num.has_zero
- znum.has_zero
- associates.has_zero
- AddGroup.has_zero
- AddCommGroup.has_zero
- category_theory.limits.has_zero_morphisms.has_zero
- dfinsupp.has_zero
- ulift.has_zero
- cardinal.has_zero
- ordinal.has_zero
- multilinear_map.has_zero
- alternating_map.has_zero
- lie_algebra.morphism.has_zero
- lie_module_hom.has_zero
- lie_subalgebra.has_zero
- lie_submodule.has_zero
- triv_sq_zero_ext.has_zero
- filter.has_zero
- continuous_linear_map.has_zero
- continuous_map.has_zero
- localization.has_zero
- cau_seq.has_zero
- cau_seq.completion.Cauchy.has_zero
- real.has_zero
- nnreal.has_zero
- complex.has_zero
- bounded_continuous_function.has_zero
- continuous_multilinear_map.has_zero
- I_has_zero
- mv_power_series.has_zero
- measure_theory.outer_measure.has_zero
- measure_theory.measure.has_zero
- measure_theory.simple_func.has_zero
- filter.germ.has_zero
- measure_theory.ae_eq_fun.has_zero
- quaternion_algebra.has_zero
- category_theory.abelian.pseudoelement.has_zero
- language.has_zero
- bitvec.has_zero
- snum.has_zero
- regular_expression.has_zero
- holor.has_zero
- padic.has_zero
- padic_int.has_zero
- ereal.has_zero
- zsqrtd.has_zero
- perfect_closure.has_zero
- smooth_add_monoid_morphism.has_zero
- lie_add_group_morphism.has_zero
- smooth_map.has_zero
- quadratic_form.has_zero
- nat.arithmetic_function.has_zero
- poly.has_zero
- ring.fractional_ideal.has_zero
- derivation.has_zero
- witt_vector.has_zero
- truncated_witt_vector.has_zero
- pgame.has_zero
- game.has_zero
- onote.has_zero
- nonote.has_zero
- surreal.has_zero
- tactic.ring2.horner_expr.has_zero
- uniform_space.completion.has_zero
- one : α
Instances
- monoid.to_has_one
- nat.has_one
- int.has_one
- fin.has_one
- unsigned.has_one
- native.float.has_one
- pi.has_one
- one_hom.has_one
- mul_hom.has_one
- monoid_hom.has_one
- multiplicative.has_one
- prod.has_one
- with_one.has_one
- with_zero.has_one
- with_top.has_one
- with_bot.has_one
- opposite.has_one
- rat.has_one
- set.has_one
- submonoid.has_one
- subgroup.has_one
- matrix.has_one
- enat.has_one
- linear_map.has_one
- alg_equiv.has_one
- submodule.has_one
- pos_num.has_one
- num.has_one
- znum.has_one
- associates.has_one
- monoid_algebra.has_one
- add_monoid_algebra.has_one
- ideal.quotient.has_one
- category_theory.End.has_one
- Group.has_one
- CommGroup.has_one
- free_group.has_one
- ulift.has_one
- cardinal.has_one
- ordinal.has_one
- lie_algebra.morphism.has_one
- lie_algebra.equiv.has_one
- lie_module_hom.has_one
- lie_module_equiv.has_one
- triv_sq_zero_ext.has_one
- filter.has_one
- continuous_linear_map.has_one
- continuous_map.has_one
- cau_seq.has_one
- cau_seq.completion.Cauchy.has_one
- real.has_one
- nnreal.has_one
- complex.has_one
- I_has_one
- mv_power_series.has_one
- filter.germ.has_one
- measure_theory.ae_eq_fun.has_one
- quaternion_algebra.has_one
- language.has_one
- bitvec.has_one
- nzsnum.has_one
- snum.has_one
- regular_expression.has_one
- padic.has_one
- padic_int.has_one
- zsqrtd.has_one
- smooth_monoid_morphism.has_one
- lie_group_morphism.has_one
- smooth_map.has_one
- matrix.special_linear_group.has_one
- nat.arithmetic_function.has_one
- poly.has_one
- lucas_lehmer.X.has_one
- ring.fractional_ideal.has_one
- witt_vector.has_one
- truncated_witt_vector.has_one
- pgame.has_one
- game.has_one
- onote.has_one
- surreal.has_one
- tactic.ring2.horner_expr.has_one
- uniform_space.completion.has_one
- add : α → α → α
Instances
- add_semigroup.to_has_add
- distrib.to_has_add
- nat.has_add
- options.has_add
- int.has_add
- fin.has_add
- unsigned.has_add
- native.float.has_add
- pi.has_add
- add_monoid_hom.has_add
- additive.has_add
- prod.has_add
- with_zero.has_add
- with_top.has_add
- opposite.has_add
- multiset.has_add
- rat.has_add
- set.has_add
- finset.has_add
- add_submonoid.has_add
- add_subgroup.has_add
- matrix.has_add
- add_con.has_add
- submodule.has_add
- enat.has_add
- finsupp.has_add
- linear_map.has_add
- submodule.quotient.has_add
- pos_num.has_add
- num.has_add
- znum.has_add
- dfinsupp.has_add
- free_add_magma.has_add
- ulift.has_add
- cardinal.has_add
- ordinal.has_add
- multilinear_map.has_add
- alternating_map.has_add
- triv_sq_zero_ext.has_add
- filter.has_add
- continuous_linear_map.has_add
- continuous_map.has_add
- localization.has_add
- cau_seq.has_add
- cau_seq.completion.Cauchy.has_add
- real.has_add
- nnreal.has_add
- complex.has_add
- bounded_continuous_function.has_add
- continuous_multilinear_map.has_add
- measure_theory.outer_measure.has_add
- measure_theory.measure.has_add
- measure_theory.simple_func.has_add
- filter.germ.has_add
- measure_theory.ae_eq_fun.has_add
- quaternion_algebra.has_add
- language.has_add
- bitvec.has_add
- snum.has_add
- many_one_degree.has_add
- regular_expression.has_add
- fp.float.has_add
- holor.has_add
- padic.has_add
- padic_int.has_add
- ereal.has_add
- zsqrtd.has_add
- perfect_closure.has_add
- smooth_map.has_add
- quadratic_form.has_add
- nat.arithmetic_function.has_add
- poly.has_add
- ring.fractional_ideal.has_add
- witt_vector.has_add
- truncated_witt_vector.has_add
- pgame.has_add
- game.has_add
- onote.has_add
- nonote.has_add
- surreal.has_add
- tactic.ring2.horner_expr.has_add
- uniform_space.completion.has_add
- mul : α → α → α
Instances
- semigroup.to_has_mul
- mul_zero_class.to_has_mul
- distrib.to_has_mul
- nat.has_mul
- int.has_mul
- fin.has_mul
- unsigned.has_mul
- native.float.has_mul
- pi.has_mul
- monoid_hom.has_mul
- multiplicative.has_mul
- prod.has_mul
- with_one.has_mul
- opposite.has_mul
- rat.has_mul
- set.has_mul
- finset.has_mul
- submonoid.has_mul
- subgroup.has_mul
- matrix.has_mul
- con.has_mul
- linear_map.has_mul
- submodule.has_mul
- pos_num.has_mul
- num.has_mul
- znum.has_mul
- associates.has_mul
- monoid_algebra.has_mul
- add_monoid_algebra.has_mul
- ideal.quotient.has_mul
- category_theory.End.has_mul
- free_group.has_mul
- ideal.has_mul
- free_magma.has_mul
- ulift.has_mul
- cardinal.has_mul
- triv_sq_zero_ext.has_mul
- filter.has_mul
- continuous_linear_map.has_mul
- continuous_map.has_mul
- cau_seq.has_mul
- cau_seq.completion.Cauchy.has_mul
- real.has_mul
- nnreal.has_mul
- complex.has_mul
- mv_power_series.has_mul
- measure_theory.simple_func.has_mul
- filter.germ.has_mul
- measure_theory.ae_eq_fun.has_mul
- quaternion_algebra.has_mul
- language.has_mul
- bitvec.has_mul
- snum.has_mul
- regular_expression.has_mul
- finsupp.has_mul
- padic.has_mul
- padic_int.has_mul
- zsqrtd.has_mul
- perfect_closure.has_mul
- smooth_map.has_mul
- matrix.special_linear_group.has_mul
- nat.arithmetic_function.has_mul
- poly.has_mul
- lucas_lehmer.X.has_mul
- ring.fractional_ideal.has_mul
- witt_vector.has_mul
- truncated_witt_vector.has_mul
- onote.has_mul
- nonote.has_mul
- pgame.has_mul
- tactic.ring2.horner_expr.has_mul
- uniform_space.completion.has_mul
- inv : α → α
Instances
- div_inv_monoid.to_has_inv
- field.to_has_inv
- pi.has_inv
- monoid_hom.has_inv
- multiplicative.has_inv
- prod.has_inv
- with_zero.has_inv
- opposite.has_inv
- rat.has_inv
- set.has_inv
- subgroup.has_inv
- con.has_inv
- free_group.has_inv
- ulift.has_inv
- matrix.has_inv
- zmod.has_inv
- cau_seq.completion.Cauchy.has_inv
- nnreal.has_inv
- ennreal.has_inv
- complex.has_inv
- mv_power_series.has_inv
- power_series.has_inv
- filter.germ.has_inv
- measure_theory.ae_eq_fun.has_inv
- quaternion.has_inv
- perfect_closure.has_inv
- matrix.special_linear_group.has_inv
- ring.fractional_ideal.has_inv
- pgame.has_inv
- neg : α → α
Instances
- sub_neg_monoid.to_has_neg
- int.has_neg
- native.float.has_neg
- pi.has_neg
- add_monoid_hom.has_neg
- additive.has_neg
- prod.has_neg
- units.has_neg
- opposite.has_neg
- rat.has_neg
- set.has_neg'
- add_subgroup.has_neg
- matrix.has_neg
- add_con.has_neg
- sub_mul_action.has_neg
- submodule.has_neg
- linear_map.has_neg
- submodule.quotient.has_neg
- tensor_product.has_neg
- znum.has_neg
- dfinsupp.has_neg
- ulift.has_neg
- multilinear_map.has_neg
- alternating_map.has_neg
- triv_sq_zero_ext.has_neg
- continuous_linear_map.has_neg
- localization.has_neg
- cau_seq.has_neg
- cau_seq.completion.Cauchy.has_neg
- complex.has_neg
- metric.sphere.has_neg
- bounded_continuous_function.has_neg
- continuous_multilinear_map.has_neg
- linear_pmap.has_neg
- measure_theory.simple_func.has_neg
- filter.germ.has_neg
- measure_theory.ae_eq_fun.has_neg
- quaternion_algebra.has_neg
- bitvec.has_neg
- snum.has_neg
- fp.float.has_neg
- holor.has_neg
- padic.has_neg
- padic_int.has_neg
- ereal.has_neg
- zsqrtd.has_neg
- perfect_closure.has_neg
- quadratic_form.has_neg
- poly.has_neg
- witt_vector.has_neg
- truncated_witt_vector.has_neg
- pgame.has_neg
- game.has_neg
- Class.has_neg
- tactic.ring2.horner_expr.has_neg
- uniform_space.completion.has_neg
- sub : α → α → α
Instances
- sub_neg_monoid.to_has_sub
- nat.has_sub
- int.has_sub
- fin.has_sub
- unsigned.has_sub
- native.float.has_sub
- pi.has_sub
- add_monoid_hom.has_sub
- additive.has_sub
- prod.has_sub
- opposite.has_sub
- multiset.has_sub
- pnat.has_sub
- add_subgroup.has_sub
- matrix.has_sub
- finsupp.nat_sub
- finsupp.has_sub
- linear_map.has_sub
- submodule.quotient.has_sub
- pos_num.has_sub
- num.has_sub
- ulift.has_sub
- ordinal.has_sub
- multilinear_map.has_sub
- alternating_map.has_sub
- continuous_linear_map.has_sub
- cau_seq.has_sub
- cau_seq.completion.Cauchy.has_sub
- real.has_sub
- nnreal.has_sub
- ennreal.has_sub
- complex.has_sub
- bounded_continuous_function.has_sub
- continuous_multilinear_map.has_sub
- measure_theory.measure.has_sub
- measure_theory.simple_func.has_sub
- filter.germ.has_sub
- quaternion_algebra.has_sub
- bitvec.has_sub
- snum.has_sub
- fp.float.has_sub
- padic.has_sub
- padic_int.has_sub
- prime_multiset.has_sub
- poly.has_sub
- witt_vector.has_sub
- pgame.has_sub
- onote.has_sub
- nonote.has_sub
- uniform_space.completion.has_sub
- div : α → α → α
Instances
- euclidean_domain.has_div
- div_inv_monoid.to_has_div
- nat.has_div
- int.has_div
- fin.has_div
- unsigned.has_div
- native.float.has_div
- pi.has_div
- monoid_hom.has_div
- multiplicative.has_div
- prod.has_div
- subgroup.has_div
- submodule.has_div
- num.has_div
- znum.has_div
- ulift.has_div
- ordinal.has_div
- polynomial.has_div
- filter.germ.has_div
- padic.has_div
- gaussian_int.has_div
- ring.fractional_ideal.fractional_ideal_has_div
- pgame.has_div
- dvd : α → α → Prop
Instances
- mod : α → α → α
- le : α → α → Prop
Instances
- with_top.has_le
- preorder.to_has_le
- nat.has_le
- list.has_le
- char.has_le
- fin.has_le
- local_context.has_le
- int.has_le
- unsigned.has_le
- native.float.has_le
- order_dual.has_le
- prod.has_le
- set.has_le
- list.has_le'
- rat.has_le
- submonoid.has_le
- add_submonoid.has_le
- subgroup.has_le
- add_subgroup.has_le
- setoid.has_le
- con.has_le
- add_con.has_le
- enat.has_le
- pos_num.has_le
- num.has_le
- znum.has_le
- string.has_le
- cardinal.has_le
- ordinal.has_le
- cau_seq.has_le
- real.has_le
- nnreal.has_le
- linear_pmap.has_le
- convex_cone.has_le
- measure_theory.simple_func.has_le
- filter.germ.has_le
- finset.colex.has_le
- snum.has_le
- many_one_degree.has_le
- omega_complete_partial_order.chain.has_le
- semiquot.has_le
- setoid.partition.le
- zsqrtd.has_le
- lex_has_le
- dlex_has_le
- pgame.has_le
- game.has_le
- lt : α → α → Prop
Instances
- with_bot.has_lt
- with_top.has_lt
- preorder.to_has_lt
- prod.has_lt
- nat.has_lt
- list.has_lt
- char.has_lt
- string.has_lt
- fin.has_lt
- name.has_lt
- expr.has_lt
- expr.coord.has_lt
- int.has_lt
- unsigned.has_lt
- native.float.has_lt
- pos.has_lt
- order_dual.has_lt
- set.has_lt
- list.has_lt'
- rat.has_lt
- linarith.monom.has_lt
- pos_num.has_lt
- num.has_lt
- znum.has_lt
- string.has_lt'
- ordinal.has_lt
- cau_seq.has_lt
- real.has_lt
- convex_cone.has_lt
- finset.colex.has_lt
- snum.has_lt
- nat.upto.has_lt
- zsqrtd.has_lt
- lex_has_lt
- dlex_has_lt
- pilex.has_lt
- pgame.has_lt
- append : α → α → α
- andthen : α → β → σ
- union : α → α → α
- inter : α → α → α
- sdiff : α → α → α
- equiv : α → α → Prop
Instances
- subset : α → α → Prop
- ssubset : α → α → Prop
Instances
- emptyc : α
Instances
- list.has_emptyc
- local_context.has_emptyc
- set.has_emptyc
- widget.html.has_emptyc
- multiset.has_emptyc
- finset.has_emptyc
- topological_space.opens.has_emptyc
- algebraic_geometry.Scheme.has_emptyc
- turing.list_blank.has_emptyc
- alist.has_emptyc
- finmap.has_emptyc
- ordnode.has_emptyc
- ordset.has_emptyc
- finsets.has_emptyc
- pSet.has_emptyc
- Set.has_emptyc
- Class.has_emptyc
- insert : α → γ → γ
- singleton : α → β
- sep : (α → Prop) → γ → γ
- mem : α → γ → Prop
Instances
- list.has_mem
- local_context.has_mem
- set.has_mem
- array.has_mem
- rbtree.has_mem
- rbmap.has_mem
- option.has_mem
- widget_override.interactive_expression.expr.address.has_mem
- buffer.has_mem
- multiset.has_mem
- finset.has_mem
- submonoid.has_mem
- add_submonoid.has_mem
- subgroup.has_mem
- add_subgroup.has_mem
- con.has_mem
- add_con.has_mem
- sub_mul_action.has_mem
- submodule.has_mem
- roption.has_mem
- subsemiring.has_mem
- subring.has_mem
- subalgebra.has_mem
- stream.has_mem
- computation.has_mem
- seq.has_mem
- filter.has_mem
- filter_basis.has_mem
- ultrafilter.has_mem
- topological_space.opens.has_mem
- associates.factor_set.has_mem
- lie_subalgebra.has_mem
- lie_submodule.has_mem
- convex_cone.has_mem
- sym.has_mem
- sym2.has_mem
- language.inst
- nat.partrec.code.has_mem
- omega_complete_partial_order.chain.has_mem
- alist.has_mem
- finmap.has_mem
- semiquot.has_mem
- hash_map.has_mem
- lazy_list.has_mem
- ordnode.has_mem
- wseq.has_mem
- subfield.has_mem
- intermediate_field.has_mem
- affine_subspace.has_mem
- structure_groupoid.has_mem
- order.ideal.has_mem
- order.cofinal.has_mem
- ring.fractional_ideal.has_mem
- lists'.has_mem
- lists.has_mem
- pSet.has_mem
- Set.has_mem
- Class.has_mem
- open_subgroup.has_mem
- open_add_subgroup.has_mem
- pow : α → β → α
- insert_emptyc_eq : ∀ (x : α), {x} = {x}
- sizeof : α → ℕ
Instances
- default_has_sizeof
- slim_check.sampleable_ext.wf
- slim_check.sampleable.wf
- nat.has_sizeof
- prod.has_sizeof
- sum.has_sizeof
- psum.has_sizeof
- sigma.has_sizeof
- psigma.has_sizeof
- punit.has_sizeof
- bool.has_sizeof
- option.has_sizeof
- list.has_sizeof
- subtype.has_sizeof
- bin_tree.has_sizeof_inst
- inhabited.has_sizeof_inst
- ulift.has_sizeof_inst
- plift.has_sizeof_inst
- has_well_founded.has_sizeof_inst
- setoid.has_sizeof_inst
- char.has_sizeof_inst
- char.has_sizeof
- string_imp.has_sizeof_inst
- string.iterator_imp.has_sizeof_inst
- string.has_sizeof
- has_repr.has_sizeof_inst
- ordering.has_sizeof_inst
- has_lift.has_sizeof_inst
- has_lift_t.has_sizeof_inst
- has_coe.has_sizeof_inst
- has_coe_t.has_sizeof_inst
- has_coe_to_fun.has_sizeof_inst
- has_coe_to_sort.has_sizeof_inst
- has_coe_t_aux.has_sizeof_inst
- has_to_string.has_sizeof_inst
- name.has_sizeof_inst
- functor.has_sizeof_inst
- has_pure.has_sizeof_inst
- has_seq.has_sizeof_inst
- has_seq_left.has_sizeof_inst
- has_seq_right.has_sizeof_inst
- applicative.has_sizeof_inst
- has_orelse.has_sizeof_inst
- alternative.has_sizeof_inst
- has_bind.has_sizeof_inst
- monad.has_sizeof_inst
- has_monad_lift.has_sizeof_inst
- has_monad_lift_t.has_sizeof_inst
- monad_functor.has_sizeof_inst
- monad_functor_t.has_sizeof_inst
- monad_run.has_sizeof_inst
- format.color.has_sizeof_inst
- monad_fail.has_sizeof_inst
- pos.has_sizeof_inst
- binder_info.has_sizeof_inst
- reducibility_hints.has_sizeof_inst
- environment.projection_info.has_sizeof_inst
- environment.implicit_infer_kind.has_sizeof_inst
- tactic.transparency.has_sizeof_inst
- tactic.new_goals.has_sizeof_inst
- tactic.apply_cfg.has_sizeof_inst
- param_info.has_sizeof_inst
- fun_info.has_sizeof_inst
- subsingleton_info.has_sizeof_inst
- occurrences.has_sizeof_inst
- tactic.rewrite_cfg.has_sizeof_inst
- tactic.dsimp_config.has_sizeof_inst
- tactic.dunfold_config.has_sizeof_inst
- tactic.delta_config.has_sizeof_inst
- tactic.unfold_proj_config.has_sizeof_inst
- tactic.simp_config.has_sizeof_inst
- tactic.simp_intros_config.has_sizeof_inst
- interactive.loc.has_sizeof_inst
- cc_config.has_sizeof_inst
- congr_arg_kind.has_sizeof_inst
- tactic.interactive.case_tag.has_sizeof_inst
- tactic.interactive.case_tag.match_result.has_sizeof_inst
- tactic.unfold_config.has_sizeof_inst
- except.has_sizeof_inst
- except_t.has_sizeof_inst
- monad_except.has_sizeof_inst
- monad_except_adapter.has_sizeof_inst
- state_t.has_sizeof_inst
- monad_state.has_sizeof_inst
- monad_state_adapter.has_sizeof_inst
- reader_t.has_sizeof_inst
- monad_reader.has_sizeof_inst
- monad_reader_adapter.has_sizeof_inst
- option_t.has_sizeof_inst
- vm_obj_kind.has_sizeof_inst
- vm_decl_kind.has_sizeof_inst
- ematch_config.has_sizeof_inst
- smt_pre_config.has_sizeof_inst
- smt_config.has_sizeof_inst
- rsimp.config.has_sizeof_inst
- expr.coord.has_sizeof_inst
- preorder.has_sizeof_inst
- partial_order.has_sizeof_inst
- linear_order.has_sizeof_inst
- int.has_sizeof_inst
- d_array.has_sizeof_inst
- rbnode.has_sizeof_inst
- rbnode.color.has_sizeof_inst
- widget.mouse_event_kind.has_sizeof_inst
- doc_category.has_sizeof_inst
- tactic_doc_entry.has_sizeof_inst
- pempty.has_sizeof_inst
- dlist.has_sizeof_inst
- function.has_uncurry.has_sizeof_inst
- random_gen.has_sizeof_inst
- std_gen.has_sizeof_inst
- io.error.has_sizeof_inst
- io.mode.has_sizeof_inst
- io.process.stdio.has_sizeof_inst
- io.process.spawn_args.has_sizeof_inst
- monad_io.has_sizeof_inst
- monad_io_terminal.has_sizeof_inst
- monad_io_net_system.has_sizeof_inst
- monad_io_file_system.has_sizeof_inst
- monad_io_environment.has_sizeof_inst
- monad_io_process.has_sizeof_inst
- monad_io_random.has_sizeof_inst
- to_additive.value_type.has_sizeof_inst
- parse_result.has_sizeof_inst
- lint_verbosity.has_sizeof_inst
- tactic.explode.status.has_sizeof_inst
- auto.auto_config.has_sizeof_inst
- auto.case_option.has_sizeof_inst
- can_lift.has_sizeof_inst
- norm_cast.label.has_sizeof_inst
- _nest_1_1._nest_1_1.tactic.tactic_script._mut_.has_sizeof_inst
- _nest_1_1.tactic.tactic_script.has_sizeof_inst
- _nest_1_1.list.tactic.tactic_script.has_sizeof_inst
- tactic.tactic_script.has_sizeof_inst
- simps_cfg.has_sizeof_inst
- applicative_transformation.has_sizeof_inst
- traversable.has_sizeof_inst
- is_lawful_traversable.has_sizeof_inst
- tactic.suggest.head_symbol_match.has_sizeof_inst
- semigroup.has_sizeof_inst
- add_semigroup.has_sizeof_inst
- comm_semigroup.has_sizeof_inst
- add_comm_semigroup.has_sizeof_inst
- left_cancel_semigroup.has_sizeof_inst
- add_left_cancel_semigroup.has_sizeof_inst
- right_cancel_semigroup.has_sizeof_inst
- add_right_cancel_semigroup.has_sizeof_inst
- monoid.has_sizeof_inst
- add_monoid.has_sizeof_inst
- comm_monoid.has_sizeof_inst
- add_comm_monoid.has_sizeof_inst
- add_left_cancel_monoid.has_sizeof_inst
- left_cancel_monoid.has_sizeof_inst
- add_left_cancel_comm_monoid.has_sizeof_inst
- left_cancel_comm_monoid.has_sizeof_inst
- add_right_cancel_monoid.has_sizeof_inst
- right_cancel_monoid.has_sizeof_inst
- add_right_cancel_comm_monoid.has_sizeof_inst
- right_cancel_comm_monoid.has_sizeof_inst
- add_cancel_monoid.has_sizeof_inst
- cancel_monoid.has_sizeof_inst
- add_cancel_comm_monoid.has_sizeof_inst
- cancel_comm_monoid.has_sizeof_inst
- div_inv_monoid.has_sizeof_inst
- sub_neg_monoid.has_sizeof_inst
- group.has_sizeof_inst
- add_group.has_sizeof_inst
- comm_group.has_sizeof_inst
- add_comm_group.has_sizeof_inst
- unique.has_sizeof_inst
- units.has_sizeof_inst
- add_units.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
- zero_hom.has_sizeof_inst
- add_hom.has_sizeof_inst
- add_monoid_hom.has_sizeof_inst
- one_hom.has_sizeof_inst
- mul_hom.has_sizeof_inst
- monoid_hom.has_sizeof_inst
- monoid_with_zero_hom.has_sizeof_inst
- has_sup.has_sizeof_inst
- has_inf.has_sizeof_inst
- semilattice_sup.has_sizeof_inst
- semilattice_inf.has_sizeof_inst
- lattice.has_sizeof_inst
- distrib_lattice.has_sizeof_inst
- has_top.has_sizeof_inst
- has_bot.has_sizeof_inst
- order_top.has_sizeof_inst
- order_bot.has_sizeof_inst
- semilattice_sup_top.has_sizeof_inst
- semilattice_sup_bot.has_sizeof_inst
- semilattice_inf_top.has_sizeof_inst
- semilattice_inf_bot.has_sizeof_inst
- bounded_lattice.has_sizeof_inst
- bounded_distrib_lattice.has_sizeof_inst
- has_compl.has_sizeof_inst
- boolean_algebra.has_sizeof_inst
- equiv.has_sizeof_inst
- add_equiv.has_sizeof_inst
- mul_equiv.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
- linear_ordered_comm_monoid_with_zero.has_sizeof_inst
- canonically_ordered_add_monoid.has_sizeof_inst
- canonically_ordered_monoid.has_sizeof_inst
- canonically_linear_ordered_add_monoid.has_sizeof_inst
- canonically_linear_ordered_monoid.has_sizeof_inst
- ordered_cancel_add_comm_monoid.has_sizeof_inst
- ordered_cancel_comm_monoid.has_sizeof_inst
- linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
- linear_ordered_cancel_comm_monoid.has_sizeof_inst
- ordered_add_comm_group.has_sizeof_inst
- ordered_comm_group.has_sizeof_inst
- linear_ordered_add_comm_group.has_sizeof_inst
- linear_ordered_comm_group.has_sizeof_inst
- nonneg_add_comm_group.has_sizeof_inst
- ordered_semiring.has_sizeof_inst
- ordered_comm_semiring.has_sizeof_inst
- linear_ordered_semiring.has_sizeof_inst
- ordered_ring.has_sizeof_inst
- ordered_comm_ring.has_sizeof_inst
- linear_ordered_ring.has_sizeof_inst
- linear_ordered_comm_ring.has_sizeof_inst
- nonneg_ring.has_sizeof_inst
- linear_nonneg_ring.has_sizeof_inst
- canonically_ordered_comm_semiring.has_sizeof_inst
- division_ring.has_sizeof_inst
- field.has_sizeof_inst
- function.embedding.has_sizeof_inst
- has_scalar.has_sizeof_inst
- mul_action.has_sizeof_inst
- distrib_mul_action.has_sizeof_inst
- linear_ordered_field.has_sizeof_inst
- multiset.has_sizeof
- rel_hom.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
- 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
- galois_insertion.has_sizeof_inst
- galois_coinsertion.has_sizeof_inst
- directed_order.has_sizeof_inst
- tactic.interactive.rep_arity.has_sizeof_inst
- expr_lens.dir.has_sizeof_inst
- finset.has_sizeof_inst
- encodable.has_sizeof_inst
- euclidean_domain.has_sizeof_inst
- rat.has_sizeof_inst
- fintype.has_sizeof_inst
- tactic.abel.normalize_mode.has_sizeof_inst
- semimodule.has_sizeof_inst
- semimodule.core.has_sizeof_inst
- submonoid.has_sizeof_inst
- add_submonoid.has_sizeof_inst
- has_vadd.has_sizeof_inst
- has_vsub.has_sizeof_inst
- add_action.has_sizeof_inst
- add_torsor.has_sizeof_inst
- ring_equiv.has_sizeof_inst
- has_star.has_sizeof_inst
- has_involutive_star.has_sizeof_inst
- star_monoid.has_sizeof_inst
- star_ring.has_sizeof_inst
- subgroup.has_sizeof_inst
- add_subgroup.has_sizeof_inst
- mul_semiring_action.has_sizeof_inst
- faithful_mul_semiring_action.has_sizeof_inst
- mul_action_hom.has_sizeof_inst
- distrib_mul_action_hom.has_sizeof_inst
- mul_semiring_action_hom.has_sizeof_inst
- linear_map.has_sizeof_inst
- linear_map.compatible_smul.has_sizeof_inst
- linear_equiv.has_sizeof_inst
- add_con.has_sizeof_inst
- con.has_sizeof_inst
- sub_mul_action.has_sizeof_inst
- submodule.has_sizeof_inst
- roption.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
- tensor_product.compatible_smul.has_sizeof_inst
- subsemiring.has_sizeof_inst
- subring.has_sizeof_inst
- algebra.has_sizeof_inst
- alg_hom.has_sizeof_inst
- alg_equiv.has_sizeof_inst
- subalgebra.has_sizeof_inst
- tactic.ring.normalize_mode.has_sizeof_inst
- linarith.ineq.has_sizeof_inst
- linarith.comp.has_sizeof_inst
- linarith.comp_source.has_sizeof_inst
- pos_num.has_sizeof_inst
- num.has_sizeof_inst
- znum.has_sizeof_inst
- tree.has_sizeof_inst
- floor_ring.has_sizeof_inst
- free_algebra.pre.has_sizeof_inst
- category_theory.has_hom.has_sizeof_inst
- category_theory.category_struct.has_sizeof_inst
- category_theory.category.has_sizeof_inst
- category_theory.functor.has_sizeof_inst
- category_theory.nat_trans.has_sizeof_inst
- category_theory.iso.has_sizeof_inst
- category_theory.is_iso.has_sizeof_inst
- category_theory.full.has_sizeof_inst
- category_theory.equivalence.has_sizeof_inst
- category_theory.is_equivalence.has_sizeof_inst
- category_theory.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.concrete_category.has_sizeof_inst
- category_theory.has_forget₂.has_sizeof_inst
- category_theory.bundled.has_sizeof_inst
- category_theory.bundled_hom.has_sizeof_inst
- category_theory.bundled_hom.parent_projection.has_sizeof_inst
- category_theory.reflects_isomorphisms.has_sizeof_inst
- category_theory.groupoid.has_sizeof_inst
- category_theory.unbundled_hom.has_sizeof_inst
- category_theory.representable.has_sizeof_inst
- category_theory.limits.cone.has_sizeof_inst
- category_theory.limits.cocone.has_sizeof_inst
- category_theory.limits.cone_morphism.has_sizeof_inst
- category_theory.limits.cocone_morphism.has_sizeof_inst
- category_theory.limits.is_limit.has_sizeof_inst
- category_theory.limits.is_colimit.has_sizeof_inst
- category_theory.limits.limit_cone.has_sizeof_inst
- category_theory.limits.colimit_cocone.has_sizeof_inst
- category_theory.limits.walking_pair.has_sizeof_inst
- category_theory.limits.walking_parallel_pair.has_sizeof_inst
- category_theory.limits.walking_parallel_pair_hom.has_sizeof_inst
- category_theory.limits.wide_pullback_shape.hom.has_sizeof_inst
- category_theory.limits.wide_pushout_shape.hom.has_sizeof_inst
- category_theory.comma.has_sizeof_inst
- category_theory.comma_morphism.has_sizeof_inst
- category_theory.arrow.lift_struct.has_sizeof_inst
- category_theory.limits.mono_factorisation.has_sizeof_inst
- category_theory.limits.is_image.has_sizeof_inst
- category_theory.limits.image_factorisation.has_sizeof_inst
- category_theory.limits.has_images.has_sizeof_inst
- category_theory.limits.image_map.has_sizeof_inst
- category_theory.limits.has_image_maps.has_sizeof_inst
- category_theory.limits.strong_epi_mono_factorisation.has_sizeof_inst
- category_theory.limits.has_zero_morphisms.has_sizeof_inst
- category_theory.limits.has_zero_object.has_sizeof_inst
- category_theory.preadditive.has_sizeof_inst
- Module.has_sizeof_inst
- Algebra.has_sizeof_inst
- category_theory.fin_category.has_sizeof_inst
- bifunctor.has_sizeof_inst
- is_lawful_bifunctor.has_sizeof_inst
- equiv_functor.has_sizeof_inst
- category_theory.limits.preserves_limit.has_sizeof_inst
- category_theory.limits.preserves_colimit.has_sizeof_inst
- category_theory.limits.preserves_limits_of_shape.has_sizeof_inst
- category_theory.limits.preserves_colimits_of_shape.has_sizeof_inst
- category_theory.limits.preserves_limits.has_sizeof_inst
- category_theory.limits.preserves_colimits.has_sizeof_inst
- category_theory.limits.reflects_limit.has_sizeof_inst
- category_theory.limits.reflects_colimit.has_sizeof_inst
- category_theory.limits.reflects_limits_of_shape.has_sizeof_inst
- category_theory.limits.reflects_colimits_of_shape.has_sizeof_inst
- category_theory.limits.reflects_limits.has_sizeof_inst
- category_theory.limits.reflects_colimits.has_sizeof_inst
- category_theory.liftable_cone.has_sizeof_inst
- category_theory.liftable_cocone.has_sizeof_inst
- category_theory.creates_limit.has_sizeof_inst
- category_theory.creates_limits_of_shape.has_sizeof_inst
- category_theory.creates_limits.has_sizeof_inst
- category_theory.creates_colimit.has_sizeof_inst
- category_theory.creates_colimits_of_shape.has_sizeof_inst
- category_theory.creates_colimits.has_sizeof_inst
- category_theory.lifts_to_limit.has_sizeof_inst
- category_theory.lifts_to_colimit.has_sizeof_inst
- dfinsupp.pre.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.bicone.has_sizeof_inst
- category_theory.limits.limit_bicone.has_sizeof_inst
- category_theory.limits.binary_bicone.has_sizeof_inst
- category_theory.limits.binary_biproduct_data.has_sizeof_inst
- category_theory.regular_mono.has_sizeof_inst
- category_theory.regular_epi.has_sizeof_inst
- category_theory.normal_mono.has_sizeof_inst
- category_theory.normal_epi.has_sizeof_inst
- category_theory.non_preadditive_abelian.has_sizeof_inst
- category_theory.abelian.has_sizeof_inst
- tactic.tfae.arrow.has_sizeof_inst
- category_theory.monoidal_category.has_sizeof_inst
- category_theory.lax_monoidal_functor.has_sizeof_inst
- category_theory.monoidal_functor.has_sizeof_inst
- category_theory.monoidal_nat_trans.has_sizeof_inst
- category_theory.braided_category.has_sizeof_inst
- category_theory.symmetric_category.has_sizeof_inst
- category_theory.lax_braided_functor.has_sizeof_inst
- category_theory.braided_functor.has_sizeof_inst
- Mon.colimits.prequotient.has_sizeof_inst
- 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
- filter.has_sizeof_inst
- denumerable.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
- normalization_monoid.has_sizeof_inst
- gcd_monoid.has_sizeof_inst
- category_theory.has_shift.has_sizeof_inst
- category_theory.differential_object.has_sizeof_inst
- category_theory.differential_object.hom.has_sizeof_inst
- invertible.has_sizeof_inst
- has_bracket.has_sizeof_inst
- initial_seg.has_sizeof_inst
- principal_seg.has_sizeof_inst
- Well_order.has_sizeof_inst
- tactic.decl_reducibility.has_sizeof_inst
- ultrafilter.has_sizeof_inst
- topological_space.has_sizeof_inst
- homeomorph.has_sizeof_inst
- pequiv.has_sizeof_inst
- multilinear_map.has_sizeof_inst
- alternating_map.has_sizeof_inst
- dual_pair.has_sizeof_inst
- bilin_form.has_sizeof_inst
- lie_ring.has_sizeof_inst
- lie_algebra.has_sizeof_inst
- lie_ring_module.has_sizeof_inst
- lie_module.has_sizeof_inst
- lie_algebra.morphism.has_sizeof_inst
- lie_algebra.equiv.has_sizeof_inst
- lie_module_hom.has_sizeof_inst
- lie_module_equiv.has_sizeof_inst
- lie_subalgebra.has_sizeof_inst
- lie_submodule.has_sizeof_inst
- linear_ordered_comm_group_with_zero.has_sizeof_inst
- linear_recurrence.has_sizeof_inst
- shelf.has_sizeof_inst
- shelf_hom.has_sizeof_inst
- rack.has_sizeof_inst
- quandle.has_sizeof_inst
- rack.pre_envel_group.has_sizeof_inst
- rack.pre_envel_group_rel'.has_sizeof_inst
- star_algebra.has_sizeof_inst
- continuous_map.has_sizeof_inst
- algebraic_geometry.PresheafedSpace.has_sizeof_inst
- algebraic_geometry.PresheafedSpace.hom.has_sizeof_inst
- Top.sheaf.has_sizeof_inst
- algebraic_geometry.SheafedSpace.has_sizeof_inst
- algebraic_geometry.LocallyRingedSpace.has_sizeof_inst
- add_group_with_zero_nhd.has_sizeof_inst
- TopCommRing.has_sizeof_inst
- uniform_space.core.has_sizeof_inst
- uniform_space.has_sizeof_inst
- continuous_linear_map.has_sizeof_inst
- continuous_linear_equiv.has_sizeof_inst
- local_equiv.has_sizeof_inst
- local_homeomorph.has_sizeof_inst
- Top.prelocal_predicate.has_sizeof_inst
- Top.local_predicate.has_sizeof_inst
- add_submonoid.localization_map.has_sizeof_inst
- submonoid.localization_map.has_sizeof_inst
- localization_map.has_sizeof_inst
- algebraic_geometry.Scheme.has_sizeof_inst
- cau_seq.is_complete.has_sizeof_inst
- has_edist.has_sizeof_inst
- emetric_space.has_sizeof_inst
- has_dist.has_sizeof_inst
- metric_space.has_sizeof_inst
- has_continuous_inv'.has_sizeof_inst
- complex.has_sizeof_inst
- affine_map.has_sizeof_inst
- has_norm.has_sizeof_inst
- normed_group.has_sizeof_inst
- normed_ring.has_sizeof_inst
- normed_comm_ring.has_sizeof_inst
- normed_field.has_sizeof_inst
- nondiscrete_normed_field.has_sizeof_inst
- normed_space.has_sizeof_inst
- normed_algebra.has_sizeof_inst
- isometric.has_sizeof_inst
- continuous_multilinear_map.has_sizeof_inst
- normed_linear_ordered_group.has_sizeof_inst
- normed_linear_ordered_field.has_sizeof_inst
- affine_equiv.has_sizeof_inst
- normed_add_torsor.has_sizeof_inst
- path.has_sizeof_inst
- measurable_space.has_sizeof_inst
- measurable_equiv.has_sizeof_inst
- measurable_space.dynkin_system.has_sizeof_inst
- measure_theory.outer_measure.has_sizeof_inst
- measure_theory.measure.has_sizeof_inst
- measure_theory.measure.finite_spanning_sets_in.has_sizeof_inst
- measure_theory.measure_space.has_sizeof_inst
- composition.has_sizeof_inst
- composition_as_set.has_sizeof_inst
- implicit_function_data.has_sizeof_inst
- linear_pmap.has_sizeof_inst
- convex_cone.has_sizeof_inst
- measure_theory.simple_func.has_sizeof_inst
- is_R_or_C.has_sizeof_inst
- ring_invo.has_sizeof_inst
- sesq_form.has_sizeof_inst
- has_inner.has_sizeof_inst
- inner_product_space.has_sizeof_inst
- inner_product_space.core.has_sizeof_inst
- enorm.has_sizeof_inst
- quaternion_algebra.has_sizeof_inst
- seminorm.has_sizeof_inst
- category_theory.is_skeleton_of.has_sizeof_inst
- category_theory.reflective.has_sizeof_inst
- category_theory.is_kernel_pair.has_sizeof_inst
- category_theory.monad.has_sizeof_inst
- category_theory.comonad.has_sizeof_inst
- category_theory.monad_hom.has_sizeof_inst
- category_theory.comonad_hom.has_sizeof_inst
- category_theory.monad.algebra.has_sizeof_inst
- category_theory.monad.algebra.hom.has_sizeof_inst
- category_theory.comonad.coalgebra.has_sizeof_inst
- category_theory.comonad.coalgebra.hom.has_sizeof_inst
- category_theory.monadic_right_adjoint.has_sizeof_inst
- category_theory.is_split_coequalizer.has_sizeof_inst
- category_theory.pairwise.has_sizeof_inst
- category_theory.pairwise.hom.has_sizeof_inst
- category_theory.closed.has_sizeof_inst
- category_theory.monoidal_closed.has_sizeof_inst
- category_theory.cartesian_closed_functor.has_sizeof_inst
- category_theory.functorial.has_sizeof_inst
- category_theory.grothendieck.has_sizeof_inst
- category_theory.grothendieck.hom.has_sizeof_inst
- category_theory.limits.diagram_of_cones.has_sizeof_inst
- category_theory.Monad.has_sizeof_inst
- category_theory.Comonad.has_sizeof_inst
- Mon_.has_sizeof_inst
- Mon_.hom.has_sizeof_inst
- CommMon_.has_sizeof_inst
- Mod.has_sizeof_inst
- Mod.hom.has_sizeof_inst
- category_theory.lax_monoidal.has_sizeof_inst
- category_theory.simple.has_sizeof_inst
- category_theory.quotient.has_sizeof_inst
- category_theory.sigma.sigma_hom.has_sizeof_inst
- category_theory.sieve.has_sizeof_inst
- category_theory.grothendieck_topology.has_sizeof_inst
- category_theory.pretopology.has_sizeof_inst
- preorder_hom.has_sizeof_inst
- closure_operator.has_sizeof_inst
- partition.has_sizeof_inst
- simple_graph.has_sizeof_inst
- simple_graph.dart.has_sizeof_inst
- simple_graph.matching.has_sizeof_inst
- DFA.has_sizeof_inst
- NFA.has_sizeof_inst
- nzsnum.has_sizeof_inst
- snum.has_sizeof_inst
- computability.encoding.has_sizeof_inst
- computability.fin_encoding.has_sizeof_inst
- computability.Γ'.has_sizeof_inst
- primcodable.has_sizeof_inst
- nat.partrec.code.has_sizeof_inst
- regular_expression.has_sizeof_inst
- turing.pointed_map.has_sizeof_inst
- turing.tape.has_sizeof_inst
- turing.dir.has_sizeof_inst
- turing.TM0.stmt.has_sizeof_inst
- turing.TM0.cfg.has_sizeof_inst
- turing.TM1.stmt.has_sizeof_inst
- turing.TM1.cfg.has_sizeof_inst
- turing.TM1to1.Λ'.has_sizeof_inst
- turing.TM0to1.Λ'.has_sizeof_inst
- turing.TM2.stmt.has_sizeof_inst
- turing.TM2.cfg.has_sizeof_inst
- turing.TM2to1.st_act.has_sizeof_inst
- turing.TM2to1.Λ'.has_sizeof_inst
- turing.fin_tm2.has_sizeof_inst
- turing.evals_to.has_sizeof_inst
- turing.evals_to_in_time.has_sizeof_inst
- turing.tm2_computable_aux.has_sizeof_inst
- turing.tm2_computable.has_sizeof_inst
- turing.tm2_computable_in_time.has_sizeof_inst
- turing.tm2_computable_in_poly_time.has_sizeof_inst
- turing.to_partrec.code.has_sizeof_inst
- turing.to_partrec.cont.has_sizeof_inst
- turing.to_partrec.cfg.has_sizeof_inst
- turing.partrec_to_TM2.Γ'.has_sizeof_inst
- turing.partrec_to_TM2.K'.has_sizeof_inst
- turing.partrec_to_TM2.cont'.has_sizeof_inst
- turing.partrec_to_TM2.Λ'.has_sizeof_inst
- bitraversable.has_sizeof_inst
- is_lawful_bitraversable.has_sizeof_inst
- has_fix.has_sizeof_inst
- fin2.has_sizeof_inst
- fin2.is_lt.has_sizeof_inst
- mvfunctor.has_sizeof_inst
- omega_complete_partial_order.has_sizeof_inst
- omega_complete_partial_order.continuous_hom.has_sizeof_inst
- lawful_fix.has_sizeof_inst
- writer_t.has_sizeof_inst
- monad_writer.has_sizeof_inst
- monad_writer_adapter.has_sizeof_inst
- monad_cont.label.has_sizeof_inst
- monad_cont.has_sizeof_inst
- is_lawful_monad_cont.has_sizeof_inst
- uliftable.has_sizeof_inst
- W_type.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
- ordnode.has_sizeof_inst
- valuation.has_sizeof_inst
- pfunctor.has_sizeof_inst
- pfunctor.approx.cofix_a.has_sizeof_inst
- pfunctor.M_intl.has_sizeof_inst
- mvpfunctor.has_sizeof_inst
- mvpfunctor.M.path.has_sizeof_inst
- mvpfunctor.W_path.has_sizeof_inst
- pnat.xgcd_type.has_sizeof_inst
- pnat.xgcd_type.has_sizeof
- mvqpf.has_sizeof_inst
- qpf.has_sizeof_inst
- has_finite_inter.has_sizeof_inst
- zsqrtd.has_sizeof_inst
- circle_deg1_lift.has_sizeof_inst
- flow.has_sizeof_inst
- subfield.has_sizeof_inst
- intermediate_field.has_sizeof_inst
- intermediate_field.insert.has_sizeof_inst
- power_basis.has_sizeof_inst
- perfect_ring.has_sizeof_inst
- affine_subspace.has_sizeof_inst
- affine.simplex.has_sizeof_inst
- affine.simplex.points_with_circumcenter_index.has_sizeof_inst
- bundle_trivialization.has_sizeof_inst
- topological_fiber_bundle_core.has_sizeof_inst
- structure_groupoid.has_sizeof_inst
- pregroupoid.has_sizeof_inst
- charted_space.has_sizeof_inst
- charted_space_core.has_sizeof_inst
- structomorph.has_sizeof_inst
- model_with_corners.has_sizeof_inst
- basic_smooth_bundle_core.has_sizeof_inst
- smooth_add_monoid_morphism.has_sizeof_inst
- smooth_monoid_morphism.has_sizeof_inst
- lie_add_group_morphism.has_sizeof_inst
- lie_group_morphism.has_sizeof_inst
- times_cont_mdiff_map.has_sizeof_inst
- times_diffeomorph.has_sizeof_inst
- dihedral.has_sizeof_inst
- semidirect_product.has_sizeof_inst
- quadratic_form.has_sizeof_inst
- quadratic_form.isometry.has_sizeof_inst
- nonempty_fin_lin_ord.has_sizeof_inst
- order.ideal.has_sizeof_inst
- order.cofinal.has_sizeof_inst
- derivation.has_sizeof_inst
- pgame.has_sizeof_inst
- pgame.restricted.has_sizeof_inst
- pgame.relabelling.has_sizeof_inst
- pgame.short.has_sizeof_inst
- pgame.list_short.has_sizeof_inst
- pgame.state.has_sizeof_inst
- lists'.has_sizeof_inst
- lists.has_sizeof
- onote.has_sizeof_inst
- pgame.inv_ty.has_sizeof_inst
- pSet.has_sizeof_inst
- pSet.definable.has_sizeof_inst
- bounded_random.has_sizeof_inst
- random.has_sizeof_inst
- has_variable_names.has_sizeof_inst
- tactic.eliminate.generalization_mode.has_sizeof_inst
- side.has_sizeof_inst
- tactic.rewrite_search.side.has_sizeof_inst
- tactic.rewrite_search.dir_pair.has_sizeof_inst
- _nest_2_2.tactic.rewrite_search.using_conv.app_addr._mut_.has_sizeof_inst
- _nest_2_2.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
- _nest_2_2.option.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
- _nest_2_1.tactic.rewrite_search._nest_1_1.tactic.rewrite_search.using_conv.app_addr.dir_pair.has_sizeof_inst
- _nest_1_1.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
- _nest_1_1.option.tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
- tactic.rewrite_search.using_conv.app_addr.has_sizeof_inst
- tactic.rewrite_search.using_conv.splice_result.has_sizeof_inst
- tactic.ring2.csring_expr.has_sizeof_inst
- tactic.ring2.horner_expr.has_sizeof_inst
- slim_check.sampleable.has_sizeof_inst
- slim_check.sampleable_functor.has_sizeof_inst
- slim_check.sampleable_bifunctor.has_sizeof_inst
- slim_check.sampleable_ext.has_sizeof_inst
- slim_check.test_result.has_sizeof_inst
- slim_check.slim_check_cfg.has_sizeof_inst
- slim_check.printable_prop.has_sizeof_inst
- slim_check.testable.has_sizeof_inst
- slim_check.total_function.has_sizeof_inst
- slim_check.injective_function.has_sizeof_inst
- slim_check.injective_function.has_sizeof
- abstract_completion.has_sizeof_inst
- open_add_subgroup.has_sizeof_inst
- open_subgroup.has_sizeof_inst
- CompHaus.has_sizeof_inst
- Profinite.has_sizeof_inst
- CpltSepUniformSpace.has_sizeof_inst
- premetric_space.has_sizeof_inst
- Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
- module_doc_info.has_sizeof_inst
- ext_tactic_doc_entry.has_sizeof_inst
- slim_check.total_function.has_sizeof
Equations
- default_has_sizeof α = {sizeof := default.sizeof α}
Equations
- nat.has_sizeof = {sizeof := nat.sizeof}
Equations
- prod.has_sizeof α β = {sizeof := prod.sizeof _inst_2}
Equations
- sum.has_sizeof α β = {sizeof := sum.sizeof _inst_2}
Equations
- psum.has_sizeof α β = {sizeof := psum.sizeof _inst_2}
Equations
- sigma.has_sizeof α β = {sizeof := sigma.sizeof (λ (a : α), _inst_2 a)}
Equations
- psigma.has_sizeof α β = {sizeof := psigma.sizeof (λ (a : α), _inst_2 a)}
Equations
- punit.has_sizeof = {sizeof := punit.sizeof}
Equations
- bool.has_sizeof = {sizeof := bool.sizeof}
Equations
- option.has_sizeof α = {sizeof := option.sizeof _inst_1}
Equations
- list.has_sizeof α = {sizeof := list.sizeof _inst_1}
Equations
- subtype.has_sizeof p = {sizeof := subtype.sizeof p}
Equations
- combinator.K a b = a
Equations
- combinator.S x y z = x z (y z)
- 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
.
Like by apply_instance
, but not dependent on the tactic framework.