| 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 | (243 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 | (4 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 | (5 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 | (1 entry) |
| 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 | (94 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 | (9 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 | (9 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 | (1 entry) |
| 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 | (27 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 | (90 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
addR [definition, in Oracle]addR2 [definition, in Oracle]
addUser [definition, in Oracle]
alpha [axiom, in Oracle]
B
B [projection, in Oracle]balance [definition, in Oracle]
blacklist_vote_preserves_mean_fields [lemma, in Oracle]
blacklist_vote [definition, in Oracle]
B_oracle_pos_preserved_step [lemma, in Oracle]
B_oracle_step_funding [lemma, in Oracle]
B_oracle_step_reward [lemma, in Oracle]
B_oracle_step_no_reward [lemma, in Oracle]
B_user_w_nonneg_hyp [axiom, in Oracle]
B_oracle_r [projection, in Oracle]
B_oracle_w [projection, in Oracle]
B_user_r [projection, in Oracle]
B_user_w [projection, in Oracle]
D
decay [definition, in Oracle]decay_between_0_1 [lemma, in Oracle]
decay_pos [lemma, in Oracle]
decay_0 [lemma, in Oracle]
decay_add [lemma, in Oracle]
Delta_wd [axiom, in Oracle]
Delta_dep [axiom, in Oracle]
denom_pos_exists_wu_pos [lemma, in Oracle]
Deposit [constructor, in Oracle]
div_le_1 [lemma, in Oracle]
E
eq38_at [definition, in Oracle]exec_prefix [definition, in Oracle]
exec_trace [definition, in Oracle]
exec_op_preserves_TW_if_not_submit [lemma, in Oracle]
exec_op [definition, in Oracle]
exp_neg_lt_1 [lemma, in Oracle]
exp2_dominates_linear [lemma, in Oracle]
F
fold_left_white_preserves_mean_fields [lemma, in Oracle]fold_left_black_preserves_mean_fields [lemma, in Oracle]
fold_left_preserves_getR_W_user [lemma, in Oracle]
fold_left_preserves_getR_T_user [lemma, in Oracle]
fold_left_preserves_TW [lemma, in Oracle]
Forall2_map_l [lemma, in Oracle]
G
G [projection, in Oracle]getBool [definition, in Oracle]
getR [definition, in Oracle]
getR_setR_neq [lemma, in Oracle]
getR_setR_eq [lemma, in Oracle]
getR2 [definition, in Oracle]
getUserSet [definition, in Oracle]
GovernanceState [record, in Oracle]
H
h [axiom, in Oracle]history [definition, in Oracle]
I
ideal_num_at_submission_time [definition, in Oracle]ideal_Q_at_submission_time [definition, in Oracle]
inactive_oracle_operator_delay [lemma, in Oracle]
inactive_implies_TW_eventually_constant [lemma, in Oracle]
inactive_along_run [definition, in Oracle]
init_mean_raw [lemma, in Oracle]
init_state [definition, in Oracle]
init_oracle [definition, in Oracle]
init_governance [definition, in Oracle]
init_B_oracle_r [definition, in Oracle]
init_B_oracle_w [definition, in Oracle]
init_B_user_r [definition, in Oracle]
init_B_user_w [definition, in Oracle]
isBlacklisted [definition, in Oracle]
is_reward_funding_dec [lemma, in Oracle]
is_submission_dec [lemma, in Oracle]
is_reward_funding [definition, in Oracle]
is_submission [definition, in Oracle]
is_submission_by [definition, in Oracle]
L
Lambda [definition, in Oracle]Lambda_x_le [lemma, in Oracle]
Lambda_x_eq38_at [lemma, in Oracle]
Lambda_u_rewrite_38 [lemma, in Oracle]
Lambda_run [definition, in Oracle]
Lambda_x [definition, in Oracle]
lift_oracle_state [definition, in Oracle]
ln_gt_1_gt_0 [lemma, in Oracle]
L_f_nonneg_hyp [axiom, in Oracle]
L_tot [projection, in Oracle]
L_f [projection, in Oracle]
L_l [projection, in Oracle]
M
mean_raw_eq_along_run [lemma, in Oracle]mean_raw_eq_preserved_step [lemma, in Oracle]
mean_raw_eq_preserved_noneop [lemma, in Oracle]
mean_raw_eq_preserved_reward_funding [lemma, in Oracle]
mean_raw_eq_preserved_weight_sync [lemma, in Oracle]
mean_raw_eq_preserved_whitelist_vote [lemma, in Oracle]
mean_raw_eq_preserved_blacklist_vote [lemma, in Oracle]
mean_raw_eq_preserved_reading [lemma, in Oracle]
mean_raw_eq_preserved_withdrawal [lemma, in Oracle]
mean_raw_eq_preserved_deposit [lemma, in Oracle]
mean_eq_curr_pbar_preserved_submission [lemma, in Oracle]
mean_raw_eq_implies_mean_eq_curr_pbar [lemma, in Oracle]
mean_eq_curr_pbar [definition, in Oracle]
mean_raw_eq_preserved_submission [lemma, in Oracle]
mean_raw_eq [definition, in Oracle]
mem_user [definition, in Oracle]
mul_le_1_of_le_1 [lemma, in Oracle]
M_white [projection, in Oracle]
M_black [projection, in Oracle]
N
NoneOp [constructor, in Oracle]O
one_minus_alpha_x_pos [lemma, in Oracle]Operation [inductive, in Oracle]
Operation_sind [definition, in Oracle]
Operation_rec [definition, in Oracle]
Operation_ind [definition, in Oracle]
Operation_rect [definition, in Oracle]
optimally_small_oracle_delay [lemma, in Oracle]
op_at [definition, in Oracle]
Oracle [library]
OracleState [record, in Oracle]
P
pbar [projection, in Oracle]pbar_decayed [definition, in Oracle]
pbar' [definition, in Oracle]
pbar'_eq_P_submitted_state [lemma, in Oracle]
pbar'_eq_sum_PWdecay [lemma, in Oracle]
Phist [projection, in Oracle]
proj1_rpos_pos [lemma, in Oracle]
ptilde [projection, in Oracle]
pu [definition, in Oracle]
P_equiv_pbar [lemma, in Oracle]
P_ [definition, in Oracle]
P_user [projection, in Oracle]
Q
Q [projection, in Oracle]q [axiom, in Oracle]
Q_decayed [definition, in Oracle]
Q' [definition, in Oracle]
Q'_eq_sum_Wdecay [lemma, in Oracle]
R
Rabs_div [lemma, in Oracle]reachable [definition, in Oracle]
Reading [constructor, in Oracle]
Recompute [definition, in Oracle]
Recompute_preserves_mean_fields [lemma, in Oracle]
Recompute_preserves_W_user [lemma, in Oracle]
Recompute_preserves_T_user [lemma, in Oracle]
remove_not_in [lemma, in Oracle]
RewardFunding [constructor, in Oracle]
reward_funding_preserves_mean_fields [lemma, in Oracle]
reward_funding [definition, in Oracle]
reward_payout [definition, in Oracle]
Reweight [definition, in Oracle]
Reweight_preserves_mean_fields [lemma, in Oracle]
reweight_white_step_preserves_mean_fields [lemma, in Oracle]
reweight_black_step_preserves_mean_fields [lemma, in Oracle]
Reweight_preserves_W_user [lemma, in Oracle]
Reweight_preserves_T_user [lemma, in Oracle]
reweight_white_step_preserves_W_user [lemma, in Oracle]
reweight_white_step_preserves_T_user [lemma, in Oracle]
reweight_black_step_preserves_W_user [lemma, in Oracle]
reweight_black_step_preserves_T_user [lemma, in Oracle]
reweight_white_step [definition, in Oracle]
reweight_black_step [definition, in Oracle]
Rgeb [definition, in Oracle]
Rgtb [definition, in Oracle]
Rleb [definition, in Oracle]
Rltb [definition, in Oracle]
Rpos [definition, in Oracle]
Rpower_2_nonneg [lemma, in Oracle]
Rpower_2_pos [lemma, in Oracle]
Run [definition, in Oracle]
S
setBool [definition, in Oracle]setR [definition, in Oracle]
setR2 [definition, in Oracle]
setUserSet [definition, in Oracle]
State [record, in Oracle]
state_at_S [lemma, in Oracle]
state_at [definition, in Oracle]
Submission [constructor, in Oracle]
submission_assumptions [definition, in Oracle]
submission_assumptions_at [definition, in Oracle]
submission_den_sum_pos [lemma, in Oracle]
submission_den_eq_factored_den [lemma, in Oracle]
submission_num_eq_factored_num [lemma, in Oracle]
submitted_oracle_state [definition, in Oracle]
sum_split_remove [lemma, in Oracle]
sum_list_R_ge_member [lemma, in Oracle]
sum_list_R_nn_exists_pos_pos [lemma, in Oracle]
sum_list_R_nonneg_nonneg [lemma, in Oracle]
sum_list_R_pos_of_one_pos [lemma, in Oracle]
sum_list_R_nonneg [lemma, in Oracle]
sum_list_R_map_mult_const [lemma, in Oracle]
sum_list_R_le [lemma, in Oracle]
sum_list_R [definition, in Oracle]
sustainable_rewards [lemma, in Oracle]
T
tends_to_0_seq_ext [lemma, in Oracle]tends_to_0_seq [definition, in Oracle]
timestamp [definition, in Oracle]
token_withdrawal_preserves_mean_fields [lemma, in Oracle]
token_deposit_preserves_mean_fields [lemma, in Oracle]
token_withdrawal [definition, in Oracle]
token_deposit [definition, in Oracle]
Trace [definition, in Oracle]
tstar [definition, in Oracle]
tstar_le_tu [lemma, in Oracle]
tu [definition, in Oracle]
t_last [projection, in Oracle]
t_sub [projection, in Oracle]
T_user [projection, in Oracle]
T_op [projection, in Oracle]
T_dep [projection, in Oracle]
U
UMap_forall [definition, in Oracle]UMFacts [module, in Oracle]
Unlock [definition, in Oracle]
Unlock_preserves_tu [lemma, in Oracle]
Unlock_preserves_mean_fields [lemma, in Oracle]
Unlock_preserves_TW [lemma, in Oracle]
UPairMap_forall [definition, in Oracle]
User [definition, in Oracle]
UserMap [module, in Oracle]
UserOT [module, in Oracle]
UserPairMap [module, in Oracle]
UserPairOT [module, in Oracle]
Users [axiom, in Oracle]
UserSet [definition, in Oracle]
Users_NoDup [axiom, in Oracle]
V
V [projection, in Oracle]value [definition, in Oracle]
value_reading_preserves_mean_fields [lemma, in Oracle]
value_reading [definition, in Oracle]
value_submission [definition, in Oracle]
VoteBlacklist [constructor, in Oracle]
VoteWhitelist [constructor, in Oracle]
V_white [projection, in Oracle]
V_black [projection, in Oracle]
W
w [definition, in Oracle]weight [definition, in Oracle]
WeightSync [constructor, in Oracle]
weight_synchronization_preserves_mean_fields [lemma, in Oracle]
weight_synchronization [definition, in Oracle]
whitelist_vote_preserves_mean_fields [lemma, in Oracle]
whitelist_vote [definition, in Oracle]
Withdrawal [constructor, in Oracle]
wu [definition, in Oracle]
w_le_Q' [lemma, in Oracle]
W_decayed_nonneg [lemma, in Oracle]
W_decayed [definition, in Oracle]
W_user [projection, in Oracle]
W_white [projection, in Oracle]
W_black [projection, in Oracle]
other
_ >b _ [notation, in Oracle]_ >=b _ [notation, in Oracle]
_ <b _ [notation, in Oracle]
_ <=b _ [notation, in Oracle]
Notation Index
other
_ >b _ [in Oracle]_ >=b _ [in Oracle]
_ <b _ [in Oracle]
_ <=b _ [in Oracle]
Module Index
U
UMFacts [in Oracle]UserMap [in Oracle]
UserOT [in Oracle]
UserPairMap [in Oracle]
UserPairOT [in Oracle]
Library Index
O
OracleLemma Index
B
blacklist_vote_preserves_mean_fields [in Oracle]B_oracle_pos_preserved_step [in Oracle]
B_oracle_step_funding [in Oracle]
B_oracle_step_reward [in Oracle]
B_oracle_step_no_reward [in Oracle]
D
decay_between_0_1 [in Oracle]decay_pos [in Oracle]
decay_0 [in Oracle]
decay_add [in Oracle]
denom_pos_exists_wu_pos [in Oracle]
div_le_1 [in Oracle]
E
exec_op_preserves_TW_if_not_submit [in Oracle]exp_neg_lt_1 [in Oracle]
exp2_dominates_linear [in Oracle]
F
fold_left_white_preserves_mean_fields [in Oracle]fold_left_black_preserves_mean_fields [in Oracle]
fold_left_preserves_getR_W_user [in Oracle]
fold_left_preserves_getR_T_user [in Oracle]
fold_left_preserves_TW [in Oracle]
Forall2_map_l [in Oracle]
G
getR_setR_neq [in Oracle]getR_setR_eq [in Oracle]
I
inactive_oracle_operator_delay [in Oracle]inactive_implies_TW_eventually_constant [in Oracle]
init_mean_raw [in Oracle]
is_reward_funding_dec [in Oracle]
is_submission_dec [in Oracle]
L
Lambda_x_le [in Oracle]Lambda_x_eq38_at [in Oracle]
Lambda_u_rewrite_38 [in Oracle]
ln_gt_1_gt_0 [in Oracle]
M
mean_raw_eq_along_run [in Oracle]mean_raw_eq_preserved_step [in Oracle]
mean_raw_eq_preserved_noneop [in Oracle]
mean_raw_eq_preserved_reward_funding [in Oracle]
mean_raw_eq_preserved_weight_sync [in Oracle]
mean_raw_eq_preserved_whitelist_vote [in Oracle]
mean_raw_eq_preserved_blacklist_vote [in Oracle]
mean_raw_eq_preserved_reading [in Oracle]
mean_raw_eq_preserved_withdrawal [in Oracle]
mean_raw_eq_preserved_deposit [in Oracle]
mean_eq_curr_pbar_preserved_submission [in Oracle]
mean_raw_eq_implies_mean_eq_curr_pbar [in Oracle]
mean_raw_eq_preserved_submission [in Oracle]
mul_le_1_of_le_1 [in Oracle]
O
one_minus_alpha_x_pos [in Oracle]optimally_small_oracle_delay [in Oracle]
P
pbar'_eq_P_submitted_state [in Oracle]pbar'_eq_sum_PWdecay [in Oracle]
proj1_rpos_pos [in Oracle]
P_equiv_pbar [in Oracle]
Q
Q'_eq_sum_Wdecay [in Oracle]R
Rabs_div [in Oracle]Recompute_preserves_mean_fields [in Oracle]
Recompute_preserves_W_user [in Oracle]
Recompute_preserves_T_user [in Oracle]
remove_not_in [in Oracle]
reward_funding_preserves_mean_fields [in Oracle]
Reweight_preserves_mean_fields [in Oracle]
reweight_white_step_preserves_mean_fields [in Oracle]
reweight_black_step_preserves_mean_fields [in Oracle]
Reweight_preserves_W_user [in Oracle]
Reweight_preserves_T_user [in Oracle]
reweight_white_step_preserves_W_user [in Oracle]
reweight_white_step_preserves_T_user [in Oracle]
reweight_black_step_preserves_W_user [in Oracle]
reweight_black_step_preserves_T_user [in Oracle]
Rpower_2_nonneg [in Oracle]
Rpower_2_pos [in Oracle]
S
state_at_S [in Oracle]submission_den_sum_pos [in Oracle]
submission_den_eq_factored_den [in Oracle]
submission_num_eq_factored_num [in Oracle]
sum_split_remove [in Oracle]
sum_list_R_ge_member [in Oracle]
sum_list_R_nn_exists_pos_pos [in Oracle]
sum_list_R_nonneg_nonneg [in Oracle]
sum_list_R_pos_of_one_pos [in Oracle]
sum_list_R_nonneg [in Oracle]
sum_list_R_map_mult_const [in Oracle]
sum_list_R_le [in Oracle]
sustainable_rewards [in Oracle]
T
tends_to_0_seq_ext [in Oracle]token_withdrawal_preserves_mean_fields [in Oracle]
token_deposit_preserves_mean_fields [in Oracle]
tstar_le_tu [in Oracle]
U
Unlock_preserves_tu [in Oracle]Unlock_preserves_mean_fields [in Oracle]
Unlock_preserves_TW [in Oracle]
V
value_reading_preserves_mean_fields [in Oracle]W
weight_synchronization_preserves_mean_fields [in Oracle]whitelist_vote_preserves_mean_fields [in Oracle]
w_le_Q' [in Oracle]
W_decayed_nonneg [in Oracle]
Axiom Index
A
alpha [in Oracle]B
B_user_w_nonneg_hyp [in Oracle]D
Delta_wd [in Oracle]Delta_dep [in Oracle]
H
h [in Oracle]L
L_f_nonneg_hyp [in Oracle]Q
q [in Oracle]U
Users [in Oracle]Users_NoDup [in Oracle]
Constructor Index
D
Deposit [in Oracle]N
NoneOp [in Oracle]R
Reading [in Oracle]RewardFunding [in Oracle]
S
Submission [in Oracle]V
VoteBlacklist [in Oracle]VoteWhitelist [in Oracle]
W
WeightSync [in Oracle]Withdrawal [in Oracle]
Inductive Index
O
Operation [in Oracle]Projection Index
B
B [in Oracle]B_oracle_r [in Oracle]
B_oracle_w [in Oracle]
B_user_r [in Oracle]
B_user_w [in Oracle]
G
G [in Oracle]L
L_tot [in Oracle]L_f [in Oracle]
L_l [in Oracle]
M
M_white [in Oracle]M_black [in Oracle]
P
pbar [in Oracle]Phist [in Oracle]
ptilde [in Oracle]
P_user [in Oracle]
Q
Q [in Oracle]T
t_last [in Oracle]t_sub [in Oracle]
T_user [in Oracle]
T_op [in Oracle]
T_dep [in Oracle]
V
V [in Oracle]V_white [in Oracle]
V_black [in Oracle]
W
W_user [in Oracle]W_white [in Oracle]
W_black [in Oracle]
Definition Index
A
addR [in Oracle]addR2 [in Oracle]
addUser [in Oracle]
B
balance [in Oracle]blacklist_vote [in Oracle]
D
decay [in Oracle]E
eq38_at [in Oracle]exec_prefix [in Oracle]
exec_trace [in Oracle]
exec_op [in Oracle]
G
getBool [in Oracle]getR [in Oracle]
getR2 [in Oracle]
getUserSet [in Oracle]
H
history [in Oracle]I
ideal_num_at_submission_time [in Oracle]ideal_Q_at_submission_time [in Oracle]
inactive_along_run [in Oracle]
init_state [in Oracle]
init_oracle [in Oracle]
init_governance [in Oracle]
init_B_oracle_r [in Oracle]
init_B_oracle_w [in Oracle]
init_B_user_r [in Oracle]
init_B_user_w [in Oracle]
isBlacklisted [in Oracle]
is_reward_funding [in Oracle]
is_submission [in Oracle]
is_submission_by [in Oracle]
L
Lambda [in Oracle]Lambda_run [in Oracle]
Lambda_x [in Oracle]
lift_oracle_state [in Oracle]
M
mean_eq_curr_pbar [in Oracle]mean_raw_eq [in Oracle]
mem_user [in Oracle]
O
Operation_sind [in Oracle]Operation_rec [in Oracle]
Operation_ind [in Oracle]
Operation_rect [in Oracle]
op_at [in Oracle]
P
pbar_decayed [in Oracle]pbar' [in Oracle]
pu [in Oracle]
P_ [in Oracle]
Q
Q_decayed [in Oracle]Q' [in Oracle]
R
reachable [in Oracle]Recompute [in Oracle]
reward_funding [in Oracle]
reward_payout [in Oracle]
Reweight [in Oracle]
reweight_white_step [in Oracle]
reweight_black_step [in Oracle]
Rgeb [in Oracle]
Rgtb [in Oracle]
Rleb [in Oracle]
Rltb [in Oracle]
Rpos [in Oracle]
Run [in Oracle]
S
setBool [in Oracle]setR [in Oracle]
setR2 [in Oracle]
setUserSet [in Oracle]
state_at [in Oracle]
submission_assumptions [in Oracle]
submission_assumptions_at [in Oracle]
submitted_oracle_state [in Oracle]
sum_list_R [in Oracle]
T
tends_to_0_seq [in Oracle]timestamp [in Oracle]
token_withdrawal [in Oracle]
token_deposit [in Oracle]
Trace [in Oracle]
tstar [in Oracle]
tu [in Oracle]
U
UMap_forall [in Oracle]Unlock [in Oracle]
UPairMap_forall [in Oracle]
User [in Oracle]
UserSet [in Oracle]
V
value [in Oracle]value_reading [in Oracle]
value_submission [in Oracle]
W
w [in Oracle]weight [in Oracle]
weight_synchronization [in Oracle]
whitelist_vote [in Oracle]
wu [in Oracle]
W_decayed [in Oracle]
Record Index
G
GovernanceState [in Oracle]O
OracleState [in Oracle]S
State [in Oracle]| 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 | (243 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 | (4 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 | (5 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 | (1 entry) |
| 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 | (94 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 | (9 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 | (9 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 | (1 entry) |
| 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 | (27 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 | (90 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) |
This page has been generated by coqdoc