| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (611 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (125 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
Global Index
A
absorbing_full [definition, in Beroal.Subset]absorbing_empty [definition, in Beroal.Subset]
absorp_union [definition, in Beroal.Subset]
absorp_intersection [definition, in Beroal.Subset]
Acc_irrefl [definition, in Beroal.Init]
ackermann [definition, in Beroal.Ackermann]
Ackermann [library]
adjF [definition, in Beroal.CategoryTheory]
adjsF [projection, in Beroal.CategoryTheory]
adjsU [projection, in Beroal.CategoryTheory]
adjs_nt_eq_u [projection, in Beroal.CategoryTheory]
adjs_nt_eq_f [projection, in Beroal.CategoryTheory]
adjs_ret [projection, in Beroal.CategoryTheory]
adjs_fold [projection, in Beroal.CategoryTheory]
adjU [definition, in Beroal.CategoryTheory]
adjunction [section, in Beroal.CategoryTheory]
adjunction [definition, in Beroal.CategoryTheory]
adjunction_set [record, in Beroal.CategoryTheory]
adjunction_prop [record, in Beroal.CategoryTheory]
adjunction.adjunction_proj.a [variable, in Beroal.CategoryTheory]
adjunction.adjunction_proj [section, in Beroal.CategoryTheory]
adjunction.cata [variable, in Beroal.CategoryTheory]
adjunction.cats [variable, in Beroal.CategoryTheory]
adj_ret [definition, in Beroal.CategoryTheory]
adj_fold [definition, in Beroal.CategoryTheory]
adj2md [section, in Beroal.CategoryTheory]
adj2md [definition, in Beroal.CategoryTheory]
adj2md_set [definition, in Beroal.CategoryTheory]
adj2md_prop [definition, in Beroal.CategoryTheory]
adj2md.a [variable, in Beroal.CategoryTheory]
adj2md.alg_fold.C [variable, in Beroal.CategoryTheory]
adj2md.alg_fold [section, in Beroal.CategoryTheory]
adj2md.cata [variable, in Beroal.CategoryTheory]
adj2md.cats [variable, in Beroal.CategoryTheory]
alg_join.m [variable, in Beroal.CategoryTheory]
alg_join_set [definition, in Beroal.CategoryTheory]
alg_join.cat [variable, in Beroal.CategoryTheory]
alg_md_prop [record, in Beroal.CategoryTheory]
alg_fold [definition, in Beroal.CategoryTheory]
alg_fold_set [definition, in Beroal.CategoryTheory]
alg_md [definition, in Beroal.CategoryTheory]
alg_join [section, in Beroal.CategoryTheory]
alg_join [definition, in Beroal.CategoryTheory]
alg_join.C [variable, in Beroal.CategoryTheory]
alg_md_set [record, in Beroal.CategoryTheory]
alg_fold_prop [definition, in Beroal.CategoryTheory]
alg_join_prop [definition, in Beroal.CategoryTheory]
ams_unit [projection, in Beroal.CategoryTheory]
ams_fold [projection, in Beroal.CategoryTheory]
ams_assoc [projection, in Beroal.CategoryTheory]
ams_ob [projection, in Beroal.CategoryTheory]
app [definition, in Beroal.Stream]
app_nil_id [definition, in Beroal.Stream]
app_pres_eq [definition, in Beroal.Stream]
app_comm_cons [definition, in Beroal.Stream]
app_single_cons [definition, in Beroal.Stream]
assoc_intersection [definition, in Beroal.Subset]
assoc_union [definition, in Beroal.Subset]
B
big_union [inductive, in Beroal.Subset]big_union_nt_law [definition, in Beroal.Subset]
bind [definition, in Beroal.Subset]
blank_0 [definition, in Beroal.IntBipart]
bound_intersection [definition, in Beroal.Subset]
bound_union [definition, in Beroal.Subset]
bound2nat [definition, in Beroal.NatBound]
bound2nat_lt [definition, in Beroal.NatBound]
Build_intersect [constructor, in Beroal.Subset]
Build_big_union [constructor, in Beroal.Subset]
Build_map [constructor, in Beroal.Subset]
C
category [record, in Beroal.CategoryTheory]CategoryTheory [library]
cf [definition, in Beroal.Init]
check [section, in Beroal.Ackermann]
check.n [variable, in Beroal.Ackermann]
check.pm [variable, in Beroal.Ackermann]
check.pn [variable, in Beroal.Ackermann]
clique [definition, in Beroal.Subset]
comm_intersection [definition, in Beroal.Subset]
comm_union [definition, in Beroal.Subset]
comp [projection, in Beroal.CategoryTheory]
compi [definition, in Beroal.CategoryTheory]
complement_intersect [definition, in Beroal.Subset]
comp_nt_fr_mor.fr1 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor_set_id [definition, in Beroal.CategoryTheory]
comp_nt_fr_mor.fr2 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob.cat2 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob_set [definition, in Beroal.CategoryTheory]
comp_nt_fr_mor.fr0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob.fr2 [variable, in Beroal.CategoryTheory]
comp_assoc [projection, in Beroal.CategoryTheory]
comp_nt_fr_mor_prop [definition, in Beroal.CategoryTheory]
comp_nt_fr_ob.cat0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob [definition, in Beroal.CategoryTheory]
comp_nt_fr_ob.cat1 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor [section, in Beroal.CategoryTheory]
comp_nt_fr_mor.nt0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor.cat2 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor_set [definition, in Beroal.CategoryTheory]
comp_associ [definition, in Beroal.CategoryTheory]
comp_nt_fr_ob.nt0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor.cat0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob.fr0 [variable, in Beroal.CategoryTheory]
comp_nt_fr_mor_distrib_set [definition, in Beroal.CategoryTheory]
comp_nt_fr_ob [section, in Beroal.CategoryTheory]
comp_nt_fr_mor [definition, in Beroal.CategoryTheory]
comp_nt_fr_mor_id [definition, in Beroal.CategoryTheory]
comp_nt_fr_mor.cat1 [variable, in Beroal.CategoryTheory]
comp_nt_fr_ob_prop [definition, in Beroal.CategoryTheory]
comp_nt_fr_ob.fr1 [variable, in Beroal.CategoryTheory]
conclusion_eq_rpc [definition, in Beroal.Subset]
conclusion_included_in_rpc [definition, in Beroal.Subset]
contraction [definition, in Beroal.FunListArg]
couple [definition, in Beroal.Subset]
couple_comm [definition, in Beroal.Subset]
cycle [definition, in Beroal.Stream]
cycle_single_nth [definition, in Beroal.Stream]
cycle_single_cyclic [definition, in Beroal.Stream]
cycle_rotate_tl_app_nil [definition, in Beroal.Stream]
cycle_cyclic [definition, in Beroal.Stream]
cyclic [definition, in Beroal.Stream]
cyclic_hd_eq [definition, in Beroal.Stream]
cyclic_tl [definition, in Beroal.Stream]
cyclic_drop [definition, in Beroal.Stream]
D
decidable_Type [definition, in Beroal.Init]decidable_relation.equiv [variable, in Beroal.Init]
decidable_relation.trd [variable, in Beroal.Init]
decidable_Prop [definition, in Beroal.Init]
decidable_equality [definition, in Beroal.Init]
decidable_relation.rel [variable, in Beroal.Init]
decidable_relation.dec [variable, in Beroal.Init]
decidable_relation.type [variable, in Beroal.Init]
decidable_relation [section, in Beroal.Init]
definition0 [section, in Beroal.Subset]
definition0.op2_type [variable, in Beroal.Subset]
definition0.U [variable, in Beroal.Subset]
definition4 [section, in Beroal.Subset]
definition4.a [variable, in Beroal.Subset]
definition4.a0 [variable, in Beroal.Subset]
definition4.a1 [variable, in Beroal.Subset]
definition4.b [variable, in Beroal.Subset]
definition4.b0 [variable, in Beroal.Subset]
definition4.b1 [variable, in Beroal.Subset]
definition4.c [variable, in Beroal.Subset]
definition4.ext_eq_axiom_local [variable, in Beroal.Subset]
definition4.U [variable, in Beroal.Subset]
definition5 [section, in Beroal.Subset]
definition5.ext_eq_axiom_local [variable, in Beroal.Subset]
definition5.U [variable, in Beroal.Subset]
definition7 [section, in Beroal.Subset]
definition7.U [variable, in Beroal.Subset]
definition8 [section, in Beroal.Subset]
definition8.a [variable, in Beroal.Subset]
definition8.a0 [variable, in Beroal.Subset]
definition8.a1 [variable, in Beroal.Subset]
definition8.b [variable, in Beroal.Subset]
definition8.b0 [variable, in Beroal.Subset]
definition8.b1 [variable, in Beroal.Subset]
definition8.c [variable, in Beroal.Subset]
definition8.ext_eq_axiom_local [variable, in Beroal.Subset]
definition8.U [variable, in Beroal.Subset]
difference [definition, in Beroal.Subset]
disjoint [definition, in Beroal.Subset]
distrib_intersection [definition, in Beroal.Subset]
distrib_rpc_intersection [definition, in Beroal.Subset]
distrib_union [definition, in Beroal.Subset]
distrib_union_rpc [definition, in Beroal.Subset]
drop [definition, in Beroal.TakeDrop]
drop_degen [definition, in Beroal.TakeDrop]
drop_plus [definition, in Beroal.Stream]
drop_pres_eq [definition, in Beroal.Stream]
drop_plus [definition, in Beroal.TakeDrop]
drop_app_degen [definition, in Beroal.TakeDrop]
drop_app_exact [definition, in Beroal.Stream]
drop_app_exact [definition, in Beroal.TakeDrop]
drop_app_part [definition, in Beroal.Stream]
drop_length [definition, in Beroal.TakeDrop]
drop_nil [definition, in Beroal.TakeDrop]
drop_app_part [definition, in Beroal.TakeDrop]
drop_app_degen [definition, in Beroal.Stream]
E
element [section, in Beroal.Stream]element [section, in Beroal.TakeDrop]
element.e [variable, in Beroal.Stream]
element.e [variable, in Beroal.TakeDrop]
empty [definition, in Beroal.Subset]
empty_rpc [definition, in Beroal.Subset]
empty_least [definition, in Beroal.Subset]
enum [definition, in Beroal.Stream]
enum_nth [definition, in Beroal.Stream]
enum_step_nth [definition, in Beroal.Stream]
enum_step [definition, in Beroal.Stream]
eqst_many [definition, in Beroal.Stream]
Equality [library]
eq_nat_equiv [definition, in Beroal.IntBipart]
eq_equivalence [definition, in Beroal.Init]
eq_nat [definition, in Beroal.IntBipart]
ext_eq_dep3 [definition, in Beroal.FunExtEq]
ext_eq [definition, in Beroal.Subset]
ext_eq_dep2 [definition, in Beroal.FunExtEq]
ext_eq [definition, in Beroal.FunExtEq]
ext_eq_axiom [axiom, in Beroal.Subset]
ext_eq_dep [axiom, in Beroal.FunExtEq]
ext_eq_included [definition, in Beroal.Subset]
F
f [definition, in Beroal.Equality]filtered_infinite [definition, in Beroal.Stream]
filtered_finite [definition, in Beroal.Stream]
flat_map_nt_law1 [definition, in Beroal.ListMonad]
flat_map_nt_law0 [definition, in Beroal.ListMonad]
flat_map_app [definition, in Beroal.ListMonad]
fnozsm [definition, in Beroal.NatBound]
forall_args_eq [definition, in Beroal.FunExtEq]
frl [definition, in Beroal.CategoryTheory]
from_list [definition, in Beroal.Subset]
frs_mor [projection, in Beroal.CategoryTheory]
frs_pres_comp [projection, in Beroal.CategoryTheory]
frs_ob [projection, in Beroal.CategoryTheory]
frs_pres_id [projection, in Beroal.CategoryTheory]
fr_comp.fr01 [variable, in Beroal.CategoryTheory]
fr_comp_prop [definition, in Beroal.CategoryTheory]
fr_comp [section, in Beroal.CategoryTheory]
fr_comp_set [definition, in Beroal.CategoryTheory]
fr_comp.fr12 [variable, in Beroal.CategoryTheory]
fr_id_set [definition, in Beroal.CategoryTheory]
fr_comp [definition, in Beroal.CategoryTheory]
fr_ob [definition, in Beroal.CategoryTheory]
fr_id [definition, in Beroal.CategoryTheory]
fr_cat [definition, in Beroal.CategoryTheory]
fr_mor [definition, in Beroal.CategoryTheory]
fr_comp.cat1 [variable, in Beroal.CategoryTheory]
fr_id_prop [definition, in Beroal.CategoryTheory]
fr_comp.cat2 [variable, in Beroal.CategoryTheory]
fr_id.cat0 [variable, in Beroal.CategoryTheory]
fr_comp.cat0 [variable, in Beroal.CategoryTheory]
fr_id [section, in Beroal.CategoryTheory]
full [definition, in Beroal.Subset]
full_rpc [definition, in Beroal.Subset]
full_greatest [definition, in Beroal.Subset]
functor [section, in Beroal.CategoryTheory]
functor [definition, in Beroal.CategoryTheory]
functor_pres_id [definition, in Beroal.ListMonad]
functor_set [record, in Beroal.CategoryTheory]
functor_pres_id [definition, in Beroal.Subset]
functor_prop [record, in Beroal.CategoryTheory]
functor_pres_comp [definition, in Beroal.Subset]
functor.cat_dom [variable, in Beroal.CategoryTheory]
functor.cat_cod [variable, in Beroal.CategoryTheory]
functor.functor_proj [section, in Beroal.CategoryTheory]
functor.functor_proj.fr0 [variable, in Beroal.CategoryTheory]
functor.nt [section, in Beroal.CategoryTheory]
functor.nt_comp.fr0 [variable, in Beroal.CategoryTheory]
functor.nt_id [section, in Beroal.CategoryTheory]
functor.nt_comp [section, in Beroal.CategoryTheory]
functor.nt_comp.fr2 [variable, in Beroal.CategoryTheory]
functor.nt_id.fr0 [variable, in Beroal.CategoryTheory]
functor.nt_comp.nt01 [variable, in Beroal.CategoryTheory]
functor.nt_comp.fr1 [variable, in Beroal.CategoryTheory]
functor.nt_comp.nt12 [variable, in Beroal.CategoryTheory]
functor.nt.fr0 [variable, in Beroal.CategoryTheory]
functor.nt.fr1 [variable, in Beroal.CategoryTheory]
functor.nt.nt_proj [section, in Beroal.CategoryTheory]
functor.nt.nt_proj.nt0 [variable, in Beroal.CategoryTheory]
functor.ob_dom [variable, in Beroal.CategoryTheory]
functor.ob_cod [variable, in Beroal.CategoryTheory]
FunExtEq [library]
FunListArg [library]
fun_ext_eq [definition, in Beroal.CategoryTheory]
G
greatest [definition, in Beroal.Subset]greatest_sup [definition, in Beroal.Subset]
groupoid [section, in Beroal.Equality]
groupoid.eq01 [variable, in Beroal.Equality]
groupoid.eq12 [variable, in Beroal.Equality]
groupoid.eq23 [variable, in Beroal.Equality]
groupoid.t0 [variable, in Beroal.Equality]
groupoid.v0 [variable, in Beroal.Equality]
groupoid.v1 [variable, in Beroal.Equality]
groupoid.v2 [variable, in Beroal.Equality]
groupoid.v3 [variable, in Beroal.Equality]
H
half [definition, in Beroal.Init]half [section, in Beroal.Init]
half_lt [definition, in Beroal.Init]
half_even [definition, in Beroal.Init]
half_odd [definition, in Beroal.Init]
half_le [definition, in Beroal.Init]
hom [projection, in Beroal.CategoryTheory]
homi [record, in Beroal.CategoryTheory]
homi [section, in Beroal.CategoryTheory]
homi_fact [section, in Beroal.CategoryTheory]
homi_fact.cat [variable, in Beroal.CategoryTheory]
homi.cat [variable, in Beroal.CategoryTheory]
I
id [projection, in Beroal.CategoryTheory]id [definition, in Beroal.Init]
idemp_union [definition, in Beroal.Subset]
idemp_intersection [definition, in Beroal.Subset]
idi [definition, in Beroal.CategoryTheory]
id_lefti [definition, in Beroal.CategoryTheory]
id_left [projection, in Beroal.CategoryTheory]
id_right [projection, in Beroal.CategoryTheory]
id_righti [definition, in Beroal.CategoryTheory]
iff_Type [definition, in Beroal.Init]
iff_equivalence [definition, in Beroal.Init]
implication_preorder [definition, in Beroal.Init]
In [definition, in Beroal.Stream]
included [definition, in Beroal.Subset]
included_intersection_eq [definition, in Beroal.Subset]
included_union_eq [definition, in Beroal.Subset]
included_ub [definition, in Beroal.Subset]
included_lb_ub [definition, in Beroal.Subset]
included_order [definition, in Beroal.Subset]
included_ub_lb [definition, in Beroal.Subset]
included_lb [definition, in Beroal.Subset]
inc_equiv_intersection [definition, in Beroal.Subset]
inc_equiv_union [definition, in Beroal.Subset]
inf [definition, in Beroal.Subset]
inf_bound [definition, in Beroal.Subset]
inf_included_sup [definition, in Beroal.Subset]
Init [library]
IntBipart [library]
intersect [inductive, in Beroal.Subset]
intersection [definition, in Beroal.Subset]
intersection_infimum [definition, in Beroal.Subset]
intuitionistic_conj_intro [definition, in Beroal.Subset]
intuitionistic_k [definition, in Beroal.Subset]
intuitionistic_disj_intro_right [definition, in Beroal.Subset]
intuitionistic_contradiction_elim [definition, in Beroal.Subset]
intuitionistic_disj_elim [definition, in Beroal.Subset]
intuitionistic_s [definition, in Beroal.Subset]
intuitionistic_conj_elim_right [definition, in Beroal.Subset]
intuitionistic_disj_intro_left [definition, in Beroal.Subset]
intuitionistic_conj_elim_left [definition, in Beroal.Subset]
int_bipart_eq_equiv [definition, in Beroal.IntBipart]
int_bipart_eq_std [definition, in Beroal.IntBipart]
int_bipart [record, in Beroal.IntBipart]
int_bipart_eq_sym [definition, in Beroal.IntBipart]
int_bipart_rt [definition, in Beroal.IntBipart]
int_bipart_eq_refl [definition, in Beroal.IntBipart]
int_bipart_eq [definition, in Beroal.IntBipart]
int_bipart_eq_trans [definition, in Beroal.IntBipart]
int_bipart_eq_part [definition, in Beroal.IntBipart]
is_empty_eq [definition, in Beroal.Subset]
is_full [definition, in Beroal.Subset]
is_full_eq [definition, in Beroal.Subset]
is_empty [definition, in Beroal.Subset]
is0 [definition, in Beroal.IntBipart]
is0_opp [definition, in Beroal.IntBipart]
iterate [definition, in Beroal.Stream]
iterate_id_nth [definition, in Beroal.Stream]
iterate_id_cyclic [definition, in Beroal.Stream]
iterate_id_eq_cycle_single [definition, in Beroal.Stream]
J
JMeq [section, in Beroal.Equality]JMeq_constr_diff_types [definition, in Beroal.Equality]
JMeq.t0 [variable, in Beroal.Equality]
JMeq.t1 [variable, in Beroal.Equality]
JMeq.t2 [variable, in Beroal.Equality]
join [definition, in Beroal.ListMonad]
L
lb [definition, in Beroal.Subset]lb_idemp [definition, in Beroal.Subset]
lb2 [definition, in Beroal.Subset]
lb2_inc [definition, in Beroal.Subset]
least [definition, in Beroal.Subset]
least_inf [definition, in Beroal.Subset]
list [section, in Beroal.NatBound]
ListMonad [library]
list_ix [definition, in Beroal.NatBound]
list.e [variable, in Beroal.NatBound]
lt_IsSucc [definition, in Beroal.Init]
M
map [inductive, in Beroal.Subset]match_option [definition, in Beroal.Init]
max_dec [definition, in Beroal.NatBound]
md [definition, in Beroal.CategoryTheory]
md [section, in Beroal.CategoryTheory]
mds_ret [projection, in Beroal.CategoryTheory]
mds_assoc [projection, in Beroal.CategoryTheory]
mds_join [projection, in Beroal.CategoryTheory]
mds_id_right [projection, in Beroal.CategoryTheory]
mds_fr [projection, in Beroal.CategoryTheory]
mds_id_left [projection, in Beroal.CategoryTheory]
md_set [record, in Beroal.CategoryTheory]
md_fr [definition, in Beroal.CategoryTheory]
md_prop [record, in Beroal.CategoryTheory]
md_ret [definition, in Beroal.CategoryTheory]
md_join [definition, in Beroal.CategoryTheory]
md.alg_md.m [variable, in Beroal.CategoryTheory]
md.alg_md [section, in Beroal.CategoryTheory]
md.cat [variable, in Beroal.CategoryTheory]
md.md_proj [section, in Beroal.CategoryTheory]
md.md_proj.m [variable, in Beroal.CategoryTheory]
minus [definition, in Beroal.IntBipart]
minus_diag [definition, in Beroal.IntBipart]
minus0 [definition, in Beroal.NatBound]
monad_assoc [definition, in Beroal.ListMonad]
monad_id_left [definition, in Beroal.Subset]
monad_id_left [definition, in Beroal.ListMonad]
monad_id_right [definition, in Beroal.ListMonad]
monad_assoc [definition, in Beroal.Subset]
monad_id_right [definition, in Beroal.Subset]
mult [definition, in Beroal.IntBipart]
mult_plus_distr_r [definition, in Beroal.IntBipart]
mult_1_l [definition, in Beroal.IntBipart]
mult_eq_compat [definition, in Beroal.IntBipart]
mult_assoc [definition, in Beroal.IntBipart]
mult_comm [definition, in Beroal.IntBipart]
mult_plus_distr_l [definition, in Beroal.IntBipart]
N
NatBound [library]nat_ext_plus [definition, in Beroal.IntBipart]
nat_bound_iso0 [definition, in Beroal.NatBound]
nat_ext_is0 [definition, in Beroal.IntBipart]
nat_in_type_intro [constructor, in Beroal.NatBound]
nat_bound_eq [definition, in Beroal.NatBound]
nat_ext_mult [definition, in Beroal.IntBipart]
nat_in_type [inductive, in Beroal.NatBound]
nat_bound [definition, in Beroal.NatBound]
nat2bound [definition, in Beroal.NatBound]
nat2bound_sig [definition, in Beroal.NatBound]
nat2int_bipart [definition, in Beroal.IntBipart]
neutral_empty [definition, in Beroal.Subset]
neutral_full [definition, in Beroal.Subset]
non_dup [definition, in Beroal.Stream]
no_blank_0 [definition, in Beroal.IntBipart]
nt [definition, in Beroal.CategoryTheory]
ntf [definition, in Beroal.CategoryTheory]
nt_id_prop [definition, in Beroal.CategoryTheory]
nt_id_set [definition, in Beroal.CategoryTheory]
nt_prop [definition, in Beroal.CategoryTheory]
nt_comm [definition, in Beroal.CategoryTheory]
nt_set [definition, in Beroal.CategoryTheory]
nt_comp_set [definition, in Beroal.CategoryTheory]
nt_id [definition, in Beroal.CategoryTheory]
nt_comp_prop [definition, in Beroal.CategoryTheory]
nt_comp [definition, in Beroal.CategoryTheory]
nt_mor_comm [definition, in Beroal.CategoryTheory]
nt_eq_set [definition, in Beroal.CategoryTheory]
O
opp [definition, in Beroal.IntBipart]opp_involution [definition, in Beroal.IntBipart]
opp_plus [definition, in Beroal.IntBipart]
opp_compat [definition, in Beroal.IntBipart]
P
pair_fr_mor [definition, in Beroal.Equality]pair_fr_ob [definition, in Beroal.Equality]
plus [definition, in Beroal.IntBipart]
plus_assoc [definition, in Beroal.IntBipart]
plus_eq_compat [definition, in Beroal.IntBipart]
plus_0_l [definition, in Beroal.IntBipart]
plus_comm [definition, in Beroal.IntBipart]
pneg [projection, in Beroal.IntBipart]
poset_bound [section, in Beroal.Subset]
poset_bound_fact.U [variable, in Beroal.Subset]
poset_bound_fact [section, in Beroal.Subset]
poset_bound_fact.r [variable, in Beroal.Subset]
poset_bound_fact.s0 [variable, in Beroal.Subset]
poset_bound_fact.ext_eq_axiom_local [variable, in Beroal.Subset]
poset_bound.U [variable, in Beroal.Subset]
poset_bound_fact.s1 [variable, in Beroal.Subset]
poset_bound_fact.s [variable, in Beroal.Subset]
ppos [projection, in Beroal.IntBipart]
proof_irrelevance [definition, in Beroal.NatBound]
pseudo_complement [definition, in Beroal.Subset]
pw [definition, in Beroal.Subset]
pw [definition, in Beroal.FunListArg]
Q
quotient_equivalence [definition, in Beroal.Init]R
refl_equal_identity_left [definition, in Beroal.Equality]relation_independent.b [variable, in Beroal.Subset]
relation_independent [section, in Beroal.Subset]
relation_independent.r [variable, in Beroal.Subset]
relation_independent.a [variable, in Beroal.Subset]
rel_dual [definition, in Beroal.Subset]
rel_dec_bool_sym [definition, in Beroal.Init]
rel_dec_bool_trans [definition, in Beroal.Init]
rel_dec_bool_equiv [definition, in Beroal.Init]
rel_dec_bool [definition, in Beroal.Init]
rel_dec_bool_refl [definition, in Beroal.Init]
rep [definition, in Beroal.Init]
repeat [definition, in Beroal.Stream]
replicate [definition, in Beroal.Stream]
reptr [definition, in Beroal.Init]
reptr_fun_comm_fun [definition, in Beroal.Init]
reptr_plus [definition, in Beroal.Init]
rep_fun_comm_fun [definition, in Beroal.Init]
rep_plus [definition, in Beroal.Init]
rep_eq_reptr [definition, in Beroal.Init]
rotate [definition, in Beroal.FunListArg]
rpc [definition, in Beroal.Subset]
rpc_eval [definition, in Beroal.Subset]
rpc_equiv_included [definition, in Beroal.Subset]
rpc_id [definition, in Beroal.Subset]
rpc_equiv_greatest [definition, in Beroal.Subset]
rpc_equiv_equiv [definition, in Beroal.Subset]
rpc_full [definition, in Beroal.Subset]
S
sig_eq [definition, in Beroal.CategoryTheory]sig_eq [definition, in Beroal.Init]
singleton [definition, in Beroal.ListMonad]
singleton_nt_law [definition, in Beroal.Subset]
singleton_unique [definition, in Beroal.Subset]
singleton_included [definition, in Beroal.Subset]
single_head [definition, in Beroal.TakeDrop]
Some_or_default [definition, in Beroal.Init]
sort_singleton [definition, in Beroal.ListMonad]
Stream [library]
Stream_nat [section, in Beroal.Stream]
subset [definition, in Beroal.Subset]
Subset [library]
subst [section, in Beroal.Equality]
subst [definition, in Beroal.Equality]
subst_pair_fr.v0 [variable, in Beroal.Equality]
subst_mix.v0 [variable, in Beroal.Equality]
subst_functor.type_fun [variable, in Beroal.Equality]
subst_mix.eq01 [variable, in Beroal.Equality]
subst_prod [definition, in Beroal.Equality]
subst_comm_f.eqt [variable, in Beroal.Equality]
subst_as_in [definition, in Beroal.Equality]
subst_pair_fr.eq01 [variable, in Beroal.Equality]
subst_functor.eq12 [variable, in Beroal.Equality]
subst_mix1 [definition, in Beroal.Equality]
subst_functor.t1 [variable, in Beroal.Equality]
subst_pair_fr [section, in Beroal.Equality]
subst_pres_id [definition, in Beroal.Equality]
subst_functor.sort0 [variable, in Beroal.Equality]
subst_functor.v0 [variable, in Beroal.Equality]
subst_comm_f [definition, in Beroal.Equality]
subst_comm_f.t0 [variable, in Beroal.Equality]
subst_mix.v1 [variable, in Beroal.Equality]
subst_functor.eq01 [variable, in Beroal.Equality]
subst_pair_fr.t0 [variable, in Beroal.Equality]
subst_mix [section, in Beroal.Equality]
subst_mix0 [definition, in Beroal.Equality]
subst_pair_fr.t1 [variable, in Beroal.Equality]
subst_pres_comp [definition, in Beroal.Equality]
subst_mix.t0 [variable, in Beroal.Equality]
subst_in [definition, in Beroal.Equality]
subst_pair_fr [definition, in Beroal.Equality]
subst_comm_f.v0 [variable, in Beroal.Equality]
subst_functor.t2 [variable, in Beroal.Equality]
subst_functor.t0 [variable, in Beroal.Equality]
subst_comm_f [section, in Beroal.Equality]
subst_comm_f.t1 [variable, in Beroal.Equality]
subst_functor [section, in Beroal.Equality]
subst.t [variable, in Beroal.Equality]
subst0 [definition, in Beroal.Equality]
subst2equivalence [definition, in Beroal.Init]
succ_ord_wf [definition, in Beroal.Init]
succ_ord [definition, in Beroal.Init]
succ_ord_irrefl [definition, in Beroal.Init]
sup [definition, in Beroal.Subset]
sup_included_inf [definition, in Beroal.Subset]
sup_bound [definition, in Beroal.Subset]
sym_eq_opp_left [definition, in Beroal.Equality]
sym_eq_inv_self [definition, in Beroal.Equality]
sym_eq_opp_right [definition, in Beroal.Equality]
T
tail_length [definition, in Beroal.TakeDrop]take [definition, in Beroal.TakeDrop]
take [definition, in Beroal.Stream]
TakeDrop [library]
take_plus [definition, in Beroal.TakeDrop]
take_app_drop [definition, in Beroal.TakeDrop]
take_app_part [definition, in Beroal.Stream]
take_nil [definition, in Beroal.TakeDrop]
take_plus [definition, in Beroal.Stream]
take_degen [definition, in Beroal.TakeDrop]
take_app_exact [definition, in Beroal.Stream]
take_app_degen [definition, in Beroal.TakeDrop]
take_length [definition, in Beroal.TakeDrop]
take_pres_eq [definition, in Beroal.Stream]
take_app_exact [definition, in Beroal.TakeDrop]
take_app_part [definition, in Beroal.TakeDrop]
take_perm_tail [definition, in Beroal.TakeDrop]
take_app_degen [definition, in Beroal.Stream]
take_app_drop [definition, in Beroal.Stream]
take_cycle_id [definition, in Beroal.Stream]
trans_eq_assoc [definition, in Beroal.Equality]
trd_rel [projection, in Beroal.Init]
trd_equiv [projection, in Beroal.Init]
trd_type [projection, in Beroal.Init]
trd_dec [projection, in Beroal.Init]
type [definition, in Beroal.FunListArg]
type_rel_dec [record, in Beroal.Init]
U
ub [definition, in Beroal.Subset]ub_idemp [definition, in Beroal.Subset]
ub2 [definition, in Beroal.Subset]
ub2_inc [definition, in Beroal.Subset]
unfold_cycle [definition, in Beroal.Stream]
union [definition, in Beroal.Subset]
union_supremum [definition, in Beroal.Subset]
uniqueness_ex [definition, in Beroal.Subset]
unique_least_antisym [definition, in Beroal.Subset]
unique2ness [definition, in Beroal.Subset]
un_homi [projection, in Beroal.CategoryTheory]
W
weak [definition, in Beroal.FunListArg]Z
zip [definition, in Beroal.Stream]zip_with [definition, in Beroal.Stream]
other
_ '>__ [notation, in Beroal.CategoryTheory]_ # _ [notation, in Beroal.CategoryTheory]
_ !- _ [notation, in Beroal.IntBipart]
_ /*\ _ [notation, in Beroal.Subset]
_ #$ _ [notation, in Beroal.CategoryTheory]
_ !+ _ [notation, in Beroal.IntBipart]
_ @$ _ [notation, in Beroal.CategoryTheory]
_ - _ [notation, in Beroal.IntBipart]
_ + _ [notation, in Beroal.IntBipart]
_ -: _ [notation, in Beroal.NatBound]
_ *-> _ [notation, in Beroal.Subset]
_ -= _ [notation, in Beroal.IntBipart]
_ <'__ [notation, in Beroal.CategoryTheory]
_ \*/ _ [notation, in Beroal.Subset]
_ @ _ [notation, in Beroal.CategoryTheory]
_ !* _ [notation, in Beroal.IntBipart]
_ =@ _ [notation, in Beroal.CategoryTheory]
_ * _ [notation, in Beroal.CategoryTheory]
_ >$ _ [notation, in Beroal.CategoryTheory]
_ * _ [notation, in Beroal.IntBipart]
_ *\ _ [notation, in Beroal.Subset]
_ <* _ [notation, in Beroal.Subset]
_ <$ _ [notation, in Beroal.CategoryTheory]
- _ [notation, in Beroal.IntBipart]
~* _ [notation, in Beroal.Subset]
Projection Index
A
adjsF [in Beroal.CategoryTheory]adjsU [in Beroal.CategoryTheory]
adjs_nt_eq_u [in Beroal.CategoryTheory]
adjs_nt_eq_f [in Beroal.CategoryTheory]
adjs_ret [in Beroal.CategoryTheory]
adjs_fold [in Beroal.CategoryTheory]
ams_unit [in Beroal.CategoryTheory]
ams_fold [in Beroal.CategoryTheory]
ams_assoc [in Beroal.CategoryTheory]
ams_ob [in Beroal.CategoryTheory]
C
comp [in Beroal.CategoryTheory]comp_assoc [in Beroal.CategoryTheory]
F
frs_mor [in Beroal.CategoryTheory]frs_pres_comp [in Beroal.CategoryTheory]
frs_ob [in Beroal.CategoryTheory]
frs_pres_id [in Beroal.CategoryTheory]
H
hom [in Beroal.CategoryTheory]I
id [in Beroal.CategoryTheory]id_left [in Beroal.CategoryTheory]
id_right [in Beroal.CategoryTheory]
M
mds_ret [in Beroal.CategoryTheory]mds_assoc [in Beroal.CategoryTheory]
mds_join [in Beroal.CategoryTheory]
mds_id_right [in Beroal.CategoryTheory]
mds_fr [in Beroal.CategoryTheory]
mds_id_left [in Beroal.CategoryTheory]
P
pneg [in Beroal.IntBipart]ppos [in Beroal.IntBipart]
T
trd_rel [in Beroal.Init]trd_equiv [in Beroal.Init]
trd_type [in Beroal.Init]
trd_dec [in Beroal.Init]
U
un_homi [in Beroal.CategoryTheory]Record Index
A
adjunction_set [in Beroal.CategoryTheory]adjunction_prop [in Beroal.CategoryTheory]
alg_md_prop [in Beroal.CategoryTheory]
alg_md_set [in Beroal.CategoryTheory]
C
category [in Beroal.CategoryTheory]F
functor_set [in Beroal.CategoryTheory]functor_prop [in Beroal.CategoryTheory]
H
homi [in Beroal.CategoryTheory]I
int_bipart [in Beroal.IntBipart]M
md_set [in Beroal.CategoryTheory]md_prop [in Beroal.CategoryTheory]
T
type_rel_dec [in Beroal.Init]Section Index
A
adjunction [in Beroal.CategoryTheory]adjunction.adjunction_proj [in Beroal.CategoryTheory]
adj2md [in Beroal.CategoryTheory]
adj2md.alg_fold [in Beroal.CategoryTheory]
alg_join [in Beroal.CategoryTheory]
C
check [in Beroal.Ackermann]comp_nt_fr_mor [in Beroal.CategoryTheory]
comp_nt_fr_ob [in Beroal.CategoryTheory]
D
decidable_relation [in Beroal.Init]definition0 [in Beroal.Subset]
definition4 [in Beroal.Subset]
definition5 [in Beroal.Subset]
definition7 [in Beroal.Subset]
definition8 [in Beroal.Subset]
E
element [in Beroal.Stream]element [in Beroal.TakeDrop]
F
fr_comp [in Beroal.CategoryTheory]fr_id [in Beroal.CategoryTheory]
functor [in Beroal.CategoryTheory]
functor.functor_proj [in Beroal.CategoryTheory]
functor.nt [in Beroal.CategoryTheory]
functor.nt_id [in Beroal.CategoryTheory]
functor.nt_comp [in Beroal.CategoryTheory]
functor.nt.nt_proj [in Beroal.CategoryTheory]
G
groupoid [in Beroal.Equality]H
half [in Beroal.Init]homi [in Beroal.CategoryTheory]
homi_fact [in Beroal.CategoryTheory]
J
JMeq [in Beroal.Equality]L
list [in Beroal.NatBound]M
md [in Beroal.CategoryTheory]md.alg_md [in Beroal.CategoryTheory]
md.md_proj [in Beroal.CategoryTheory]
P
poset_bound [in Beroal.Subset]poset_bound_fact [in Beroal.Subset]
R
relation_independent [in Beroal.Subset]S
Stream_nat [in Beroal.Stream]subst [in Beroal.Equality]
subst_pair_fr [in Beroal.Equality]
subst_mix [in Beroal.Equality]
subst_comm_f [in Beroal.Equality]
subst_functor [in Beroal.Equality]
Notation Index
other
_ '>__ [in Beroal.CategoryTheory]_ # _ [in Beroal.CategoryTheory]
_ !- _ [in Beroal.IntBipart]
_ /*\ _ [in Beroal.Subset]
_ #$ _ [in Beroal.CategoryTheory]
_ !+ _ [in Beroal.IntBipart]
_ @$ _ [in Beroal.CategoryTheory]
_ - _ [in Beroal.IntBipart]
_ + _ [in Beroal.IntBipart]
_ -: _ [in Beroal.NatBound]
_ *-> _ [in Beroal.Subset]
_ -= _ [in Beroal.IntBipart]
_ <'__ [in Beroal.CategoryTheory]
_ \*/ _ [in Beroal.Subset]
_ @ _ [in Beroal.CategoryTheory]
_ !* _ [in Beroal.IntBipart]
_ =@ _ [in Beroal.CategoryTheory]
_ * _ [in Beroal.CategoryTheory]
_ >$ _ [in Beroal.CategoryTheory]
_ * _ [in Beroal.IntBipart]
_ *\ _ [in Beroal.Subset]
_ <* _ [in Beroal.Subset]
_ <$ _ [in Beroal.CategoryTheory]
- _ [in Beroal.IntBipart]
~* _ [in Beroal.Subset]
Constructor Index
B
Build_intersect [in Beroal.Subset]Build_big_union [in Beroal.Subset]
Build_map [in Beroal.Subset]
N
nat_in_type_intro [in Beroal.NatBound]Inductive Index
B
big_union [in Beroal.Subset]I
intersect [in Beroal.Subset]M
map [in Beroal.Subset]N
nat_in_type [in Beroal.NatBound]Definition Index
A
absorbing_full [in Beroal.Subset]absorbing_empty [in Beroal.Subset]
absorp_union [in Beroal.Subset]
absorp_intersection [in Beroal.Subset]
Acc_irrefl [in Beroal.Init]
ackermann [in Beroal.Ackermann]
adjF [in Beroal.CategoryTheory]
adjU [in Beroal.CategoryTheory]
adjunction [in Beroal.CategoryTheory]
adj_ret [in Beroal.CategoryTheory]
adj_fold [in Beroal.CategoryTheory]
adj2md [in Beroal.CategoryTheory]
adj2md_set [in Beroal.CategoryTheory]
adj2md_prop [in Beroal.CategoryTheory]
alg_join_set [in Beroal.CategoryTheory]
alg_fold [in Beroal.CategoryTheory]
alg_fold_set [in Beroal.CategoryTheory]
alg_md [in Beroal.CategoryTheory]
alg_join [in Beroal.CategoryTheory]
alg_fold_prop [in Beroal.CategoryTheory]
alg_join_prop [in Beroal.CategoryTheory]
app [in Beroal.Stream]
app_nil_id [in Beroal.Stream]
app_pres_eq [in Beroal.Stream]
app_comm_cons [in Beroal.Stream]
app_single_cons [in Beroal.Stream]
assoc_intersection [in Beroal.Subset]
assoc_union [in Beroal.Subset]
B
big_union_nt_law [in Beroal.Subset]bind [in Beroal.Subset]
blank_0 [in Beroal.IntBipart]
bound_intersection [in Beroal.Subset]
bound_union [in Beroal.Subset]
bound2nat [in Beroal.NatBound]
bound2nat_lt [in Beroal.NatBound]
C
cf [in Beroal.Init]clique [in Beroal.Subset]
comm_intersection [in Beroal.Subset]
comm_union [in Beroal.Subset]
compi [in Beroal.CategoryTheory]
complement_intersect [in Beroal.Subset]
comp_nt_fr_mor_set_id [in Beroal.CategoryTheory]
comp_nt_fr_ob_set [in Beroal.CategoryTheory]
comp_nt_fr_mor_prop [in Beroal.CategoryTheory]
comp_nt_fr_ob [in Beroal.CategoryTheory]
comp_nt_fr_mor_set [in Beroal.CategoryTheory]
comp_associ [in Beroal.CategoryTheory]
comp_nt_fr_mor_distrib_set [in Beroal.CategoryTheory]
comp_nt_fr_mor [in Beroal.CategoryTheory]
comp_nt_fr_mor_id [in Beroal.CategoryTheory]
comp_nt_fr_ob_prop [in Beroal.CategoryTheory]
conclusion_eq_rpc [in Beroal.Subset]
conclusion_included_in_rpc [in Beroal.Subset]
contraction [in Beroal.FunListArg]
couple [in Beroal.Subset]
couple_comm [in Beroal.Subset]
cycle [in Beroal.Stream]
cycle_single_nth [in Beroal.Stream]
cycle_single_cyclic [in Beroal.Stream]
cycle_rotate_tl_app_nil [in Beroal.Stream]
cycle_cyclic [in Beroal.Stream]
cyclic [in Beroal.Stream]
cyclic_hd_eq [in Beroal.Stream]
cyclic_tl [in Beroal.Stream]
cyclic_drop [in Beroal.Stream]
D
decidable_Type [in Beroal.Init]decidable_Prop [in Beroal.Init]
decidable_equality [in Beroal.Init]
difference [in Beroal.Subset]
disjoint [in Beroal.Subset]
distrib_intersection [in Beroal.Subset]
distrib_rpc_intersection [in Beroal.Subset]
distrib_union [in Beroal.Subset]
distrib_union_rpc [in Beroal.Subset]
drop [in Beroal.TakeDrop]
drop_degen [in Beroal.TakeDrop]
drop_plus [in Beroal.Stream]
drop_pres_eq [in Beroal.Stream]
drop_plus [in Beroal.TakeDrop]
drop_app_degen [in Beroal.TakeDrop]
drop_app_exact [in Beroal.Stream]
drop_app_exact [in Beroal.TakeDrop]
drop_app_part [in Beroal.Stream]
drop_length [in Beroal.TakeDrop]
drop_nil [in Beroal.TakeDrop]
drop_app_part [in Beroal.TakeDrop]
drop_app_degen [in Beroal.Stream]
E
empty [in Beroal.Subset]empty_rpc [in Beroal.Subset]
empty_least [in Beroal.Subset]
enum [in Beroal.Stream]
enum_nth [in Beroal.Stream]
enum_step_nth [in Beroal.Stream]
enum_step [in Beroal.Stream]
eqst_many [in Beroal.Stream]
eq_nat_equiv [in Beroal.IntBipart]
eq_equivalence [in Beroal.Init]
eq_nat [in Beroal.IntBipart]
ext_eq_dep3 [in Beroal.FunExtEq]
ext_eq [in Beroal.Subset]
ext_eq_dep2 [in Beroal.FunExtEq]
ext_eq [in Beroal.FunExtEq]
ext_eq_included [in Beroal.Subset]
F
f [in Beroal.Equality]filtered_infinite [in Beroal.Stream]
filtered_finite [in Beroal.Stream]
flat_map_nt_law1 [in Beroal.ListMonad]
flat_map_nt_law0 [in Beroal.ListMonad]
flat_map_app [in Beroal.ListMonad]
fnozsm [in Beroal.NatBound]
forall_args_eq [in Beroal.FunExtEq]
frl [in Beroal.CategoryTheory]
from_list [in Beroal.Subset]
fr_comp_prop [in Beroal.CategoryTheory]
fr_comp_set [in Beroal.CategoryTheory]
fr_id_set [in Beroal.CategoryTheory]
fr_comp [in Beroal.CategoryTheory]
fr_ob [in Beroal.CategoryTheory]
fr_id [in Beroal.CategoryTheory]
fr_cat [in Beroal.CategoryTheory]
fr_mor [in Beroal.CategoryTheory]
fr_id_prop [in Beroal.CategoryTheory]
full [in Beroal.Subset]
full_rpc [in Beroal.Subset]
full_greatest [in Beroal.Subset]
functor [in Beroal.CategoryTheory]
functor_pres_id [in Beroal.ListMonad]
functor_pres_id [in Beroal.Subset]
functor_pres_comp [in Beroal.Subset]
fun_ext_eq [in Beroal.CategoryTheory]
G
greatest [in Beroal.Subset]greatest_sup [in Beroal.Subset]
H
half [in Beroal.Init]half_lt [in Beroal.Init]
half_even [in Beroal.Init]
half_odd [in Beroal.Init]
half_le [in Beroal.Init]
I
id [in Beroal.Init]idemp_union [in Beroal.Subset]
idemp_intersection [in Beroal.Subset]
idi [in Beroal.CategoryTheory]
id_lefti [in Beroal.CategoryTheory]
id_righti [in Beroal.CategoryTheory]
iff_Type [in Beroal.Init]
iff_equivalence [in Beroal.Init]
implication_preorder [in Beroal.Init]
In [in Beroal.Stream]
included [in Beroal.Subset]
included_intersection_eq [in Beroal.Subset]
included_union_eq [in Beroal.Subset]
included_ub [in Beroal.Subset]
included_lb_ub [in Beroal.Subset]
included_order [in Beroal.Subset]
included_ub_lb [in Beroal.Subset]
included_lb [in Beroal.Subset]
inc_equiv_intersection [in Beroal.Subset]
inc_equiv_union [in Beroal.Subset]
inf [in Beroal.Subset]
inf_bound [in Beroal.Subset]
inf_included_sup [in Beroal.Subset]
intersection [in Beroal.Subset]
intersection_infimum [in Beroal.Subset]
intuitionistic_conj_intro [in Beroal.Subset]
intuitionistic_k [in Beroal.Subset]
intuitionistic_disj_intro_right [in Beroal.Subset]
intuitionistic_contradiction_elim [in Beroal.Subset]
intuitionistic_disj_elim [in Beroal.Subset]
intuitionistic_s [in Beroal.Subset]
intuitionistic_conj_elim_right [in Beroal.Subset]
intuitionistic_disj_intro_left [in Beroal.Subset]
intuitionistic_conj_elim_left [in Beroal.Subset]
int_bipart_eq_equiv [in Beroal.IntBipart]
int_bipart_eq_std [in Beroal.IntBipart]
int_bipart_eq_sym [in Beroal.IntBipart]
int_bipart_rt [in Beroal.IntBipart]
int_bipart_eq_refl [in Beroal.IntBipart]
int_bipart_eq [in Beroal.IntBipart]
int_bipart_eq_trans [in Beroal.IntBipart]
int_bipart_eq_part [in Beroal.IntBipart]
is_empty_eq [in Beroal.Subset]
is_full [in Beroal.Subset]
is_full_eq [in Beroal.Subset]
is_empty [in Beroal.Subset]
is0 [in Beroal.IntBipart]
is0_opp [in Beroal.IntBipart]
iterate [in Beroal.Stream]
iterate_id_nth [in Beroal.Stream]
iterate_id_cyclic [in Beroal.Stream]
iterate_id_eq_cycle_single [in Beroal.Stream]
J
JMeq_constr_diff_types [in Beroal.Equality]join [in Beroal.ListMonad]
L
lb [in Beroal.Subset]lb_idemp [in Beroal.Subset]
lb2 [in Beroal.Subset]
lb2_inc [in Beroal.Subset]
least [in Beroal.Subset]
least_inf [in Beroal.Subset]
list_ix [in Beroal.NatBound]
lt_IsSucc [in Beroal.Init]
M
match_option [in Beroal.Init]max_dec [in Beroal.NatBound]
md [in Beroal.CategoryTheory]
md_fr [in Beroal.CategoryTheory]
md_ret [in Beroal.CategoryTheory]
md_join [in Beroal.CategoryTheory]
minus [in Beroal.IntBipart]
minus_diag [in Beroal.IntBipart]
minus0 [in Beroal.NatBound]
monad_assoc [in Beroal.ListMonad]
monad_id_left [in Beroal.Subset]
monad_id_left [in Beroal.ListMonad]
monad_id_right [in Beroal.ListMonad]
monad_assoc [in Beroal.Subset]
monad_id_right [in Beroal.Subset]
mult [in Beroal.IntBipart]
mult_plus_distr_r [in Beroal.IntBipart]
mult_1_l [in Beroal.IntBipart]
mult_eq_compat [in Beroal.IntBipart]
mult_assoc [in Beroal.IntBipart]
mult_comm [in Beroal.IntBipart]
mult_plus_distr_l [in Beroal.IntBipart]
N
nat_ext_plus [in Beroal.IntBipart]nat_bound_iso0 [in Beroal.NatBound]
nat_ext_is0 [in Beroal.IntBipart]
nat_bound_eq [in Beroal.NatBound]
nat_ext_mult [in Beroal.IntBipart]
nat_bound [in Beroal.NatBound]
nat2bound [in Beroal.NatBound]
nat2bound_sig [in Beroal.NatBound]
nat2int_bipart [in Beroal.IntBipart]
neutral_empty [in Beroal.Subset]
neutral_full [in Beroal.Subset]
non_dup [in Beroal.Stream]
no_blank_0 [in Beroal.IntBipart]
nt [in Beroal.CategoryTheory]
ntf [in Beroal.CategoryTheory]
nt_id_prop [in Beroal.CategoryTheory]
nt_id_set [in Beroal.CategoryTheory]
nt_prop [in Beroal.CategoryTheory]
nt_comm [in Beroal.CategoryTheory]
nt_set [in Beroal.CategoryTheory]
nt_comp_set [in Beroal.CategoryTheory]
nt_id [in Beroal.CategoryTheory]
nt_comp_prop [in Beroal.CategoryTheory]
nt_comp [in Beroal.CategoryTheory]
nt_mor_comm [in Beroal.CategoryTheory]
nt_eq_set [in Beroal.CategoryTheory]
O
opp [in Beroal.IntBipart]opp_involution [in Beroal.IntBipart]
opp_plus [in Beroal.IntBipart]
opp_compat [in Beroal.IntBipart]
P
pair_fr_mor [in Beroal.Equality]pair_fr_ob [in Beroal.Equality]
plus [in Beroal.IntBipart]
plus_assoc [in Beroal.IntBipart]
plus_eq_compat [in Beroal.IntBipart]
plus_0_l [in Beroal.IntBipart]
plus_comm [in Beroal.IntBipart]
proof_irrelevance [in Beroal.NatBound]
pseudo_complement [in Beroal.Subset]
pw [in Beroal.Subset]
pw [in Beroal.FunListArg]
Q
quotient_equivalence [in Beroal.Init]R
refl_equal_identity_left [in Beroal.Equality]rel_dual [in Beroal.Subset]
rel_dec_bool_sym [in Beroal.Init]
rel_dec_bool_trans [in Beroal.Init]
rel_dec_bool_equiv [in Beroal.Init]
rel_dec_bool [in Beroal.Init]
rel_dec_bool_refl [in Beroal.Init]
rep [in Beroal.Init]
repeat [in Beroal.Stream]
replicate [in Beroal.Stream]
reptr [in Beroal.Init]
reptr_fun_comm_fun [in Beroal.Init]
reptr_plus [in Beroal.Init]
rep_fun_comm_fun [in Beroal.Init]
rep_plus [in Beroal.Init]
rep_eq_reptr [in Beroal.Init]
rotate [in Beroal.FunListArg]
rpc [in Beroal.Subset]
rpc_eval [in Beroal.Subset]
rpc_equiv_included [in Beroal.Subset]
rpc_id [in Beroal.Subset]
rpc_equiv_greatest [in Beroal.Subset]
rpc_equiv_equiv [in Beroal.Subset]
rpc_full [in Beroal.Subset]
S
sig_eq [in Beroal.CategoryTheory]sig_eq [in Beroal.Init]
singleton [in Beroal.ListMonad]
singleton_nt_law [in Beroal.Subset]
singleton_unique [in Beroal.Subset]
singleton_included [in Beroal.Subset]
single_head [in Beroal.TakeDrop]
Some_or_default [in Beroal.Init]
sort_singleton [in Beroal.ListMonad]
subset [in Beroal.Subset]
subst [in Beroal.Equality]
subst_prod [in Beroal.Equality]
subst_as_in [in Beroal.Equality]
subst_mix1 [in Beroal.Equality]
subst_pres_id [in Beroal.Equality]
subst_comm_f [in Beroal.Equality]
subst_mix0 [in Beroal.Equality]
subst_pres_comp [in Beroal.Equality]
subst_in [in Beroal.Equality]
subst_pair_fr [in Beroal.Equality]
subst0 [in Beroal.Equality]
subst2equivalence [in Beroal.Init]
succ_ord_wf [in Beroal.Init]
succ_ord [in Beroal.Init]
succ_ord_irrefl [in Beroal.Init]
sup [in Beroal.Subset]
sup_included_inf [in Beroal.Subset]
sup_bound [in Beroal.Subset]
sym_eq_opp_left [in Beroal.Equality]
sym_eq_inv_self [in Beroal.Equality]
sym_eq_opp_right [in Beroal.Equality]
T
tail_length [in Beroal.TakeDrop]take [in Beroal.TakeDrop]
take [in Beroal.Stream]
take_plus [in Beroal.TakeDrop]
take_app_drop [in Beroal.TakeDrop]
take_app_part [in Beroal.Stream]
take_nil [in Beroal.TakeDrop]
take_plus [in Beroal.Stream]
take_degen [in Beroal.TakeDrop]
take_app_exact [in Beroal.Stream]
take_app_degen [in Beroal.TakeDrop]
take_length [in Beroal.TakeDrop]
take_pres_eq [in Beroal.Stream]
take_app_exact [in Beroal.TakeDrop]
take_app_part [in Beroal.TakeDrop]
take_perm_tail [in Beroal.TakeDrop]
take_app_degen [in Beroal.Stream]
take_app_drop [in Beroal.Stream]
take_cycle_id [in Beroal.Stream]
trans_eq_assoc [in Beroal.Equality]
type [in Beroal.FunListArg]
U
ub [in Beroal.Subset]ub_idemp [in Beroal.Subset]
ub2 [in Beroal.Subset]
ub2_inc [in Beroal.Subset]
unfold_cycle [in Beroal.Stream]
union [in Beroal.Subset]
union_supremum [in Beroal.Subset]
uniqueness_ex [in Beroal.Subset]
unique_least_antisym [in Beroal.Subset]
unique2ness [in Beroal.Subset]
W
weak [in Beroal.FunListArg]Z
zip [in Beroal.Stream]zip_with [in Beroal.Stream]
Axiom Index
E
ext_eq_axiom [in Beroal.Subset]ext_eq_dep [in Beroal.FunExtEq]
Variable Index
A
adjunction.adjunction_proj.a [in Beroal.CategoryTheory]adjunction.cata [in Beroal.CategoryTheory]
adjunction.cats [in Beroal.CategoryTheory]
adj2md.a [in Beroal.CategoryTheory]
adj2md.alg_fold.C [in Beroal.CategoryTheory]
adj2md.cata [in Beroal.CategoryTheory]
adj2md.cats [in Beroal.CategoryTheory]
alg_join.m [in Beroal.CategoryTheory]
alg_join.cat [in Beroal.CategoryTheory]
alg_join.C [in Beroal.CategoryTheory]
C
check.n [in Beroal.Ackermann]check.pm [in Beroal.Ackermann]
check.pn [in Beroal.Ackermann]
comp_nt_fr_mor.fr1 [in Beroal.CategoryTheory]
comp_nt_fr_mor.fr2 [in Beroal.CategoryTheory]
comp_nt_fr_ob.cat2 [in Beroal.CategoryTheory]
comp_nt_fr_mor.fr0 [in Beroal.CategoryTheory]
comp_nt_fr_ob.fr2 [in Beroal.CategoryTheory]
comp_nt_fr_ob.cat0 [in Beroal.CategoryTheory]
comp_nt_fr_ob.cat1 [in Beroal.CategoryTheory]
comp_nt_fr_mor.nt0 [in Beroal.CategoryTheory]
comp_nt_fr_mor.cat2 [in Beroal.CategoryTheory]
comp_nt_fr_ob.nt0 [in Beroal.CategoryTheory]
comp_nt_fr_mor.cat0 [in Beroal.CategoryTheory]
comp_nt_fr_ob.fr0 [in Beroal.CategoryTheory]
comp_nt_fr_mor.cat1 [in Beroal.CategoryTheory]
comp_nt_fr_ob.fr1 [in Beroal.CategoryTheory]
D
decidable_relation.equiv [in Beroal.Init]decidable_relation.trd [in Beroal.Init]
decidable_relation.rel [in Beroal.Init]
decidable_relation.dec [in Beroal.Init]
decidable_relation.type [in Beroal.Init]
definition0.op2_type [in Beroal.Subset]
definition0.U [in Beroal.Subset]
definition4.a [in Beroal.Subset]
definition4.a0 [in Beroal.Subset]
definition4.a1 [in Beroal.Subset]
definition4.b [in Beroal.Subset]
definition4.b0 [in Beroal.Subset]
definition4.b1 [in Beroal.Subset]
definition4.c [in Beroal.Subset]
definition4.ext_eq_axiom_local [in Beroal.Subset]
definition4.U [in Beroal.Subset]
definition5.ext_eq_axiom_local [in Beroal.Subset]
definition5.U [in Beroal.Subset]
definition7.U [in Beroal.Subset]
definition8.a [in Beroal.Subset]
definition8.a0 [in Beroal.Subset]
definition8.a1 [in Beroal.Subset]
definition8.b [in Beroal.Subset]
definition8.b0 [in Beroal.Subset]
definition8.b1 [in Beroal.Subset]
definition8.c [in Beroal.Subset]
definition8.ext_eq_axiom_local [in Beroal.Subset]
definition8.U [in Beroal.Subset]
E
element.e [in Beroal.Stream]element.e [in Beroal.TakeDrop]
F
fr_comp.fr01 [in Beroal.CategoryTheory]fr_comp.fr12 [in Beroal.CategoryTheory]
fr_comp.cat1 [in Beroal.CategoryTheory]
fr_comp.cat2 [in Beroal.CategoryTheory]
fr_id.cat0 [in Beroal.CategoryTheory]
fr_comp.cat0 [in Beroal.CategoryTheory]
functor.cat_dom [in Beroal.CategoryTheory]
functor.cat_cod [in Beroal.CategoryTheory]
functor.functor_proj.fr0 [in Beroal.CategoryTheory]
functor.nt_comp.fr0 [in Beroal.CategoryTheory]
functor.nt_comp.fr2 [in Beroal.CategoryTheory]
functor.nt_id.fr0 [in Beroal.CategoryTheory]
functor.nt_comp.nt01 [in Beroal.CategoryTheory]
functor.nt_comp.fr1 [in Beroal.CategoryTheory]
functor.nt_comp.nt12 [in Beroal.CategoryTheory]
functor.nt.fr0 [in Beroal.CategoryTheory]
functor.nt.fr1 [in Beroal.CategoryTheory]
functor.nt.nt_proj.nt0 [in Beroal.CategoryTheory]
functor.ob_dom [in Beroal.CategoryTheory]
functor.ob_cod [in Beroal.CategoryTheory]
G
groupoid.eq01 [in Beroal.Equality]groupoid.eq12 [in Beroal.Equality]
groupoid.eq23 [in Beroal.Equality]
groupoid.t0 [in Beroal.Equality]
groupoid.v0 [in Beroal.Equality]
groupoid.v1 [in Beroal.Equality]
groupoid.v2 [in Beroal.Equality]
groupoid.v3 [in Beroal.Equality]
H
homi_fact.cat [in Beroal.CategoryTheory]homi.cat [in Beroal.CategoryTheory]
J
JMeq.t0 [in Beroal.Equality]JMeq.t1 [in Beroal.Equality]
JMeq.t2 [in Beroal.Equality]
L
list.e [in Beroal.NatBound]M
md.alg_md.m [in Beroal.CategoryTheory]md.cat [in Beroal.CategoryTheory]
md.md_proj.m [in Beroal.CategoryTheory]
P
poset_bound_fact.U [in Beroal.Subset]poset_bound_fact.r [in Beroal.Subset]
poset_bound_fact.s0 [in Beroal.Subset]
poset_bound_fact.ext_eq_axiom_local [in Beroal.Subset]
poset_bound.U [in Beroal.Subset]
poset_bound_fact.s1 [in Beroal.Subset]
poset_bound_fact.s [in Beroal.Subset]
R
relation_independent.b [in Beroal.Subset]relation_independent.r [in Beroal.Subset]
relation_independent.a [in Beroal.Subset]
S
subst_pair_fr.v0 [in Beroal.Equality]subst_mix.v0 [in Beroal.Equality]
subst_functor.type_fun [in Beroal.Equality]
subst_mix.eq01 [in Beroal.Equality]
subst_comm_f.eqt [in Beroal.Equality]
subst_pair_fr.eq01 [in Beroal.Equality]
subst_functor.eq12 [in Beroal.Equality]
subst_functor.t1 [in Beroal.Equality]
subst_functor.sort0 [in Beroal.Equality]
subst_functor.v0 [in Beroal.Equality]
subst_comm_f.t0 [in Beroal.Equality]
subst_mix.v1 [in Beroal.Equality]
subst_functor.eq01 [in Beroal.Equality]
subst_pair_fr.t0 [in Beroal.Equality]
subst_pair_fr.t1 [in Beroal.Equality]
subst_mix.t0 [in Beroal.Equality]
subst_comm_f.v0 [in Beroal.Equality]
subst_functor.t2 [in Beroal.Equality]
subst_functor.t0 [in Beroal.Equality]
subst_comm_f.t1 [in Beroal.Equality]
subst.t [in Beroal.Equality]
Library Index
A
AckermannC
CategoryTheoryE
EqualityF
FunExtEqFunListArg
I
InitIntBipart
L
ListMonadN
NatBoundS
StreamSubset
T
TakeDrop| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (611 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (125 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
This page has been generated by coqdoc