| 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 | (421 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 | (30 entries) |
| Module 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 | (3 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 | (11 entries) |
| Lemma 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 | (133 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 | (51 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 | (11 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 | (16 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 | (4 entries) |
| Instance 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 | (41 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 | (118 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 | (3 entries) |
Global Index
A
add_comm_related [lemma, in OpSemProofs.applications]add_zero_related [lemma, in OpSemProofs.applications]
applications [library]
apply_id_equiv [lemma, in OpSemProofs.applications]
apply_as_transformer [lemma, in OpSemProofs.relations]
apply_in [definition, in OpSemProofs.relations]
apply_G_rel [lemma, in OpSemProofs.relations]
apply_dG_rel [lemma, in OpSemProofs.determinism]
Arrow [constructor, in OpSemProofs.syntax]
A_rel_subidentity [lemma, in OpSemProofs.properties_of_relations]
A_rel_transitive [instance, in OpSemProofs.properties_of_relations]
A_rel_transitive' [instance, in OpSemProofs.properties_of_relations]
A_rel_symmetric [instance, in OpSemProofs.properties_of_relations]
A_rel_symmetric' [lemma, in OpSemProofs.properties_of_relations]
A_rel [definition, in OpSemProofs.relations]
A_rel' [definition, in OpSemProofs.relations]
B
beta_value [lemma, in OpSemProofs.applications]bichain [definition, in OpSemProofs.chain]
bichain_rect [lemma, in OpSemProofs.chain]
bichain_to_list [definition, in OpSemProofs.chain]
bichain_fold_right [definition, in OpSemProofs.chain]
bichain_cons [definition, in OpSemProofs.chain]
bicurry [definition, in OpSemProofs.chain]
bind_πL_πR [lemma, in OpSemProofs.integration]
bind_interchangable [lemma, in OpSemProofs.integration]
bind_meas_option [lemma, in OpSemProofs.integration]
bind_empty [lemma, in OpSemProofs.integration]
bool_of_dec [definition, in OpSemProofs.integration]
C
chain [inductive, in OpSemProofs.chain]chain [library]
chain_to_list [definition, in OpSemProofs.chain]
chain_fold_left [definition, in OpSemProofs.chain]
chain_fold_right [definition, in OpSemProofs.chain]
chain_snoc [definition, in OpSemProofs.chain]
chain_app_assoc [lemma, in OpSemProofs.chain]
chain_app_nil_r [lemma, in OpSemProofs.chain]
chain_app [definition, in OpSemProofs.chain]
chain_cons [constructor, in OpSemProofs.chain]
chain_nil [constructor, in OpSemProofs.chain]
close [lemma, in OpSemProofs.syntax]
closed_pure_is_val [lemma, in OpSemProofs.applications]
close_nil [lemma, in OpSemProofs.syntax]
coarsening [lemma, in OpSemProofs.integration]
coarsening' [lemma, in OpSemProofs.integration]
coarsen_helper [lemma, in OpSemProofs.relations]
compat_let [lemma, in OpSemProofs.applications]
compat_factor [lemma, in OpSemProofs.relations]
compat_sample [lemma, in OpSemProofs.relations]
compat_app [lemma, in OpSemProofs.relations]
compat_plus [lemma, in OpSemProofs.relations]
compat_lam [lemma, in OpSemProofs.relations]
compat_var [lemma, in OpSemProofs.relations]
compat_real [lemma, in OpSemProofs.relations]
compat_plug [lemma, in OpSemProofs.ctxequiv]
compat_plug1 [lemma, in OpSemProofs.ctxequiv]
compat_plus [lemma, in OpSemProofs.determinism]
compat_sample [lemma, in OpSemProofs.determinism]
compat_factor [lemma, in OpSemProofs.determinism]
compat_app [lemma, in OpSemProofs.determinism]
compat_lam [lemma, in OpSemProofs.determinism]
compat_var [lemma, in OpSemProofs.determinism]
compat_real [lemma, in OpSemProofs.determinism]
ctx [definition, in OpSemProofs.ctxequiv]
ctxequiv [library]
ctx_equiv [definition, in OpSemProofs.ctxequiv]
ctx_type_unique [lemma, in OpSemProofs.ctxequiv]
ctx_frame [inductive, in OpSemProofs.ctxequiv]
c_hole [definition, in OpSemProofs.ctxequiv]
c_lam [constructor, in OpSemProofs.ctxequiv]
c_plus_r [constructor, in OpSemProofs.ctxequiv]
c_plus_l [constructor, in OpSemProofs.ctxequiv]
c_factor [constructor, in OpSemProofs.ctxequiv]
c_app_a [constructor, in OpSemProofs.ctxequiv]
c_app_f [constructor, in OpSemProofs.ctxequiv]
D
dep_ids_ids [lemma, in OpSemProofs.applications]dep_ids [definition, in OpSemProofs.applications]
dep_ids' [definition, in OpSemProofs.applications]
dep_env_allT [definition, in OpSemProofs.syntax]
dep_map [definition, in OpSemProofs.syntax]
dep_lookup [definition, in OpSemProofs.syntax]
dep_cons [constructor, in OpSemProofs.syntax]
dep_nil [constructor, in OpSemProofs.syntax]
dep_list [inductive, in OpSemProofs.syntax]
determinism [library]
dE_rel [definition, in OpSemProofs.determinism]
dE_rel' [definition, in OpSemProofs.determinism]
dG_rel [definition, in OpSemProofs.determinism]
dirac [definition, in OpSemProofs.integration]
dV_rel [definition, in OpSemProofs.determinism]
dV_rel_arrow [inductive, in OpSemProofs.determinism]
dV_rel_real [definition, in OpSemProofs.determinism]
E
empty_env [definition, in OpSemProofs.syntax]empty_meas [definition, in OpSemProofs.integration]
ennr [inductive, in OpSemProofs.ennr]
ennr [library]
ennr_gt_dec [lemma, in OpSemProofs.ennr]
ennr_ge [definition, in OpSemProofs.ennr]
ennr_le [definition, in OpSemProofs.ennr]
ennr_gt [definition, in OpSemProofs.ennr]
ennr_lt [definition, in OpSemProofs.ennr]
ennr_semiring [definition, in OpSemProofs.ennr]
ennr_distr_l [lemma, in OpSemProofs.ennr]
ennr_mul_assoc [lemma, in OpSemProofs.ennr]
ennr_mul_comm [lemma, in OpSemProofs.ennr]
ennr_mul_0_l [lemma, in OpSemProofs.ennr]
ennr_mul_1_l [lemma, in OpSemProofs.ennr]
ennr_add_assoc [lemma, in OpSemProofs.ennr]
ennr_add_comm [lemma, in OpSemProofs.ennr]
ennr_add_0_l [lemma, in OpSemProofs.ennr]
ennr_mult [definition, in OpSemProofs.ennr]
ennr_plus [definition, in OpSemProofs.ennr]
ennr_1 [definition, in OpSemProofs.ennr]
ennr_0 [definition, in OpSemProofs.ennr]
Entropy [definition, in OpSemProofs.entropy]
entropy [library]
ent_finite [constructor, in OpSemProofs.integration]
Env [definition, in OpSemProofs.syntax]
env_search_subst [lemma, in OpSemProofs.syntax]
env_search [lemma, in OpSemProofs.syntax]
eq_pointwise [instance, in OpSemProofs.utils]
erase [definition, in OpSemProofs.syntax]
erase_simple [lemma, in OpSemProofs.applications]
erase_up_simple_ctx [lemma, in OpSemProofs.applications]
erase_simple_plug [lemma, in OpSemProofs.applications]
erase_simple_ctx [definition, in OpSemProofs.applications]
erase_plug [lemma, in OpSemProofs.applications]
erase_eq [lemma, in OpSemProofs.applications]
erase_envs_equiv [lemma, in OpSemProofs.syntax]
erase_wt_env [definition, in OpSemProofs.syntax]
erase_wt_expr_env [definition, in OpSemProofs.syntax]
erase_injective [lemma, in OpSemProofs.syntax]
erase_ctx_injective [lemma, in OpSemProofs.ctxequiv]
erase_cons [lemma, in OpSemProofs.ctxequiv]
erase_ctx [definition, in OpSemProofs.ctxequiv]
erase_ctx_frame [definition, in OpSemProofs.ctxequiv]
erase' [definition, in OpSemProofs.syntax]
ev [definition, in OpSemProofs.relations]
eval [inductive, in OpSemProofs.syntax]
eval_in [definition, in OpSemProofs.relations]
EVAL_plus [constructor, in OpSemProofs.syntax]
EVAL_sample [constructor, in OpSemProofs.syntax]
EVAL_factor [constructor, in OpSemProofs.syntax]
EVAL_app [constructor, in OpSemProofs.syntax]
EVAL_val [constructor, in OpSemProofs.syntax]
eval_dec.eval_dec [lemma, in OpSemProofs.determinism]
eval_dec.eval_dec_not_ex [constructor, in OpSemProofs.determinism]
eval_dec.eval_dec_ex_unique [constructor, in OpSemProofs.determinism]
eval_dec.eval_dec_result [inductive, in OpSemProofs.determinism]
eval_dec [module, in OpSemProofs.determinism]
Event [definition, in OpSemProofs.integration]
ew [definition, in OpSemProofs.relations]
expr [inductive, in OpSemProofs.syntax]
expr_lift_erase [lemma, in OpSemProofs.applications]
expr_lift [instance, in OpSemProofs.applications]
expr_eq_dec [lemma, in OpSemProofs.syntax]
expr_ren [lemma, in OpSemProofs.syntax]
expr_of_val [definition, in OpSemProofs.syntax]
expr_type_unique [lemma, in OpSemProofs.syntax]
extend_dgrel [lemma, in OpSemProofs.determinism]
E_rel_reflexive [instance, in OpSemProofs.properties_of_relations]
E_rel_transitive [instance, in OpSemProofs.properties_of_relations]
E_rel_transitive' [instance, in OpSemProofs.properties_of_relations]
E_rel_symmetric [instance, in OpSemProofs.properties_of_relations]
E_rel_symmetric' [lemma, in OpSemProofs.properties_of_relations]
e_seq [definition, in OpSemProofs.applications]
e_let [definition, in OpSemProofs.applications]
E_rel [definition, in OpSemProofs.relations]
E_rel' [definition, in OpSemProofs.relations]
e_plus [constructor, in OpSemProofs.syntax]
e_sample [constructor, in OpSemProofs.syntax]
e_factor [constructor, in OpSemProofs.syntax]
e_app [constructor, in OpSemProofs.syntax]
e_lam [constructor, in OpSemProofs.syntax]
e_var [constructor, in OpSemProofs.syntax]
e_real [constructor, in OpSemProofs.syntax]
F
factor_as_transformer [lemma, in OpSemProofs.relations]factor_in [definition, in OpSemProofs.relations]
finite [constructor, in OpSemProofs.ennr]
finite_inj [lemma, in OpSemProofs.ennr]
for_absurd_val [lemma, in OpSemProofs.syntax]
fromOption [definition, in OpSemProofs.utils]
full_event [definition, in OpSemProofs.integration]
functional_ext_rewriting2 [instance, in OpSemProofs.utils]
functional_ext_rewriting [instance, in OpSemProofs.utils]
fundamental_property [lemma, in OpSemProofs.relations]
fundamental_property [lemma, in OpSemProofs.determinism]
G
G_rel_reflexive [instance, in OpSemProofs.properties_of_relations]G_rel_transitive [instance, in OpSemProofs.properties_of_relations]
G_rel_symmetric [instance, in OpSemProofs.properties_of_relations]
G_rel_cons [constructor, in OpSemProofs.relations]
G_rel_nil [constructor, in OpSemProofs.relations]
G_rel [inductive, in OpSemProofs.relations]
I
Ids_u_expr [instance, in OpSemProofs.syntax]ifte [definition, in OpSemProofs.integration]
indicator [definition, in OpSemProofs.integration]
infinite [constructor, in OpSemProofs.ennr]
integration [axiom, in OpSemProofs.integration]
integration [library]
integration_const_entropy [lemma, in OpSemProofs.integration]
integration_of_pushforward [lemma, in OpSemProofs.integration]
integration_of_0 [lemma, in OpSemProofs.integration]
integration_linear_in_meas [lemma, in OpSemProofs.integration]
integration_linear_mult_l [lemma, in OpSemProofs.integration]
integration_linear_mult_r [lemma, in OpSemProofs.integration]
integration_πL_πR [axiom, in OpSemProofs.integration]
integration_of_indicator [axiom, in OpSemProofs.integration]
integration_linear [axiom, in OpSemProofs.integration]
interchangable [record, in OpSemProofs.integration]
interchangable [inductive, in OpSemProofs.integration]
interchangable_sym [definition, in OpSemProofs.integration]
interchange [projection, in OpSemProofs.integration]
interchange [constructor, in OpSemProofs.integration]
invert_eval_val [lemma, in OpSemProofs.syntax]
is_commutative [lemma, in OpSemProofs.applications]
is_u_simple [definition, in OpSemProofs.applications]
is_pure [definition, in OpSemProofs.applications]
is_val_unique [lemma, in OpSemProofs.syntax]
is_val [definition, in OpSemProofs.syntax]
J
join [definition, in OpSemProofs.entropy]join_πL_πR [lemma, in OpSemProofs.entropy]
join' [definition, in OpSemProofs.entropy]
K
kernel [definition, in OpSemProofs.integration]KnownToBeSigmaFinite [inductive, in OpSemProofs.integration]
L
lebesgue_pos_measure_interval [axiom, in OpSemProofs.integration]lebesgue_pos_measure [axiom, in OpSemProofs.integration]
leb_finite [constructor, in OpSemProofs.integration]
let_as_transformer [lemma, in OpSemProofs.applications]
let_in [definition, in OpSemProofs.applications]
let2_as_transformer [lemma, in OpSemProofs.applications]
Lift [module, in OpSemProofs.applications]
Lift.lift1 [projection, in OpSemProofs.applications]
Lift.lobj [projection, in OpSemProofs.applications]
Lift.mk [constructor, in OpSemProofs.applications]
Lift.type [record, in OpSemProofs.applications]
lift1 [definition, in OpSemProofs.applications]
lookup [definition, in OpSemProofs.syntax]
M
Meas [definition, in OpSemProofs.integration]meas_option_interchangable [instance, in OpSemProofs.integration]
meas_join [definition, in OpSemProofs.integration]
meas_id_right [lemma, in OpSemProofs.integration]
meas_id_left [lemma, in OpSemProofs.integration]
meas_option [definition, in OpSemProofs.integration]
meas_bind_assoc [axiom, in OpSemProofs.integration]
meas_bind [definition, in OpSemProofs.integration]
mk_V_rel_arrow [constructor, in OpSemProofs.relations]
mk_val [constructor, in OpSemProofs.syntax]
mk_dV_rel_arrow [constructor, in OpSemProofs.determinism]
O
open_subst1 [definition, in OpSemProofs.applications]option_bind [definition, in OpSemProofs.utils]
option_ap [definition, in OpSemProofs.utils]
option_meas [definition, in OpSemProofs.integration]
option0 [definition, in OpSemProofs.utils]
P
pick_2_entropies [lemma, in OpSemProofs.integration]pick_3_entropies [lemma, in OpSemProofs.integration]
pick_3_and_leftover [lemma, in OpSemProofs.integration]
plug [instance, in OpSemProofs.ctxequiv]
Plug [module, in OpSemProofs.ctxequiv]
plug_app [lemma, in OpSemProofs.applications]
plug_cons [definition, in OpSemProofs.ctxequiv]
plug_frame [instance, in OpSemProofs.ctxequiv]
Plug.mk [constructor, in OpSemProofs.ctxequiv]
Plug.plug [projection, in OpSemProofs.ctxequiv]
Plug.Plug [record, in OpSemProofs.ctxequiv]
plus_as_transformer [lemma, in OpSemProofs.relations]
plus_in [definition, in OpSemProofs.relations]
pointwise_eq_ext [instance, in OpSemProofs.utils]
pred_up [lemma, in OpSemProofs.applications]
preimage [definition, in OpSemProofs.integration]
project_same_integral [lemma, in OpSemProofs.applications]
properties_of_relations [library]
pushforward [definition, in OpSemProofs.integration]
pushforward_interchangable [instance, in OpSemProofs.integration]
R
refl_respectful [instance, in OpSemProofs.utils]related_exprs [definition, in OpSemProofs.relations]
related_expr [definition, in OpSemProofs.determinism]
relate_exprs [lemma, in OpSemProofs.properties_of_relations]
relations [library]
relation_sound [lemma, in OpSemProofs.ctxequiv]
rel_expr_reflexive [instance, in OpSemProofs.properties_of_relations]
rel_expr_transitive [instance, in OpSemProofs.properties_of_relations]
rel_expr_symmetric [instance, in OpSemProofs.properties_of_relations]
rename_simple_u_plug [lemma, in OpSemProofs.applications]
Rename_u_expr [instance, in OpSemProofs.syntax]
Rename_u_ctx [instance, in OpSemProofs.ctxequiv]
Rename_u_ctx_frame [instance, in OpSemProofs.ctxequiv]
rewrite_v_lam [definition, in OpSemProofs.syntax]
rewrite_v_real [definition, in OpSemProofs.syntax]
riemann_def_of_lebesgue_integration [axiom, in OpSemProofs.integration]
S
same_substitution_suffices [lemma, in OpSemProofs.properties_of_relations]score_meas_interchangable [instance, in OpSemProofs.integration]
score_meas [definition, in OpSemProofs.integration]
sigma_finite_is_interchangable [instance, in OpSemProofs.integration]
simple_cons_plug [lemma, in OpSemProofs.applications]
simple_ctx_frame_lift' [instance, in OpSemProofs.applications]
simple_ctx_frame_lift [definition, in OpSemProofs.applications]
simple_plug [instance, in OpSemProofs.applications]
simple_ctx_frame_rect [lemma, in OpSemProofs.applications]
simple_ctx [definition, in OpSemProofs.applications]
simple_ctx_frame [definition, in OpSemProofs.applications]
single_frame_case_plus_r [lemma, in OpSemProofs.applications]
single_frame_case_plus_l [lemma, in OpSemProofs.applications]
single_frame_case_factor [lemma, in OpSemProofs.applications]
single_frame_case_app_a [lemma, in OpSemProofs.applications]
single_frame_case_app_f [lemma, in OpSemProofs.applications]
subrel_eq_respect [instance, in OpSemProofs.utils]
SubstLemmas_u_expr [instance, in OpSemProofs.syntax]
subst_into_simple [lemma, in OpSemProofs.applications]
subst_real [lemma, in OpSemProofs.applications]
subst_lam [lemma, in OpSemProofs.applications]
subst_val [lemma, in OpSemProofs.applications]
subst_only_matters_up_to_env [lemma, in OpSemProofs.syntax]
Subst_u_expr [instance, in OpSemProofs.syntax]
syntax [library]
T
the_infinite_cons_doesnt_exist [lemma, in OpSemProofs.applications]tonelli_sigma_finite [axiom, in OpSemProofs.integration]
Ty [inductive, in OpSemProofs.syntax]
ty_swap [definition, in OpSemProofs.applications]
ty_subst1 [definition, in OpSemProofs.syntax]
ty_subst [lemma, in OpSemProofs.syntax]
ty_eq_dec [lemma, in OpSemProofs.syntax]
U
uc_hole [definition, in OpSemProofs.ctxequiv]uc_lam [constructor, in OpSemProofs.ctxequiv]
uc_plus_r [constructor, in OpSemProofs.ctxequiv]
uc_plus_l [constructor, in OpSemProofs.ctxequiv]
uc_factor [constructor, in OpSemProofs.ctxequiv]
uc_app_a [constructor, in OpSemProofs.ctxequiv]
uc_app_f [constructor, in OpSemProofs.ctxequiv]
unif_score_meas [definition, in OpSemProofs.integration]
unsimple [definition, in OpSemProofs.applications]
unsimple_cons [lemma, in OpSemProofs.applications]
up_app [lemma, in OpSemProofs.applications]
up_cons [lemma, in OpSemProofs.applications]
up_simple_ctx [instance, in OpSemProofs.applications]
up_simple_ctx' [definition, in OpSemProofs.applications]
up_expr_env [lemma, in OpSemProofs.syntax]
utils [library]
u_expr_eq_dec [lemma, in OpSemProofs.syntax]
u_var [constructor, in OpSemProofs.syntax]
u_lam [constructor, in OpSemProofs.syntax]
u_real [constructor, in OpSemProofs.syntax]
u_plus [constructor, in OpSemProofs.syntax]
u_sample [constructor, in OpSemProofs.syntax]
u_factor [constructor, in OpSemProofs.syntax]
u_app [constructor, in OpSemProofs.syntax]
u_expr [inductive, in OpSemProofs.syntax]
u_plug' [instance, in OpSemProofs.ctxequiv]
u_plug [definition, in OpSemProofs.ctxequiv]
u_plug_frame [instance, in OpSemProofs.ctxequiv]
u_ctx [definition, in OpSemProofs.ctxequiv]
u_ctx_frame [inductive, in OpSemProofs.ctxequiv]
V
val [inductive, in OpSemProofs.syntax]val_is_dirac [lemma, in OpSemProofs.relations]
val_real_rect [lemma, in OpSemProofs.syntax]
val_arrow_rect [definition, in OpSemProofs.syntax]
val_eq [lemma, in OpSemProofs.syntax]
var_swap [definition, in OpSemProofs.applications]
var_1 [definition, in OpSemProofs.applications]
var_0 [definition, in OpSemProofs.applications]
V_rel_reflexive [instance, in OpSemProofs.properties_of_relations]
V_rel_transitive [instance, in OpSemProofs.properties_of_relations]
V_rel_symmetric [instance, in OpSemProofs.properties_of_relations]
V_rel [definition, in OpSemProofs.relations]
V_rel_arrow [inductive, in OpSemProofs.relations]
V_rel_real [definition, in OpSemProofs.relations]
v_lam [definition, in OpSemProofs.syntax]
v_real [definition, in OpSemProofs.syntax]
W
weaken [definition, in OpSemProofs.syntax]weaken_lookup [lemma, in OpSemProofs.syntax]
wt_env [definition, in OpSemProofs.syntax]
wt_val_rect [lemma, in OpSemProofs.syntax]
other
R+ (type_scope) [notation, in OpSemProofs.ennr]_ :::: _ [notation, in OpSemProofs.chain]
_ +++ _ [notation, in OpSemProofs.chain]
_ ::: _ [notation, in OpSemProofs.chain]
_ <*> _ [notation, in OpSemProofs.utils]
_ <$> _ [notation, in OpSemProofs.utils]
_ ∘ _ [notation, in OpSemProofs.utils]
_ ↑ [notation, in OpSemProofs.applications]
_ ^ _ [notation, in OpSemProofs.applications]
_ ^ _ [notation, in OpSemProofs.applications]
_ +! _ [notation, in OpSemProofs.applications]
_ @ _ [notation, in OpSemProofs.applications]
_ >= _ [notation, in OpSemProofs.ennr]
_ > _ [notation, in OpSemProofs.ennr]
_ <= _ [notation, in OpSemProofs.ennr]
_ < _ [notation, in OpSemProofs.ennr]
_ * _ [notation, in OpSemProofs.ennr]
_ + _ [notation, in OpSemProofs.ennr]
_ ~> _ [notation, in OpSemProofs.syntax]
_ ⟨ _ ⟩ [notation, in OpSemProofs.ctxequiv]
_ >>= _ [notation, in OpSemProofs.integration]
CTX _ ⊢ [ _ ⊢ _ ] : _ [notation, in OpSemProofs.ctxequiv]
EVAL _ ⊢ _ ⇓ _ , _ [notation, in OpSemProofs.syntax]
EXP _ ⊢ _ ≈ _ : _ [notation, in OpSemProofs.relations]
FRAME _ ⊢ [ _ ⊢ _ ] : _ [notation, in OpSemProofs.ctxequiv]
SIMPLE _ ⊢ [ _ ] : _ [notation, in OpSemProofs.applications]
0 [notation, in OpSemProofs.ennr]
1 [notation, in OpSemProofs.ennr]
· [notation, in OpSemProofs.syntax]
λ, _ [notation, in OpSemProofs.applications]
ℝ [constructor, in OpSemProofs.syntax]
μ [definition, in OpSemProofs.relations]
μEntropy [axiom, in OpSemProofs.integration]
μEntropy_is_a_probability_measure [axiom, in OpSemProofs.integration]
μe_as_pushforard [lemma, in OpSemProofs.applications]
μe_eq_μEntropy2 [lemma, in OpSemProofs.relations]
μe_eq_μEntropy [lemma, in OpSemProofs.relations]
μ_interchangable' [lemma, in OpSemProofs.applications]
μ_interchangable [instance, in OpSemProofs.applications]
π [definition, in OpSemProofs.entropy]
πL [definition, in OpSemProofs.entropy]
πL_same_integral [lemma, in OpSemProofs.applications]
πL_join [lemma, in OpSemProofs.entropy]
πL_n [definition, in OpSemProofs.entropy]
πR [definition, in OpSemProofs.entropy]
πR_same_integral [lemma, in OpSemProofs.applications]
πR_join [lemma, in OpSemProofs.entropy]
πR_n [definition, in OpSemProofs.entropy]
π_S_join [lemma, in OpSemProofs.entropy]
π_O_join [lemma, in OpSemProofs.entropy]
π_leftover [definition, in OpSemProofs.entropy]
Notation Index
other
R+ (type_scope) [in OpSemProofs.ennr]_ :::: _ [in OpSemProofs.chain]
_ +++ _ [in OpSemProofs.chain]
_ ::: _ [in OpSemProofs.chain]
_ <*> _ [in OpSemProofs.utils]
_ <$> _ [in OpSemProofs.utils]
_ ∘ _ [in OpSemProofs.utils]
_ ↑ [in OpSemProofs.applications]
_ ^ _ [in OpSemProofs.applications]
_ ^ _ [in OpSemProofs.applications]
_ +! _ [in OpSemProofs.applications]
_ @ _ [in OpSemProofs.applications]
_ >= _ [in OpSemProofs.ennr]
_ > _ [in OpSemProofs.ennr]
_ <= _ [in OpSemProofs.ennr]
_ < _ [in OpSemProofs.ennr]
_ * _ [in OpSemProofs.ennr]
_ + _ [in OpSemProofs.ennr]
_ ~> _ [in OpSemProofs.syntax]
_ ⟨ _ ⟩ [in OpSemProofs.ctxequiv]
_ >>= _ [in OpSemProofs.integration]
CTX _ ⊢ [ _ ⊢ _ ] : _ [in OpSemProofs.ctxequiv]
EVAL _ ⊢ _ ⇓ _ , _ [in OpSemProofs.syntax]
EXP _ ⊢ _ ≈ _ : _ [in OpSemProofs.relations]
FRAME _ ⊢ [ _ ⊢ _ ] : _ [in OpSemProofs.ctxequiv]
SIMPLE _ ⊢ [ _ ] : _ [in OpSemProofs.applications]
0 [in OpSemProofs.ennr]
1 [in OpSemProofs.ennr]
· [in OpSemProofs.syntax]
λ, _ [in OpSemProofs.applications]
Module Index
E
eval_dec [in OpSemProofs.determinism]L
Lift [in OpSemProofs.applications]P
Plug [in OpSemProofs.ctxequiv]Library Index
A
applicationsC
chainctxequiv
D
determinismE
ennrentropy
I
integrationP
properties_of_relationsR
relationsS
syntaxU
utilsLemma Index
A
add_comm_related [in OpSemProofs.applications]add_zero_related [in OpSemProofs.applications]
apply_id_equiv [in OpSemProofs.applications]
apply_as_transformer [in OpSemProofs.relations]
apply_G_rel [in OpSemProofs.relations]
apply_dG_rel [in OpSemProofs.determinism]
A_rel_subidentity [in OpSemProofs.properties_of_relations]
A_rel_symmetric' [in OpSemProofs.properties_of_relations]
B
beta_value [in OpSemProofs.applications]bichain_rect [in OpSemProofs.chain]
bind_πL_πR [in OpSemProofs.integration]
bind_interchangable [in OpSemProofs.integration]
bind_meas_option [in OpSemProofs.integration]
bind_empty [in OpSemProofs.integration]
C
chain_app_assoc [in OpSemProofs.chain]chain_app_nil_r [in OpSemProofs.chain]
close [in OpSemProofs.syntax]
closed_pure_is_val [in OpSemProofs.applications]
close_nil [in OpSemProofs.syntax]
coarsening [in OpSemProofs.integration]
coarsening' [in OpSemProofs.integration]
coarsen_helper [in OpSemProofs.relations]
compat_let [in OpSemProofs.applications]
compat_factor [in OpSemProofs.relations]
compat_sample [in OpSemProofs.relations]
compat_app [in OpSemProofs.relations]
compat_plus [in OpSemProofs.relations]
compat_lam [in OpSemProofs.relations]
compat_var [in OpSemProofs.relations]
compat_real [in OpSemProofs.relations]
compat_plug [in OpSemProofs.ctxequiv]
compat_plug1 [in OpSemProofs.ctxequiv]
compat_plus [in OpSemProofs.determinism]
compat_sample [in OpSemProofs.determinism]
compat_factor [in OpSemProofs.determinism]
compat_app [in OpSemProofs.determinism]
compat_lam [in OpSemProofs.determinism]
compat_var [in OpSemProofs.determinism]
compat_real [in OpSemProofs.determinism]
ctx_type_unique [in OpSemProofs.ctxequiv]
D
dep_ids_ids [in OpSemProofs.applications]E
ennr_gt_dec [in OpSemProofs.ennr]ennr_distr_l [in OpSemProofs.ennr]
ennr_mul_assoc [in OpSemProofs.ennr]
ennr_mul_comm [in OpSemProofs.ennr]
ennr_mul_0_l [in OpSemProofs.ennr]
ennr_mul_1_l [in OpSemProofs.ennr]
ennr_add_assoc [in OpSemProofs.ennr]
ennr_add_comm [in OpSemProofs.ennr]
ennr_add_0_l [in OpSemProofs.ennr]
env_search_subst [in OpSemProofs.syntax]
env_search [in OpSemProofs.syntax]
erase_simple [in OpSemProofs.applications]
erase_up_simple_ctx [in OpSemProofs.applications]
erase_simple_plug [in OpSemProofs.applications]
erase_plug [in OpSemProofs.applications]
erase_eq [in OpSemProofs.applications]
erase_envs_equiv [in OpSemProofs.syntax]
erase_injective [in OpSemProofs.syntax]
erase_ctx_injective [in OpSemProofs.ctxequiv]
erase_cons [in OpSemProofs.ctxequiv]
eval_dec.eval_dec [in OpSemProofs.determinism]
expr_lift_erase [in OpSemProofs.applications]
expr_eq_dec [in OpSemProofs.syntax]
expr_ren [in OpSemProofs.syntax]
expr_type_unique [in OpSemProofs.syntax]
extend_dgrel [in OpSemProofs.determinism]
E_rel_symmetric' [in OpSemProofs.properties_of_relations]
F
factor_as_transformer [in OpSemProofs.relations]finite_inj [in OpSemProofs.ennr]
for_absurd_val [in OpSemProofs.syntax]
fundamental_property [in OpSemProofs.relations]
fundamental_property [in OpSemProofs.determinism]
I
integration_const_entropy [in OpSemProofs.integration]integration_of_pushforward [in OpSemProofs.integration]
integration_of_0 [in OpSemProofs.integration]
integration_linear_in_meas [in OpSemProofs.integration]
integration_linear_mult_l [in OpSemProofs.integration]
integration_linear_mult_r [in OpSemProofs.integration]
invert_eval_val [in OpSemProofs.syntax]
is_commutative [in OpSemProofs.applications]
is_val_unique [in OpSemProofs.syntax]
J
join_πL_πR [in OpSemProofs.entropy]L
let_as_transformer [in OpSemProofs.applications]let2_as_transformer [in OpSemProofs.applications]
M
meas_id_right [in OpSemProofs.integration]meas_id_left [in OpSemProofs.integration]
P
pick_2_entropies [in OpSemProofs.integration]pick_3_entropies [in OpSemProofs.integration]
pick_3_and_leftover [in OpSemProofs.integration]
plug_app [in OpSemProofs.applications]
plus_as_transformer [in OpSemProofs.relations]
pred_up [in OpSemProofs.applications]
project_same_integral [in OpSemProofs.applications]
R
relate_exprs [in OpSemProofs.properties_of_relations]relation_sound [in OpSemProofs.ctxequiv]
rename_simple_u_plug [in OpSemProofs.applications]
S
same_substitution_suffices [in OpSemProofs.properties_of_relations]simple_cons_plug [in OpSemProofs.applications]
simple_ctx_frame_rect [in OpSemProofs.applications]
single_frame_case_plus_r [in OpSemProofs.applications]
single_frame_case_plus_l [in OpSemProofs.applications]
single_frame_case_factor [in OpSemProofs.applications]
single_frame_case_app_a [in OpSemProofs.applications]
single_frame_case_app_f [in OpSemProofs.applications]
subst_into_simple [in OpSemProofs.applications]
subst_real [in OpSemProofs.applications]
subst_lam [in OpSemProofs.applications]
subst_val [in OpSemProofs.applications]
subst_only_matters_up_to_env [in OpSemProofs.syntax]
T
the_infinite_cons_doesnt_exist [in OpSemProofs.applications]ty_subst [in OpSemProofs.syntax]
ty_eq_dec [in OpSemProofs.syntax]
U
unsimple_cons [in OpSemProofs.applications]up_app [in OpSemProofs.applications]
up_cons [in OpSemProofs.applications]
up_expr_env [in OpSemProofs.syntax]
u_expr_eq_dec [in OpSemProofs.syntax]
V
val_is_dirac [in OpSemProofs.relations]val_real_rect [in OpSemProofs.syntax]
val_eq [in OpSemProofs.syntax]
W
weaken_lookup [in OpSemProofs.syntax]wt_val_rect [in OpSemProofs.syntax]
other
μe_as_pushforard [in OpSemProofs.applications]μe_eq_μEntropy2 [in OpSemProofs.relations]
μe_eq_μEntropy [in OpSemProofs.relations]
μ_interchangable' [in OpSemProofs.applications]
πL_same_integral [in OpSemProofs.applications]
πL_join [in OpSemProofs.entropy]
πR_same_integral [in OpSemProofs.applications]
πR_join [in OpSemProofs.entropy]
π_S_join [in OpSemProofs.entropy]
π_O_join [in OpSemProofs.entropy]
Constructor Index
A
Arrow [in OpSemProofs.syntax]C
chain_cons [in OpSemProofs.chain]chain_nil [in OpSemProofs.chain]
c_lam [in OpSemProofs.ctxequiv]
c_plus_r [in OpSemProofs.ctxequiv]
c_plus_l [in OpSemProofs.ctxequiv]
c_factor [in OpSemProofs.ctxequiv]
c_app_a [in OpSemProofs.ctxequiv]
c_app_f [in OpSemProofs.ctxequiv]
D
dep_cons [in OpSemProofs.syntax]dep_nil [in OpSemProofs.syntax]
E
ent_finite [in OpSemProofs.integration]EVAL_plus [in OpSemProofs.syntax]
EVAL_sample [in OpSemProofs.syntax]
EVAL_factor [in OpSemProofs.syntax]
EVAL_app [in OpSemProofs.syntax]
EVAL_val [in OpSemProofs.syntax]
eval_dec.eval_dec_not_ex [in OpSemProofs.determinism]
eval_dec.eval_dec_ex_unique [in OpSemProofs.determinism]
e_plus [in OpSemProofs.syntax]
e_sample [in OpSemProofs.syntax]
e_factor [in OpSemProofs.syntax]
e_app [in OpSemProofs.syntax]
e_lam [in OpSemProofs.syntax]
e_var [in OpSemProofs.syntax]
e_real [in OpSemProofs.syntax]
F
finite [in OpSemProofs.ennr]G
G_rel_cons [in OpSemProofs.relations]G_rel_nil [in OpSemProofs.relations]
I
infinite [in OpSemProofs.ennr]interchange [in OpSemProofs.integration]
L
leb_finite [in OpSemProofs.integration]Lift.mk [in OpSemProofs.applications]
M
mk_V_rel_arrow [in OpSemProofs.relations]mk_val [in OpSemProofs.syntax]
mk_dV_rel_arrow [in OpSemProofs.determinism]
P
Plug.mk [in OpSemProofs.ctxequiv]U
uc_lam [in OpSemProofs.ctxequiv]uc_plus_r [in OpSemProofs.ctxequiv]
uc_plus_l [in OpSemProofs.ctxequiv]
uc_factor [in OpSemProofs.ctxequiv]
uc_app_a [in OpSemProofs.ctxequiv]
uc_app_f [in OpSemProofs.ctxequiv]
u_var [in OpSemProofs.syntax]
u_lam [in OpSemProofs.syntax]
u_real [in OpSemProofs.syntax]
u_plus [in OpSemProofs.syntax]
u_sample [in OpSemProofs.syntax]
u_factor [in OpSemProofs.syntax]
u_app [in OpSemProofs.syntax]
other
ℝ [in OpSemProofs.syntax]Axiom Index
I
integration [in OpSemProofs.integration]integration_πL_πR [in OpSemProofs.integration]
integration_of_indicator [in OpSemProofs.integration]
integration_linear [in OpSemProofs.integration]
L
lebesgue_pos_measure_interval [in OpSemProofs.integration]lebesgue_pos_measure [in OpSemProofs.integration]
M
meas_bind_assoc [in OpSemProofs.integration]R
riemann_def_of_lebesgue_integration [in OpSemProofs.integration]T
tonelli_sigma_finite [in OpSemProofs.integration]other
μEntropy [in OpSemProofs.integration]μEntropy_is_a_probability_measure [in OpSemProofs.integration]
Inductive Index
C
chain [in OpSemProofs.chain]ctx_frame [in OpSemProofs.ctxequiv]
D
dep_list [in OpSemProofs.syntax]dV_rel_arrow [in OpSemProofs.determinism]
E
ennr [in OpSemProofs.ennr]eval [in OpSemProofs.syntax]
eval_dec.eval_dec_result [in OpSemProofs.determinism]
expr [in OpSemProofs.syntax]
G
G_rel [in OpSemProofs.relations]I
interchangable [in OpSemProofs.integration]K
KnownToBeSigmaFinite [in OpSemProofs.integration]T
Ty [in OpSemProofs.syntax]U
u_expr [in OpSemProofs.syntax]u_ctx_frame [in OpSemProofs.ctxequiv]
V
val [in OpSemProofs.syntax]V_rel_arrow [in OpSemProofs.relations]
Projection Index
I
interchange [in OpSemProofs.integration]L
Lift.lift1 [in OpSemProofs.applications]Lift.lobj [in OpSemProofs.applications]
P
Plug.plug [in OpSemProofs.ctxequiv]Instance Index
A
A_rel_transitive [in OpSemProofs.properties_of_relations]A_rel_transitive' [in OpSemProofs.properties_of_relations]
A_rel_symmetric [in OpSemProofs.properties_of_relations]
E
eq_pointwise [in OpSemProofs.utils]expr_lift [in OpSemProofs.applications]
E_rel_reflexive [in OpSemProofs.properties_of_relations]
E_rel_transitive [in OpSemProofs.properties_of_relations]
E_rel_transitive' [in OpSemProofs.properties_of_relations]
E_rel_symmetric [in OpSemProofs.properties_of_relations]
F
functional_ext_rewriting2 [in OpSemProofs.utils]functional_ext_rewriting [in OpSemProofs.utils]
G
G_rel_reflexive [in OpSemProofs.properties_of_relations]G_rel_transitive [in OpSemProofs.properties_of_relations]
G_rel_symmetric [in OpSemProofs.properties_of_relations]
I
Ids_u_expr [in OpSemProofs.syntax]M
meas_option_interchangable [in OpSemProofs.integration]P
plug [in OpSemProofs.ctxequiv]plug_frame [in OpSemProofs.ctxequiv]
pointwise_eq_ext [in OpSemProofs.utils]
pushforward_interchangable [in OpSemProofs.integration]
R
refl_respectful [in OpSemProofs.utils]rel_expr_reflexive [in OpSemProofs.properties_of_relations]
rel_expr_transitive [in OpSemProofs.properties_of_relations]
rel_expr_symmetric [in OpSemProofs.properties_of_relations]
Rename_u_expr [in OpSemProofs.syntax]
Rename_u_ctx [in OpSemProofs.ctxequiv]
Rename_u_ctx_frame [in OpSemProofs.ctxequiv]
S
score_meas_interchangable [in OpSemProofs.integration]sigma_finite_is_interchangable [in OpSemProofs.integration]
simple_ctx_frame_lift' [in OpSemProofs.applications]
simple_plug [in OpSemProofs.applications]
subrel_eq_respect [in OpSemProofs.utils]
SubstLemmas_u_expr [in OpSemProofs.syntax]
Subst_u_expr [in OpSemProofs.syntax]
U
up_simple_ctx [in OpSemProofs.applications]u_plug' [in OpSemProofs.ctxequiv]
u_plug_frame [in OpSemProofs.ctxequiv]
V
V_rel_reflexive [in OpSemProofs.properties_of_relations]V_rel_transitive [in OpSemProofs.properties_of_relations]
V_rel_symmetric [in OpSemProofs.properties_of_relations]
other
μ_interchangable [in OpSemProofs.applications]Definition Index
A
apply_in [in OpSemProofs.relations]A_rel [in OpSemProofs.relations]
A_rel' [in OpSemProofs.relations]
B
bichain [in OpSemProofs.chain]bichain_to_list [in OpSemProofs.chain]
bichain_fold_right [in OpSemProofs.chain]
bichain_cons [in OpSemProofs.chain]
bicurry [in OpSemProofs.chain]
bool_of_dec [in OpSemProofs.integration]
C
chain_to_list [in OpSemProofs.chain]chain_fold_left [in OpSemProofs.chain]
chain_fold_right [in OpSemProofs.chain]
chain_snoc [in OpSemProofs.chain]
chain_app [in OpSemProofs.chain]
ctx [in OpSemProofs.ctxequiv]
ctx_equiv [in OpSemProofs.ctxequiv]
c_hole [in OpSemProofs.ctxequiv]
D
dep_ids [in OpSemProofs.applications]dep_ids' [in OpSemProofs.applications]
dep_env_allT [in OpSemProofs.syntax]
dep_map [in OpSemProofs.syntax]
dep_lookup [in OpSemProofs.syntax]
dE_rel [in OpSemProofs.determinism]
dE_rel' [in OpSemProofs.determinism]
dG_rel [in OpSemProofs.determinism]
dirac [in OpSemProofs.integration]
dV_rel [in OpSemProofs.determinism]
dV_rel_real [in OpSemProofs.determinism]
E
empty_env [in OpSemProofs.syntax]empty_meas [in OpSemProofs.integration]
ennr_ge [in OpSemProofs.ennr]
ennr_le [in OpSemProofs.ennr]
ennr_gt [in OpSemProofs.ennr]
ennr_lt [in OpSemProofs.ennr]
ennr_semiring [in OpSemProofs.ennr]
ennr_mult [in OpSemProofs.ennr]
ennr_plus [in OpSemProofs.ennr]
ennr_1 [in OpSemProofs.ennr]
ennr_0 [in OpSemProofs.ennr]
Entropy [in OpSemProofs.entropy]
Env [in OpSemProofs.syntax]
erase [in OpSemProofs.syntax]
erase_simple_ctx [in OpSemProofs.applications]
erase_wt_env [in OpSemProofs.syntax]
erase_wt_expr_env [in OpSemProofs.syntax]
erase_ctx [in OpSemProofs.ctxequiv]
erase_ctx_frame [in OpSemProofs.ctxequiv]
erase' [in OpSemProofs.syntax]
ev [in OpSemProofs.relations]
eval_in [in OpSemProofs.relations]
Event [in OpSemProofs.integration]
ew [in OpSemProofs.relations]
expr_of_val [in OpSemProofs.syntax]
e_seq [in OpSemProofs.applications]
e_let [in OpSemProofs.applications]
E_rel [in OpSemProofs.relations]
E_rel' [in OpSemProofs.relations]
F
factor_in [in OpSemProofs.relations]fromOption [in OpSemProofs.utils]
full_event [in OpSemProofs.integration]
I
ifte [in OpSemProofs.integration]indicator [in OpSemProofs.integration]
interchangable_sym [in OpSemProofs.integration]
is_u_simple [in OpSemProofs.applications]
is_pure [in OpSemProofs.applications]
is_val [in OpSemProofs.syntax]
J
join [in OpSemProofs.entropy]join' [in OpSemProofs.entropy]
K
kernel [in OpSemProofs.integration]L
let_in [in OpSemProofs.applications]lift1 [in OpSemProofs.applications]
lookup [in OpSemProofs.syntax]
M
Meas [in OpSemProofs.integration]meas_join [in OpSemProofs.integration]
meas_option [in OpSemProofs.integration]
meas_bind [in OpSemProofs.integration]
O
open_subst1 [in OpSemProofs.applications]option_bind [in OpSemProofs.utils]
option_ap [in OpSemProofs.utils]
option_meas [in OpSemProofs.integration]
option0 [in OpSemProofs.utils]
P
plug_cons [in OpSemProofs.ctxequiv]plus_in [in OpSemProofs.relations]
preimage [in OpSemProofs.integration]
pushforward [in OpSemProofs.integration]
R
related_exprs [in OpSemProofs.relations]related_expr [in OpSemProofs.determinism]
rewrite_v_lam [in OpSemProofs.syntax]
rewrite_v_real [in OpSemProofs.syntax]
S
score_meas [in OpSemProofs.integration]simple_ctx_frame_lift [in OpSemProofs.applications]
simple_ctx [in OpSemProofs.applications]
simple_ctx_frame [in OpSemProofs.applications]
T
ty_swap [in OpSemProofs.applications]ty_subst1 [in OpSemProofs.syntax]
U
uc_hole [in OpSemProofs.ctxequiv]unif_score_meas [in OpSemProofs.integration]
unsimple [in OpSemProofs.applications]
up_simple_ctx' [in OpSemProofs.applications]
u_plug [in OpSemProofs.ctxequiv]
u_ctx [in OpSemProofs.ctxequiv]
V
val_arrow_rect [in OpSemProofs.syntax]var_swap [in OpSemProofs.applications]
var_1 [in OpSemProofs.applications]
var_0 [in OpSemProofs.applications]
V_rel [in OpSemProofs.relations]
V_rel_real [in OpSemProofs.relations]
v_lam [in OpSemProofs.syntax]
v_real [in OpSemProofs.syntax]
W
weaken [in OpSemProofs.syntax]wt_env [in OpSemProofs.syntax]
other
μ [in OpSemProofs.relations]π [in OpSemProofs.entropy]
πL [in OpSemProofs.entropy]
πL_n [in OpSemProofs.entropy]
πR [in OpSemProofs.entropy]
πR_n [in OpSemProofs.entropy]
π_leftover [in OpSemProofs.entropy]
Record Index
I
interchangable [in OpSemProofs.integration]L
Lift.type [in OpSemProofs.applications]P
Plug.Plug [in OpSemProofs.ctxequiv]| 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 | (421 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 | (30 entries) |
| Module 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 | (3 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 | (11 entries) |
| Lemma 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 | (133 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 | (51 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 | (11 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 | (16 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 | (4 entries) |
| Instance 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 | (41 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 | (118 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 | (3 entries) |