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 | (845 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 | (26 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 | (11 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 | (11 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 | (14 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 | (218 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 | (72 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 | (1 entry) |
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 | (43 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 | (41 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 | (7 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 | (12 entries) |
Abbreviation 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) |
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 | (373 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 | (14 entries) |
Global Index
A
Acc [inductive, in PRFA.live_coding5]Acc_iff [lemma, in PRFA.live_coding5]
Acc_sind [definition, in PRFA.live_coding5]
Acc_rec [definition, in PRFA.live_coding5]
Acc_ind [definition, in PRFA.live_coding5]
Acc_rect [definition, in PRFA.live_coding5]
Acc_intro [constructor, in PRFA.live_coding5]
add [definition, in PRFA.tp2c]
add [definition, in PRFA.live_coding3]
add_from_nat [lemma, in PRFA.tp2c]
add_sub [lemma, in PRFA.review2]
Advanced [section, in PRFA.tp1c]
All [inductive, in PRFA.tp3c]
All_sind [definition, in PRFA.tp3c]
All_rec [definition, in PRFA.tp3c]
All_ind [definition, in PRFA.tp3c]
All_rect [definition, in PRFA.tp3c]
All_cons [constructor, in PRFA.tp3c]
All_nil [constructor, in PRFA.tp3c]
andb_orb_distr [lemma, in PRFA.tp1c]
andb_comm' [lemma, in PRFA.live_coding1]
andb_comm [lemma, in PRFA.live_coding1]
and_comm [lemma, in PRFA.tp1c]
and_assoc [lemma, in PRFA.tp4c]
and_com [lemma, in PRFA.tp4c]
and_AA [lemma, in PRFA.tp4c]
and_comm [lemma, in PRFA.live_coding1]
anything_goes [lemma, in PRFA.tp1c]
anything_goes [lemma, in PRFA.live_coding1]
app_assoc [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.live_coding2]
B
bad [inductive, in PRFA.live_coding3]bad [inductive, in PRFA.tp3c]
bad_not_bad [lemma, in PRFA.tp3c]
bad_rational2 [record, in PRFA.live_coding4]
bad_rational1 [record, in PRFA.live_coding4]
bar [definition, in PRFA.live_coding3]
baz [definition, in PRFA.live_coding3]
below [definition, in PRFA.tp3c]
bintree [inductive, in PRFA.live_coding5]
bintree_sind [definition, in PRFA.live_coding5]
bintree_rec [definition, in PRFA.live_coding5]
bintree_ind [definition, in PRFA.live_coding5]
bintree_rect [definition, in PRFA.live_coding5]
box [constructor, in PRFA.live_coding5]
Box [inductive, in PRFA.live_coding5]
Box_sind [definition, in PRFA.live_coding5]
Box_rec [definition, in PRFA.live_coding5]
Box_ind [definition, in PRFA.live_coding5]
Box_rect [definition, in PRFA.live_coding5]
brec [definition, in PRFA.tp3c]
brec' [definition, in PRFA.tp3c]
bt_to_tree [definition, in PRFA.live_coding5]
bt_map_id [lemma, in PRFA.live_coding5]
bt_map [definition, in PRFA.live_coding5]
bt_node [constructor, in PRFA.live_coding5]
bt_leaf [constructor, in PRFA.live_coding5]
C
C [constructor, in PRFA.live_coding3]C [constructor, in PRFA.tp3c]
calc_12_3 [lemma, in PRFA.tp1c]
calc_12_3 [lemma, in PRFA.live_coding1]
cancel_to_of [lemma, in PRFA.tp2c]
cancel_of_to [lemma, in PRFA.tp2c]
car [definition, in PRFA.tp2c]
car [definition, in PRFA.live_coding2]
car_cur [lemma, in PRFA.tp2c]
car_cur [lemma, in PRFA.live_coding2]
car' [definition, in PRFA.tp2c]
car'' [definition, in PRFA.tp2c]
classical_impl [lemma, in PRFA.tp1c]
classical_or_contra_r [lemma, in PRFA.tp1c]
contrad [lemma, in PRFA.tp1c]
contrapositive [lemma, in PRFA.tp1c]
count [definition, in PRFA.live_coding3]
count [definition, in PRFA.tp3c]
count_list [definition, in PRFA.live_coding3]
count_list [definition, in PRFA.tp3c]
cur [definition, in PRFA.tp2c]
cur [definition, in PRFA.live_coding2]
cur_car [lemma, in PRFA.tp2c]
cur_car [lemma, in PRFA.live_coding2]
D
define_nat.add_sub_alt [lemma, in PRFA.tp2c]define_nat.sub_O [lemma, in PRFA.tp2c]
define_nat.add_sub [lemma, in PRFA.tp2c]
_ - _ [notation, in PRFA.tp2c]
_ + _ [notation, in PRFA.tp2c]
define_nat.add_S [lemma, in PRFA.tp2c]
define_nat.add_0 [lemma, in PRFA.tp2c]
define_nat.sub [definition, in PRFA.tp2c]
define_nat.add [definition, in PRFA.tp2c]
define_nat.nat_sind [definition, in PRFA.tp2c]
define_nat.nat_rec [definition, in PRFA.tp2c]
define_nat.nat_ind [definition, in PRFA.tp2c]
define_nat.nat_rect [definition, in PRFA.tp2c]
define_nat.S [constructor, in PRFA.tp2c]
define_nat.O [constructor, in PRFA.tp2c]
define_nat.nat [inductive, in PRFA.tp2c]
define_nat [module, in PRFA.tp2c]
define_sigma.pair2 [definition, in PRFA.live_coding2]
define_sigma.pair1 [definition, in PRFA.live_coding2]
define_sigma.T [definition, in PRFA.live_coding2]
define_sigma.sigT_sind [definition, in PRFA.live_coding2]
define_sigma.sigT_rec [definition, in PRFA.live_coding2]
define_sigma.sigT_ind [definition, in PRFA.live_coding2]
define_sigma.sigT_rect [definition, in PRFA.live_coding2]
define_sigma.existT [constructor, in PRFA.live_coding2]
define_sigma.sigT [inductive, in PRFA.live_coding2]
define_sigma [module, in PRFA.live_coding2]
define_list.list_sind [definition, in PRFA.live_coding2]
define_list.list_rec [definition, in PRFA.live_coding2]
define_list.list_ind [definition, in PRFA.live_coding2]
define_list.list_rect [definition, in PRFA.live_coding2]
define_list.cons [constructor, in PRFA.live_coding2]
define_list.nil [constructor, in PRFA.live_coding2]
define_list.list [inductive, in PRFA.live_coding2]
define_list [module, in PRFA.live_coding2]
define_prod.snd [definition, in PRFA.live_coding2]
define_prod.fst [definition, in PRFA.live_coding2]
define_prod.pair' [definition, in PRFA.live_coding2]
define_prod.prod_sind [definition, in PRFA.live_coding2]
define_prod.prod_rec [definition, in PRFA.live_coding2]
define_prod.prod_ind [definition, in PRFA.live_coding2]
define_prod.prod_rect [definition, in PRFA.live_coding2]
define_prod.pair [constructor, in PRFA.live_coding2]
define_prod.prod [inductive, in PRFA.live_coding2]
define_prod [module, in PRFA.live_coding2]
define_bool.true_false [lemma, in PRFA.live_coding2]
define_bool.bool_sind [definition, in PRFA.live_coding2]
define_bool.bool_rec [definition, in PRFA.live_coding2]
define_bool.bool_ind [definition, in PRFA.live_coding2]
define_bool.bool_rect [definition, in PRFA.live_coding2]
define_bool.false [constructor, in PRFA.live_coding2]
define_bool.true [constructor, in PRFA.live_coding2]
define_bool.bool [inductive, in PRFA.live_coding2]
define_bool [module, in PRFA.live_coding2]
define_nat.eq_nat_spec [lemma, in PRFA.live_coding2]
define_nat.eq_nat_spec [lemma, in PRFA.live_coding2]
define_nat.eq_nat [definition, in PRFA.live_coding2]
define_nat.S_inj_4 [lemma, in PRFA.live_coding2]
define_nat.S_inj_3 [lemma, in PRFA.live_coding2]
define_nat.S_inj_2 [lemma, in PRFA.live_coding2]
define_nat.S_inj [lemma, in PRFA.live_coding2]
define_nat.pred [definition, in PRFA.live_coding2]
define_nat.S_0' [lemma, in PRFA.live_coding2]
define_nat.S_O [lemma, in PRFA.live_coding2]
define_nat.is_zero [definition, in PRFA.live_coding2]
define_nat.is_zerob [definition, in PRFA.live_coding2]
define_nat.add_sub [lemma, in PRFA.live_coding2]
_ - _ [notation, in PRFA.live_coding2]
define_nat.sub [definition, in PRFA.live_coding2]
define_nat.add_S [lemma, in PRFA.live_coding2]
_ + _ [notation, in PRFA.live_coding2]
define_nat.add_0 [lemma, in PRFA.live_coding2]
define_nat.add [definition, in PRFA.live_coding2]
define_nat.variant2.nat_sind [definition, in PRFA.live_coding2]
define_nat.variant2.nat_rec [definition, in PRFA.live_coding2]
define_nat.variant2.nat_ind [definition, in PRFA.live_coding2]
define_nat.variant2.nat_rect [definition, in PRFA.live_coding2]
define_nat.variant2.S [constructor, in PRFA.live_coding2]
define_nat.variant2.O [constructor, in PRFA.live_coding2]
define_nat.variant2.nat [inductive, in PRFA.live_coding2]
define_nat.variant2 [module, in PRFA.live_coding2]
define_nat.variant1.nat_sind [definition, in PRFA.live_coding2]
define_nat.variant1.nat_rec [definition, in PRFA.live_coding2]
define_nat.variant1.nat_ind [definition, in PRFA.live_coding2]
define_nat.variant1.nat_rect [definition, in PRFA.live_coding2]
define_nat.variant1.S [constructor, in PRFA.live_coding2]
define_nat.variant1.O [constructor, in PRFA.live_coding2]
define_nat.variant1.nat [inductive, in PRFA.live_coding2]
define_nat.variant1 [module, in PRFA.live_coding2]
define_nat.nat_sind [definition, in PRFA.live_coding2]
define_nat.nat_rec [definition, in PRFA.live_coding2]
define_nat.nat_ind [definition, in PRFA.live_coding2]
define_nat.nat_rect [definition, in PRFA.live_coding2]
define_nat.S [constructor, in PRFA.live_coding2]
define_nat.O [constructor, in PRFA.live_coding2]
define_nat.nat [inductive, in PRFA.live_coding2]
define_nat [module, in PRFA.live_coding2]
Demo [section, in PRFA.live_coding3]
Demo.X [variable, in PRFA.live_coding3]
Demo.Y [variable, in PRFA.live_coding3]
Demo.Z [variable, in PRFA.live_coding3]
denominator [projection, in PRFA.live_coding4]
denominator' [projection, in PRFA.live_coding4]
denominator'' [projection, in PRFA.live_coding4]
den_not_zero [projection, in PRFA.live_coding4]
dependent [definition, in PRFA.live_coding3]
de_morgan [lemma, in PRFA.tp1c]
distr [lemma, in PRFA.tp1c]
DNE [axiom, in PRFA.live_coding4]
DNS [definition, in PRFA.tp1c]
dns_lem [lemma, in PRFA.tp1c]
dn_functorial [lemma, in PRFA.tp1c]
double [definition, in PRFA.live_coding1]
double_S [definition, in PRFA.live_coding6]
double_eq [lemma, in PRFA.tp1c]
double_eq2 [lemma, in PRFA.live_coding1]
double_eq [lemma, in PRFA.live_coding1]
E
elim_or [definition, in PRFA.live_coding3]elim_and [definition, in PRFA.live_coding3]
elim_False [definition, in PRFA.live_coding3]
empty_tree [definition, in PRFA.live_coding3]
Eq [record, in PRFA.tp4c]
Eq [record, in PRFA.live_coding4]
eqb [projection, in PRFA.tp4c]
eqb [projection, in PRFA.live_coding4]
eqb_iff [projection, in PRFA.tp4c]
eqb_iff [projection, in PRFA.live_coding4]
eq_nat_spec [lemma, in PRFA.tp2c]
eq_nat [definition, in PRFA.tp2c]
Eq_nat [instance, in PRFA.tp4c]
Eq_nat [instance, in PRFA.live_coding4]
eq_nat_spec [lemma, in PRFA.review2]
eq_nat [definition, in PRFA.review2]
even [inductive, in PRFA.review3]
even [inductive, in PRFA.live_coding2]
even [inductive, in PRFA.live_coding3]
evenb [definition, in PRFA.live_coding2]
evenb_to_even [lemma, in PRFA.live_coding2]
evenb_to_even [lemma, in PRFA.live_coding2]
evenO [constructor, in PRFA.review3]
evenO [constructor, in PRFA.tp2c]
evenO [constructor, in PRFA.live_coding2]
evenO [constructor, in PRFA.live_coding3]
evenS [constructor, in PRFA.review3]
evenS [constructor, in PRFA.tp2c]
evenS [constructor, in PRFA.live_coding2]
evenS [constructor, in PRFA.live_coding3]
even_sind [definition, in PRFA.review3]
even_ind [definition, in PRFA.review3]
even_to_evenb [lemma, in PRFA.live_coding2]
even_sind [definition, in PRFA.live_coding2]
even_ind [definition, in PRFA.live_coding2]
even_plus_four_term [definition, in PRFA.live_coding3]
even_plus_four_refine [lemma, in PRFA.live_coding3]
even_plus_four [lemma, in PRFA.live_coding3]
even_four' [definition, in PRFA.live_coding3]
even_four [lemma, in PRFA.live_coding3]
even_sind [definition, in PRFA.live_coding3]
even_ind [definition, in PRFA.live_coding3]
even1 [definition, in PRFA.tp2c]
even1_to_even2 [lemma, in PRFA.tp2c]
even2 [definition, in PRFA.tp2c]
even2 [definition, in PRFA.review2]
even2_iff_even3 [lemma, in PRFA.tp2c]
even2_iff_even3 [lemma, in PRFA.review2]
even3 [definition, in PRFA.tp2c]
even3 [definition, in PRFA.review2]
even3_to_even4 [lemma, in PRFA.tp2c]
even4 [inductive, in PRFA.tp2c]
even4_to_even1 [lemma, in PRFA.tp2c]
even4_sind [definition, in PRFA.tp2c]
even4_ind [definition, in PRFA.tp2c]
exercise_chain [lemma, in PRFA.live_coding5]
exercise_loop [lemma, in PRFA.live_coding5]
exfalso' [definition, in PRFA.live_coding5]
exp [definition, in PRFA.tp2c]
exp_from_nat [lemma, in PRFA.tp2c]
ex1 [definition, in PRFA.tp3c]
ex2 [definition, in PRFA.tp3c]
ex3 [definition, in PRFA.tp3c]
ex3_alt [definition, in PRFA.tp3c]
ex4 [definition, in PRFA.tp3c]
F
f [definition, in PRFA.live_coding3]f [definition, in PRFA.tp3c]
fact_equiv [lemma, in PRFA.tp2c]
fact_iter [definition, in PRFA.tp2c]
fact_iter_f [definition, in PRFA.tp2c]
fact_fix [definition, in PRFA.tp2c]
falsefalse [lemma, in PRFA.live_coding1]
False_forall [lemma, in PRFA.tp1c]
fast_rev_eq_alt [lemma, in PRFA.tp2c]
fast_rev_eq [lemma, in PRFA.tp2c]
fast_rev [definition, in PRFA.tp2c]
fast_rev_eq_alt [lemma, in PRFA.live_coding2]
fast_rev_eq [lemma, in PRFA.live_coding2]
fast_rev_eq [lemma, in PRFA.live_coding2]
fast_rev [definition, in PRFA.live_coding2]
fib [definition, in PRFA.tp3c]
Fib_Iter.fib_eq3 [lemma, in PRFA.tp2c]
Fib_Iter.fib_eq1 [lemma, in PRFA.tp2c]
Fib_Iter.fib_eq0 [lemma, in PRFA.tp2c]
Fib_Iter.fib [definition, in PRFA.tp2c]
Fib_Iter.sigma [definition, in PRFA.tp2c]
Fib_Iter [module, in PRFA.tp2c]
fib_brec [definition, in PRFA.tp3c]
fib_natrec [definition, in PRFA.tp3c]
fold_def [definition, in PRFA.MetaCoqPrelude]
fold_branches [definition, in PRFA.MetaCoqPrelude]
fold_branch [definition, in PRFA.MetaCoqPrelude]
fold_predicate [definition, in PRFA.MetaCoqPrelude]
fold_handler [definition, in PRFA.MetaCoqPrelude]
foo [definition, in PRFA.tp4c]
foo [definition, in PRFA.live_coding3]
foo [definition, in PRFA.live_coding4]
forall_or [lemma, in PRFA.tp1c]
forall_False' [lemma, in PRFA.tp1c]
forall_False [lemma, in PRFA.tp1c]
Forall_set_eq [lemma, in PRFA.tp4c]
Forall_In [lemma, in PRFA.tp4c]
from_nat [definition, in PRFA.tp2c]
from_to_tree_alt [lemma, in PRFA.tp3c]
from_to_tree_list [definition, in PRFA.tp3c]
from_to_tree [definition, in PRFA.tp3c]
from_tree_list [definition, in PRFA.tp3c]
from_tree [definition, in PRFA.tp3c]
fst' [projection, in PRFA.review4]
fst' [projection, in PRFA.tp4c]
fst' [projection, in PRFA.live_coding4]
G
G [inductive, in PRFA.live_coding5]get_kername [definition, in PRFA.MetaCoqPrelude]
GI [constructor, in PRFA.live_coding5]
good_tree_ind [lemma, in PRFA.live_coding5]
good_tree_ind' [lemma, in PRFA.live_coding5]
Group [record, in PRFA.tp4c]
group [record, in PRFA.tp4c]
Group_Z [instance, in PRFA.tp4c]
group_inverse_unique [lemma, in PRFA.tp4c]
group_neutral_unique [lemma, in PRFA.tp4c]
group_inv [projection, in PRFA.tp4c]
group_assoc [projection, in PRFA.tp4c]
group_right_neutral [projection, in PRFA.tp4c]
group_left_neutral [projection, in PRFA.tp4c]
group_fact [lemma, in PRFA.tp4c]
g_inv [projection, in PRFA.tp4c]
g_mon [projection, in PRFA.tp4c]
G_zero [lemma, in PRFA.live_coding5]
G_sig [lemma, in PRFA.live_coding5]
G_sind [definition, in PRFA.live_coding5]
G_rec [definition, in PRFA.live_coding5]
G_ind [definition, in PRFA.live_coding5]
G_rect [definition, in PRFA.live_coding5]
H
half [definition, in PRFA.live_coding4]half' [definition, in PRFA.live_coding4]
Hierarchy [module, in PRFA.tp3c]
Hierarchy.embeds [definition, in PRFA.tp3c]
Hierarchy.embeds_refl [lemma, in PRFA.tp3c]
Hierarchy.hier [lemma, in PRFA.tp3c]
Hierarchy.hierarchy [lemma, in PRFA.tp3c]
Hierarchy.inconsistent [lemma, in PRFA.tp3c]
Hierarchy.sub [definition, in PRFA.tp3c]
Hierarchy.sub_irrefl [lemma, in PRFA.tp3c]
Hierarchy.T [constructor, in PRFA.tp3c]
Hierarchy.tree [inductive, in PRFA.tp3c]
Hierarchy.tree_sind [definition, in PRFA.tp3c]
Hierarchy.tree_rec [definition, in PRFA.tp3c]
Hierarchy.tree_ind [definition, in PRFA.tp3c]
Hierarchy.tree_rect [definition, in PRFA.tp3c]
Hierarchy.Tyi [definition, in PRFA.tp3c]
I
iAnd [definition, in PRFA.review3]iAnd [definition, in PRFA.tp3c]
iAnd_and [lemma, in PRFA.review3]
iAnd_iff [lemma, in PRFA.tp3c]
idNat [definition, in PRFA.live_coding6]
idnat [definition, in PRFA.tp3c]
iEx [definition, in PRFA.review3]
iEx [definition, in PRFA.tp3c]
iEx_ex [lemma, in PRFA.review3]
iEx_iff [lemma, in PRFA.tp3c]
iFalse [definition, in PRFA.review3]
iFalse [definition, in PRFA.tp3c]
iFalse_iff [lemma, in PRFA.tp3c]
imp_trans [lemma, in PRFA.tp1c]
In [definition, in PRFA.tp2c]
incl [constructor, in PRFA.tp2c]
incl [constructor, in PRFA.live_coding2]
in_cons [lemma, in PRFA.review4]
in_add_left [lemma, in PRFA.review4]
in_add_right [lemma, in PRFA.review4]
In_iff [lemma, in PRFA.tp2c]
In_i_sind [definition, in PRFA.tp2c]
In_i_ind [definition, in PRFA.tp2c]
in_tl [constructor, in PRFA.tp2c]
in_hd [constructor, in PRFA.tp2c]
In_i [inductive, in PRFA.tp2c]
In_app_inv [lemma, in PRFA.tp4c]
In_hd_eq [lemma, in PRFA.tp4c]
In_app_r [lemma, in PRFA.tp4c]
In_app_l [lemma, in PRFA.tp4c]
In_hd' [lemma, in PRFA.tp4c]
In_4 [lemma, in PRFA.tp4c]
In_tl [lemma, in PRFA.tp4c]
In_hd [lemma, in PRFA.tp4c]
In_hd' [lemma, in PRFA.live_coding4]
In_4 [lemma, in PRFA.live_coding4]
In_tl [lemma, in PRFA.live_coding4]
In_hd [lemma, in PRFA.live_coding4]
iOr [definition, in PRFA.tp3c]
iOr_iff [lemma, in PRFA.tp3c]
iter [definition, in PRFA.tp2c]
iter [definition, in PRFA.live_coding2]
iter_shift [lemma, in PRFA.tp2c]
iter_pow [lemma, in PRFA.tp2c]
iter_mul [lemma, in PRFA.live_coding2]
iter_add [lemma, in PRFA.live_coding2]
iTrue [definition, in PRFA.tp3c]
iTrue_iff [lemma, in PRFA.tp3c]
L
le [inductive, in PRFA.live_coding2]least [definition, in PRFA.live_coding5]
leb [definition, in PRFA.tp2c]
leb_spec_alt [lemma, in PRFA.tp2c]
leb_spec [lemma, in PRFA.tp2c]
LEM [definition, in PRFA.tp1c]
lem_dns [lemma, in PRFA.tp1c]
lem_pl [lemma, in PRFA.tp1c]
leO [constructor, in PRFA.live_coding2]
leO' [constructor, in PRFA.tp2c]
leS [constructor, in PRFA.live_coding2]
leS' [constructor, in PRFA.tp2c]
le_n_S [lemma, in PRFA.review3]
le_equiv [lemma, in PRFA.tp2c]
le_n_S [lemma, in PRFA.tp2c]
le_0_n [lemma, in PRFA.tp2c]
le_rtclos [lemma, in PRFA.live_coding2]
le_trans [lemma, in PRFA.live_coding2]
le_iff [lemma, in PRFA.live_coding2]
le_sind [definition, in PRFA.live_coding2]
le_ind [definition, in PRFA.live_coding2]
le' [inductive, in PRFA.tp2c]
le'_n_S [lemma, in PRFA.tp2c]
le'_refl [lemma, in PRFA.tp2c]
le'_sind [definition, in PRFA.tp2c]
le'_ind [definition, in PRFA.tp2c]
linear_search [lemma, in PRFA.live_coding5]
list_seq_eq_app [lemma, in PRFA.tp4c]
list_set_eq_trans [instance, in PRFA.tp4c]
list_set_eq_sym [instance, in PRFA.tp4c]
list_set_eq_refl [instance, in PRFA.tp4c]
list_set_eq [definition, in PRFA.tp4c]
list_fact [lemma, in PRFA.tp4c]
list_monoid [definition, in PRFA.tp4c]
list_rect [definition, in PRFA.live_coding3]
Live [section, in PRFA.live_coding1]
live_coding6 [library]
live_coding5 [library]
live_coding2 [library]
live_coding1 [library]
live_coding4 [library]
live_coding3 [library]
lt [inductive, in PRFA.review3]
lt [inductive, in PRFA.tp3c]
lt_plus_4' [definition, in PRFA.review3]
lt_plus_4 [definition, in PRFA.review3]
lt_sind [definition, in PRFA.review3]
lt_ind [definition, in PRFA.review3]
lt_S [constructor, in PRFA.review3]
lt_B [constructor, in PRFA.review3]
lt_plus_4' [definition, in PRFA.tp3c]
lt_plus_4 [lemma, in PRFA.tp3c]
lt_sind [definition, in PRFA.tp3c]
lt_ind [definition, in PRFA.tp3c]
lt_S [constructor, in PRFA.tp3c]
lt_B [constructor, in PRFA.tp3c]
M
memb [definition, in PRFA.tp4c]memb [definition, in PRFA.live_coding4]
memb_spec [lemma, in PRFA.tp4c]
MetaCoqPrelude [library]
min [definition, in PRFA.tp1c]
min_comm [lemma, in PRFA.tp1c]
Monoid [record, in PRFA.tp4c]
monoid [record, in PRFA.tp4c]
Monoid [record, in PRFA.live_coding4]
monoid [record, in PRFA.live_coding4]
MonoidList [instance, in PRFA.tp4c]
MonoidNat [instance, in PRFA.tp4c]
MonoidNat [instance, in PRFA.live_coding4]
MonoidProd [instance, in PRFA.tp4c]
MonoidProd [instance, in PRFA.live_coding4]
Monoid_Group [instance, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.live_coding4]
mon_assoc [projection, in PRFA.tp4c]
mon_right_neutral [projection, in PRFA.tp4c]
mon_left_neutral [projection, in PRFA.tp4c]
mon_assoc [projection, in PRFA.live_coding4]
mon_right_neutral [projection, in PRFA.live_coding4]
mon_left_neutral [projection, in PRFA.live_coding4]
mpow [definition, in PRFA.live_coding6]
mpow' [definition, in PRFA.live_coding6]
mul [definition, in PRFA.tp2c]
mult_distr_lia [lemma, in PRFA.tp1c]
mult_distr [lemma, in PRFA.tp1c]
mult_comm [lemma, in PRFA.tp1c]
mult_S [lemma, in PRFA.tp1c]
mult_0 [lemma, in PRFA.tp1c]
mult4 [inductive, in PRFA.live_coding6]
mult4_sind [definition, in PRFA.live_coding6]
mult4_ind [definition, in PRFA.live_coding6]
mult4_plus [constructor, in PRFA.live_coding6]
mult4_0 [constructor, in PRFA.live_coding6]
mul_from_nat [lemma, in PRFA.tp2c]
m_assoc [projection, in PRFA.tp4c]
m_r_ne [projection, in PRFA.tp4c]
m_l_ne [projection, in PRFA.tp4c]
m_op [projection, in PRFA.tp4c]
m_ne [projection, in PRFA.tp4c]
m_ty [projection, in PRFA.tp4c]
m_assoc [projection, in PRFA.live_coding4]
m_r_ne [projection, in PRFA.live_coding4]
m_l_ne [projection, in PRFA.live_coding4]
m_op [projection, in PRFA.live_coding4]
m_ne [projection, in PRFA.live_coding4]
m_ty [projection, in PRFA.live_coding4]
N
N [constructor, in PRFA.live_coding3]N [constructor, in PRFA.tp3c]
nat_fact [lemma, in PRFA.tp4c]
nat_monoid [definition, in PRFA.tp4c]
nat_rect [definition, in PRFA.live_coding3]
nat_nat_fact [lemma, in PRFA.live_coding4]
nat_nat_fact [lemma, in PRFA.live_coding4]
nat_fact [lemma, in PRFA.live_coding4]
nat_monoid [definition, in PRFA.live_coding4]
ncons [constructor, in PRFA.live_coding3]
ncons [constructor, in PRFA.tp3c]
negb_invol [lemma, in PRFA.live_coding1]
negb_true [lemma, in PRFA.live_coding1]
nforest [inductive, in PRFA.live_coding3]
nforest [inductive, in PRFA.tp3c]
nforest_sind [definition, in PRFA.live_coding3]
nforest_rec [definition, in PRFA.live_coding3]
nforest_ind [definition, in PRFA.live_coding3]
nforest_rect [definition, in PRFA.live_coding3]
nforest_ntree_rec [definition, in PRFA.tp3c]
nforest_map [definition, in PRFA.tp3c]
nforest_sind [definition, in PRFA.tp3c]
nforest_rec [definition, in PRFA.tp3c]
nforest_ind [definition, in PRFA.tp3c]
nforest_rect [definition, in PRFA.tp3c]
nnil [constructor, in PRFA.live_coding3]
nnil [constructor, in PRFA.tp3c]
nnode [constructor, in PRFA.live_coding3]
nnode [constructor, in PRFA.tp3c]
node [constructor, in PRFA.live_coding5]
nofalse [lemma, in PRFA.tp1c]
nofalse [lemma, in PRFA.live_coding1]
not_mult4_sind [definition, in PRFA.live_coding6]
not_mult4_ind [definition, in PRFA.live_coding6]
not_mult4_plus [constructor, in PRFA.live_coding6]
not_mult4_3 [constructor, in PRFA.live_coding6]
not_mult4_2 [constructor, in PRFA.live_coding6]
not_mult4_1 [constructor, in PRFA.live_coding6]
not_mult4 [inductive, in PRFA.live_coding6]
ntree [inductive, in PRFA.live_coding3]
ntree [inductive, in PRFA.tp3c]
ntree_sind [definition, in PRFA.live_coding3]
ntree_rec [definition, in PRFA.live_coding3]
ntree_ind [definition, in PRFA.live_coding3]
ntree_rect [definition, in PRFA.live_coding3]
ntree_nforest_rec [definition, in PRFA.tp3c]
ntree_map [definition, in PRFA.tp3c]
ntree_sind [definition, in PRFA.tp3c]
ntree_rec [definition, in PRFA.tp3c]
ntree_ind [definition, in PRFA.tp3c]
ntree_rect [definition, in PRFA.tp3c]
num [definition, in PRFA.tp2c]
numerator [projection, in PRFA.live_coding4]
numerator' [projection, in PRFA.live_coding4]
numerator'' [projection, in PRFA.live_coding4]
Nx [constructor, in PRFA.tp3c]
n_plus_0 [lemma, in PRFA.tp1c]
O
of_nat_inj [lemma, in PRFA.tp2c]of_nat [definition, in PRFA.tp2c]
one_zero_Z [lemma, in PRFA.tp4c]
or_imp [definition, in PRFA.review3]
or_imp [lemma, in PRFA.tp1c]
or_comm [lemma, in PRFA.tp1c]
or_com [lemma, in PRFA.tp4c]
or_AA [lemma, in PRFA.tp4c]
or_comm [definition, in PRFA.tp3c]
or_comm [lemma, in PRFA.live_coding1]
P
pfalse [constructor, in PRFA.live_coding5]PI [definition, in PRFA.live_coding5]
PL [definition, in PRFA.tp1c]
plus_assoc [lemma, in PRFA.tp1c]
plus_comm [lemma, in PRFA.tp1c]
plus_S [lemma, in PRFA.tp1c]
pl_lem [lemma, in PRFA.tp1c]
pneg [definition, in PRFA.live_coding5]
pneg_invol [lemma, in PRFA.live_coding5]
pow13 [definition, in PRFA.live_coding6]
pow3 [definition, in PRFA.live_coding6]
pow5 [definition, in PRFA.live_coding6]
pred [definition, in PRFA.tp2c]
pred_from_nat [lemma, in PRFA.tp2c]
pred' [definition, in PRFA.tp2c]
pred'_from_nat [lemma, in PRFA.tp2c]
prod_monoid [definition, in PRFA.tp4c]
prod_monoid [definition, in PRFA.live_coding4]
prod' [record, in PRFA.review4]
prod' [record, in PRFA.tp4c]
prod' [record, in PRFA.live_coding4]
prod'_ind [definition, in PRFA.review4]
prop_bool_sind [definition, in PRFA.live_coding5]
prop_bool_ind [definition, in PRFA.live_coding5]
prop_bool [inductive, in PRFA.live_coding5]
ptrue [constructor, in PRFA.live_coding5]
P_iff_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.live_coding1]
Q
quarter [definition, in PRFA.live_coding4]quarter'' [definition, in PRFA.live_coding4]
R
rational [record, in PRFA.live_coding4]refl [constructor, in PRFA.tp2c]
refl [constructor, in PRFA.live_coding2]
refl' [constructor, in PRFA.tp2c]
REPLACE_ME [definition, in PRFA.tp1c]
review2 [library]
review3 [library]
review4 [library]
rev_rev [lemma, in PRFA.tp2c]
rev_app_distr [lemma, in PRFA.tp2c]
rev_rev [lemma, in PRFA.live_coding2]
rev_app_distr [lemma, in PRFA.live_coding2]
rtclos [inductive, in PRFA.tp2c]
rtclos [inductive, in PRFA.live_coding2]
rtclos_iff [lemma, in PRFA.tp2c]
rtclos_sind [definition, in PRFA.tp2c]
rtclos_ind [definition, in PRFA.tp2c]
rtclos_sind [definition, in PRFA.live_coding2]
rtclos_ind [definition, in PRFA.live_coding2]
rtclos' [inductive, in PRFA.tp2c]
rtclos'_trans [lemma, in PRFA.tp2c]
rtclos'_sind [definition, in PRFA.tp2c]
rtclos'_ind [definition, in PRFA.tp2c]
Russel [definition, in PRFA.review3]
Russel [definition, in PRFA.review3]
Russel [lemma, in PRFA.tp1c]
Russel [definition, in PRFA.tp3c]
Russell [lemma, in PRFA.live_coding3]
S
Show_Definitions.or_sind [definition, in PRFA.live_coding3]Show_Definitions.or_ind [definition, in PRFA.live_coding3]
Show_Definitions.or_intror [constructor, in PRFA.live_coding3]
Show_Definitions.or_introl [constructor, in PRFA.live_coding3]
Show_Definitions.or [inductive, in PRFA.live_coding3]
Show_Definitions.and_sind [definition, in PRFA.live_coding3]
Show_Definitions.and_rec [definition, in PRFA.live_coding3]
Show_Definitions.and_ind [definition, in PRFA.live_coding3]
Show_Definitions.and_rect [definition, in PRFA.live_coding3]
Show_Definitions.conj [constructor, in PRFA.live_coding3]
Show_Definitions.and [inductive, in PRFA.live_coding3]
~ _ [notation, in PRFA.live_coding3]
Show_Definitions.True_sind [definition, in PRFA.live_coding3]
Show_Definitions.True_rec [definition, in PRFA.live_coding3]
Show_Definitions.True_ind [definition, in PRFA.live_coding3]
Show_Definitions.True_rect [definition, in PRFA.live_coding3]
Show_Definitions.I [constructor, in PRFA.live_coding3]
Show_Definitions.True [inductive, in PRFA.live_coding3]
Show_Definitions.False_sind [definition, in PRFA.live_coding3]
Show_Definitions.False_rec [definition, in PRFA.live_coding3]
Show_Definitions.False_ind [definition, in PRFA.live_coding3]
Show_Definitions.False_rect [definition, in PRFA.live_coding3]
Show_Definitions.False [inductive, in PRFA.live_coding3]
Show_Definitions [module, in PRFA.live_coding3]
size_recursion [lemma, in PRFA.live_coding5]
snd' [projection, in PRFA.review4]
snd' [projection, in PRFA.tp4c]
snd' [projection, in PRFA.live_coding4]
some_other_pair [definition, in PRFA.tp4c]
some_pair [definition, in PRFA.tp4c]
some_tree [definition, in PRFA.live_coding3]
some_other_pair [definition, in PRFA.live_coding4]
some_pair [definition, in PRFA.live_coding4]
strong_nat_ind [lemma, in PRFA.tp2c]
strong_nat_ind [lemma, in PRFA.live_coding2]
strong_nat_ind [lemma, in PRFA.review2]
succ [definition, in PRFA.tp2c]
swap [definition, in PRFA.tp2c]
swap_invol [lemma, in PRFA.tp2c]
S_neq [lemma, in PRFA.tp3c]
T
T [definition, in PRFA.live_coding3]term_eqb [definition, in PRFA.MetaCoqPrelude]
test [lemma, in PRFA.live_coding6]
test_list [lemma, in PRFA.tp4c]
test_nat' [lemma, in PRFA.tp4c]
test_monoid [lemma, in PRFA.tp4c]
test_nat [lemma, in PRFA.tp4c]
test_nat' [lemma, in PRFA.live_coding4]
test_monoid [lemma, in PRFA.live_coding4]
test_nat [lemma, in PRFA.live_coding4]
theDNS [definition, in PRFA.tp1c]
theLEM [definition, in PRFA.tp1c]
thePL [definition, in PRFA.tp1c]
tLam [abbreviation, in PRFA.MetaCoqPrelude]
tLet [abbreviation, in PRFA.MetaCoqPrelude]
tm_fold [definition, in PRFA.MetaCoqPrelude]
tm_nb_handler [definition, in PRFA.MetaCoqPrelude]
tm_handler [definition, in PRFA.MetaCoqPrelude]
tNat [definition, in PRFA.live_coding6]
to_nat_inj [lemma, in PRFA.tp2c]
to_nat [definition, in PRFA.tp2c]
to_nat' [definition, in PRFA.tp2c]
to_not_not [lemma, in PRFA.tp1c]
to_prod_eq [lemma, in PRFA.tp4c]
to_prod_alt3 [definition, in PRFA.tp4c]
to_prod_alt2 [definition, in PRFA.tp4c]
to_prod_alt [definition, in PRFA.tp4c]
to_prod [definition, in PRFA.tp4c]
to_tree_map [lemma, in PRFA.live_coding5]
to_bool_function_not_PI [lemma, in PRFA.live_coding5]
to_bool [lemma, in PRFA.live_coding5]
to_bool [lemma, in PRFA.live_coding5]
to_bool [definition, in PRFA.live_coding5]
to_prop_bool [definition, in PRFA.live_coding5]
to_from_tree [lemma, in PRFA.tp3c]
to_tree_list [definition, in PRFA.tp3c]
to_tree [definition, in PRFA.tp3c]
to_prod_alt3 [definition, in PRFA.live_coding4]
to_prod_alt2 [definition, in PRFA.live_coding4]
to_prod_alt [definition, in PRFA.live_coding4]
to_prod [definition, in PRFA.live_coding4]
TP1 [section, in PRFA.tp1c]
tp1c [library]
tp2c [library]
tp3c [library]
tp4c [library]
trans [constructor, in PRFA.tp2c]
trans [constructor, in PRFA.live_coding2]
transform [definition, in PRFA.MetaCoqPrelude]
transform_nb [definition, in PRFA.MetaCoqPrelude]
trans' [constructor, in PRFA.tp2c]
tree [inductive, in PRFA.live_coding5]
tree [inductive, in PRFA.live_coding3]
tree [inductive, in PRFA.tp3c]
tree_map_id_again' [lemma, in PRFA.live_coding5]
tree_map_id_again [lemma, in PRFA.live_coding5]
tree_map_id [definition, in PRFA.live_coding5]
tree_map_id [lemma, in PRFA.live_coding5]
tree_map [definition, in PRFA.live_coding5]
tree_sind [definition, in PRFA.live_coding5]
tree_rec [definition, in PRFA.live_coding5]
tree_ind [definition, in PRFA.live_coding5]
tree_rect [definition, in PRFA.live_coding5]
tree_sind [definition, in PRFA.live_coding3]
tree_rec [definition, in PRFA.live_coding3]
tree_ind [definition, in PRFA.live_coding3]
tree_rect [definition, in PRFA.live_coding3]
tree_rect_strong [definition, in PRFA.tp3c]
tree_sind [definition, in PRFA.tp3c]
tree_rec [definition, in PRFA.tp3c]
tree_ind [definition, in PRFA.tp3c]
tree_rect [definition, in PRFA.tp3c]
truetrue [lemma, in PRFA.tp1c]
truetrue [lemma, in PRFA.live_coding1]
true_false [lemma, in PRFA.review3]
true_false [lemma, in PRFA.tp2c]
twice [lemma, in PRFA.tp1c]
U
unfold_toplevel [definition, in PRFA.MetaCoqPrelude]Universes [section, in PRFA.live_coding5]
Universes.A [variable, in PRFA.live_coding5]
Universes.B [variable, in PRFA.live_coding5]
Universes.C [variable, in PRFA.live_coding5]
Universes.P [variable, in PRFA.live_coding5]
Universes.Q [variable, in PRFA.live_coding5]
Unnamed_thm2 [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.live_coding6]
Unnamed_thm0 [definition, in PRFA.live_coding6]
Unnamed_thm [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.review4]
Unnamed_thm0 [definition, in PRFA.review4]
Unnamed_thm [definition, in PRFA.review4]
Unnamed_thm18 [definition, in PRFA.tp4c]
Unnamed_thm17 [definition, in PRFA.tp4c]
Unnamed_thm16 [definition, in PRFA.tp4c]
Unnamed_thm15 [definition, in PRFA.tp4c]
Unnamed_thm14 [definition, in PRFA.tp4c]
Unnamed_thm13 [definition, in PRFA.tp4c]
Unnamed_thm12 [definition, in PRFA.tp4c]
Unnamed_thm11 [definition, in PRFA.tp4c]
Unnamed_thm10 [definition, in PRFA.tp4c]
Unnamed_thm9 [definition, in PRFA.tp4c]
Unnamed_thm8 [definition, in PRFA.tp4c]
Unnamed_thm7 [definition, in PRFA.tp4c]
Unnamed_thm6 [definition, in PRFA.tp4c]
Unnamed_thm5 [definition, in PRFA.tp4c]
Unnamed_thm4 [definition, in PRFA.tp4c]
Unnamed_thm3 [definition, in PRFA.tp4c]
Unnamed_thm2 [definition, in PRFA.tp4c]
Unnamed_thm1 [definition, in PRFA.tp4c]
Unnamed_thm0 [definition, in PRFA.tp4c]
Unnamed_thm [definition, in PRFA.tp4c]
Unnamed_thm4 [definition, in PRFA.live_coding2]
Unnamed_thm3 [definition, in PRFA.live_coding2]
Unnamed_thm2 [definition, in PRFA.live_coding2]
Unnamed_thm1 [definition, in PRFA.live_coding2]
Unnamed_thm1 [definition, in PRFA.live_coding2]
Unnamed_thm0 [definition, in PRFA.live_coding2]
Unnamed_thm [definition, in PRFA.live_coding2]
Unnamed_thm2 [definition, in PRFA.live_coding5]
Unnamed_thm2 [definition, in PRFA.live_coding5]
Unnamed_thm1 [definition, in PRFA.live_coding5]
Unnamed_thm0 [definition, in PRFA.live_coding5]
Unnamed_thm [definition, in PRFA.live_coding5]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm5 [definition, in PRFA.live_coding3]
Unnamed_thm4 [definition, in PRFA.live_coding3]
Unnamed_thm3 [definition, in PRFA.live_coding3]
Unnamed_thm2 [definition, in PRFA.live_coding3]
Unnamed_thm1 [definition, in PRFA.live_coding3]
Unnamed_thm0 [definition, in PRFA.live_coding3]
Unnamed_thm [definition, in PRFA.live_coding3]
Unnamed_thm0 [definition, in PRFA.tp3c]
Unnamed_thm [definition, in PRFA.tp3c]
Unnamed_thm2 [definition, in PRFA.live_coding4]
Unnamed_thm1 [definition, in PRFA.live_coding4]
Unnamed_thm0 [definition, in PRFA.live_coding4]
Unnamed_thm [definition, in PRFA.live_coding4]
Unnamed_thm [definition, in PRFA.review2]
W
Well_founded.R [variable, in PRFA.live_coding5]Well_founded.A [variable, in PRFA.live_coding5]
Well_founded [section, in PRFA.live_coding5]
WO [section, in PRFA.live_coding5]
WO.f [variable, in PRFA.live_coding5]
X
xtree [inductive, in PRFA.tp3c]xtree_rect_strong [definition, in PRFA.tp3c]
xtree_sind [definition, in PRFA.tp3c]
xtree_rec [definition, in PRFA.tp3c]
xtree_ind [definition, in PRFA.tp3c]
xtree_rect [definition, in PRFA.tp3c]
Z
zero [definition, in PRFA.tp2c]other
_ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]' _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
mlet ' _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
mlet _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ =<< _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ >>= _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ == _ [notation, in PRFA.MetaCoqPrelude]
_ ~ _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.live_coding4]
__ [notation, in PRFA.MetaCoqPrelude]
$name _ [notation, in PRFA.MetaCoqPrelude]
$Quote_rec _ [notation, in PRFA.MetaCoqPrelude]
$quote_rec _ [notation, in PRFA.MetaCoqPrelude]
$Quote _ [notation, in PRFA.MetaCoqPrelude]
$quote _ [notation, in PRFA.MetaCoqPrelude]
$run _ [notation, in PRFA.MetaCoqPrelude]
$unquote _ : _ [notation, in PRFA.MetaCoqPrelude]
$unquote _ [notation, in PRFA.MetaCoqPrelude]
Notation Index
D
_ - _ [in PRFA.tp2c]_ + _ [in PRFA.tp2c]
_ - _ [in PRFA.live_coding2]
_ + _ [in PRFA.live_coding2]
S
~ _ [in PRFA.live_coding3]other
_ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]' _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
mlet ' _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
mlet _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ =<< _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ >>= _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ == _ [in PRFA.MetaCoqPrelude]
_ ~ _ [in PRFA.tp4c]
_ ** _ [in PRFA.tp4c]
_ ** _ [in PRFA.tp4c]
_ ** _ [in PRFA.live_coding4]
__ [in PRFA.MetaCoqPrelude]
$name _ [in PRFA.MetaCoqPrelude]
$Quote_rec _ [in PRFA.MetaCoqPrelude]
$quote_rec _ [in PRFA.MetaCoqPrelude]
$Quote _ [in PRFA.MetaCoqPrelude]
$quote _ [in PRFA.MetaCoqPrelude]
$run _ [in PRFA.MetaCoqPrelude]
$unquote _ : _ [in PRFA.MetaCoqPrelude]
$unquote _ [in PRFA.MetaCoqPrelude]
Module Index
D
define_nat [in PRFA.tp2c]define_sigma [in PRFA.live_coding2]
define_list [in PRFA.live_coding2]
define_prod [in PRFA.live_coding2]
define_bool [in PRFA.live_coding2]
define_nat.variant2 [in PRFA.live_coding2]
define_nat.variant1 [in PRFA.live_coding2]
define_nat [in PRFA.live_coding2]
F
Fib_Iter [in PRFA.tp2c]H
Hierarchy [in PRFA.tp3c]S
Show_Definitions [in PRFA.live_coding3]Variable Index
D
Demo.X [in PRFA.live_coding3]Demo.Y [in PRFA.live_coding3]
Demo.Z [in PRFA.live_coding3]
U
Universes.A [in PRFA.live_coding5]Universes.B [in PRFA.live_coding5]
Universes.C [in PRFA.live_coding5]
Universes.P [in PRFA.live_coding5]
Universes.Q [in PRFA.live_coding5]
W
Well_founded.R [in PRFA.live_coding5]Well_founded.A [in PRFA.live_coding5]
WO.f [in PRFA.live_coding5]
Library Index
L
live_coding6live_coding5
live_coding2
live_coding1
live_coding4
live_coding3
M
MetaCoqPreludeR
review2review3
review4
T
tp1ctp2c
tp3c
tp4c
Lemma Index
A
Acc_iff [in PRFA.live_coding5]add_from_nat [in PRFA.tp2c]
add_sub [in PRFA.review2]
andb_orb_distr [in PRFA.tp1c]
andb_comm' [in PRFA.live_coding1]
andb_comm [in PRFA.live_coding1]
and_comm [in PRFA.tp1c]
and_assoc [in PRFA.tp4c]
and_com [in PRFA.tp4c]
and_AA [in PRFA.tp4c]
and_comm [in PRFA.live_coding1]
anything_goes [in PRFA.tp1c]
anything_goes [in PRFA.live_coding1]
app_assoc [in PRFA.tp2c]
app_nil_r [in PRFA.tp2c]
app_nil_r [in PRFA.live_coding2]
B
bad_not_bad [in PRFA.tp3c]bt_map_id [in PRFA.live_coding5]
C
calc_12_3 [in PRFA.tp1c]calc_12_3 [in PRFA.live_coding1]
cancel_to_of [in PRFA.tp2c]
cancel_of_to [in PRFA.tp2c]
car_cur [in PRFA.tp2c]
car_cur [in PRFA.live_coding2]
classical_impl [in PRFA.tp1c]
classical_or_contra_r [in PRFA.tp1c]
contrad [in PRFA.tp1c]
contrapositive [in PRFA.tp1c]
cur_car [in PRFA.tp2c]
cur_car [in PRFA.live_coding2]
D
define_nat.add_sub_alt [in PRFA.tp2c]define_nat.sub_O [in PRFA.tp2c]
define_nat.add_sub [in PRFA.tp2c]
define_nat.add_S [in PRFA.tp2c]
define_nat.add_0 [in PRFA.tp2c]
define_bool.true_false [in PRFA.live_coding2]
define_nat.eq_nat_spec [in PRFA.live_coding2]
define_nat.eq_nat_spec [in PRFA.live_coding2]
define_nat.S_inj_4 [in PRFA.live_coding2]
define_nat.S_inj_3 [in PRFA.live_coding2]
define_nat.S_inj_2 [in PRFA.live_coding2]
define_nat.S_inj [in PRFA.live_coding2]
define_nat.S_0' [in PRFA.live_coding2]
define_nat.S_O [in PRFA.live_coding2]
define_nat.add_sub [in PRFA.live_coding2]
define_nat.add_S [in PRFA.live_coding2]
define_nat.add_0 [in PRFA.live_coding2]
de_morgan [in PRFA.tp1c]
distr [in PRFA.tp1c]
dns_lem [in PRFA.tp1c]
dn_functorial [in PRFA.tp1c]
double_eq [in PRFA.tp1c]
double_eq2 [in PRFA.live_coding1]
double_eq [in PRFA.live_coding1]
E
eq_nat_spec [in PRFA.tp2c]eq_nat_spec [in PRFA.review2]
evenb_to_even [in PRFA.live_coding2]
evenb_to_even [in PRFA.live_coding2]
even_to_evenb [in PRFA.live_coding2]
even_plus_four_refine [in PRFA.live_coding3]
even_plus_four [in PRFA.live_coding3]
even_four [in PRFA.live_coding3]
even1_to_even2 [in PRFA.tp2c]
even2_iff_even3 [in PRFA.tp2c]
even2_iff_even3 [in PRFA.review2]
even3_to_even4 [in PRFA.tp2c]
even4_to_even1 [in PRFA.tp2c]
exercise_chain [in PRFA.live_coding5]
exercise_loop [in PRFA.live_coding5]
exp_from_nat [in PRFA.tp2c]
F
fact_equiv [in PRFA.tp2c]falsefalse [in PRFA.live_coding1]
False_forall [in PRFA.tp1c]
fast_rev_eq_alt [in PRFA.tp2c]
fast_rev_eq [in PRFA.tp2c]
fast_rev_eq_alt [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
Fib_Iter.fib_eq3 [in PRFA.tp2c]
Fib_Iter.fib_eq1 [in PRFA.tp2c]
Fib_Iter.fib_eq0 [in PRFA.tp2c]
forall_or [in PRFA.tp1c]
forall_False' [in PRFA.tp1c]
forall_False [in PRFA.tp1c]
Forall_set_eq [in PRFA.tp4c]
Forall_In [in PRFA.tp4c]
from_to_tree_alt [in PRFA.tp3c]
G
good_tree_ind [in PRFA.live_coding5]good_tree_ind' [in PRFA.live_coding5]
group_inverse_unique [in PRFA.tp4c]
group_neutral_unique [in PRFA.tp4c]
group_fact [in PRFA.tp4c]
G_zero [in PRFA.live_coding5]
G_sig [in PRFA.live_coding5]
H
Hierarchy.embeds_refl [in PRFA.tp3c]Hierarchy.hier [in PRFA.tp3c]
Hierarchy.hierarchy [in PRFA.tp3c]
Hierarchy.inconsistent [in PRFA.tp3c]
Hierarchy.sub_irrefl [in PRFA.tp3c]
I
iAnd_and [in PRFA.review3]iAnd_iff [in PRFA.tp3c]
iEx_ex [in PRFA.review3]
iEx_iff [in PRFA.tp3c]
iFalse_iff [in PRFA.tp3c]
imp_trans [in PRFA.tp1c]
in_cons [in PRFA.review4]
in_add_left [in PRFA.review4]
in_add_right [in PRFA.review4]
In_iff [in PRFA.tp2c]
In_app_inv [in PRFA.tp4c]
In_hd_eq [in PRFA.tp4c]
In_app_r [in PRFA.tp4c]
In_app_l [in PRFA.tp4c]
In_hd' [in PRFA.tp4c]
In_4 [in PRFA.tp4c]
In_tl [in PRFA.tp4c]
In_hd [in PRFA.tp4c]
In_hd' [in PRFA.live_coding4]
In_4 [in PRFA.live_coding4]
In_tl [in PRFA.live_coding4]
In_hd [in PRFA.live_coding4]
iOr_iff [in PRFA.tp3c]
iter_shift [in PRFA.tp2c]
iter_pow [in PRFA.tp2c]
iter_mul [in PRFA.live_coding2]
iter_add [in PRFA.live_coding2]
iTrue_iff [in PRFA.tp3c]
L
leb_spec_alt [in PRFA.tp2c]leb_spec [in PRFA.tp2c]
lem_dns [in PRFA.tp1c]
lem_pl [in PRFA.tp1c]
le_n_S [in PRFA.review3]
le_equiv [in PRFA.tp2c]
le_n_S [in PRFA.tp2c]
le_0_n [in PRFA.tp2c]
le_rtclos [in PRFA.live_coding2]
le_trans [in PRFA.live_coding2]
le_iff [in PRFA.live_coding2]
le'_n_S [in PRFA.tp2c]
le'_refl [in PRFA.tp2c]
linear_search [in PRFA.live_coding5]
list_seq_eq_app [in PRFA.tp4c]
list_fact [in PRFA.tp4c]
lt_plus_4 [in PRFA.tp3c]
M
memb_spec [in PRFA.tp4c]min_comm [in PRFA.tp1c]
monoid_fact [in PRFA.tp4c]
monoid_fact [in PRFA.live_coding4]
mult_distr_lia [in PRFA.tp1c]
mult_distr [in PRFA.tp1c]
mult_comm [in PRFA.tp1c]
mult_S [in PRFA.tp1c]
mult_0 [in PRFA.tp1c]
mul_from_nat [in PRFA.tp2c]
N
nat_fact [in PRFA.tp4c]nat_nat_fact [in PRFA.live_coding4]
nat_nat_fact [in PRFA.live_coding4]
nat_fact [in PRFA.live_coding4]
negb_invol [in PRFA.live_coding1]
negb_true [in PRFA.live_coding1]
nofalse [in PRFA.tp1c]
nofalse [in PRFA.live_coding1]
n_plus_0 [in PRFA.tp1c]
O
of_nat_inj [in PRFA.tp2c]one_zero_Z [in PRFA.tp4c]
or_imp [in PRFA.tp1c]
or_comm [in PRFA.tp1c]
or_com [in PRFA.tp4c]
or_AA [in PRFA.tp4c]
or_comm [in PRFA.live_coding1]
P
plus_assoc [in PRFA.tp1c]plus_comm [in PRFA.tp1c]
plus_S [in PRFA.tp1c]
pl_lem [in PRFA.tp1c]
pneg_invol [in PRFA.live_coding5]
pred_from_nat [in PRFA.tp2c]
pred'_from_nat [in PRFA.tp2c]
P_iff_P [in PRFA.tp1c]
P_imp_P [in PRFA.tp1c]
P_imp_P [in PRFA.live_coding1]
R
rev_rev [in PRFA.tp2c]rev_app_distr [in PRFA.tp2c]
rev_rev [in PRFA.live_coding2]
rev_app_distr [in PRFA.live_coding2]
rtclos_iff [in PRFA.tp2c]
rtclos'_trans [in PRFA.tp2c]
Russel [in PRFA.tp1c]
Russell [in PRFA.live_coding3]
S
size_recursion [in PRFA.live_coding5]strong_nat_ind [in PRFA.tp2c]
strong_nat_ind [in PRFA.live_coding2]
strong_nat_ind [in PRFA.review2]
swap_invol [in PRFA.tp2c]
S_neq [in PRFA.tp3c]
T
test [in PRFA.live_coding6]test_list [in PRFA.tp4c]
test_nat' [in PRFA.tp4c]
test_monoid [in PRFA.tp4c]
test_nat [in PRFA.tp4c]
test_nat' [in PRFA.live_coding4]
test_monoid [in PRFA.live_coding4]
test_nat [in PRFA.live_coding4]
to_nat_inj [in PRFA.tp2c]
to_not_not [in PRFA.tp1c]
to_prod_eq [in PRFA.tp4c]
to_tree_map [in PRFA.live_coding5]
to_bool_function_not_PI [in PRFA.live_coding5]
to_bool [in PRFA.live_coding5]
to_bool [in PRFA.live_coding5]
to_from_tree [in PRFA.tp3c]
tree_map_id_again' [in PRFA.live_coding5]
tree_map_id_again [in PRFA.live_coding5]
tree_map_id [in PRFA.live_coding5]
truetrue [in PRFA.tp1c]
truetrue [in PRFA.live_coding1]
true_false [in PRFA.review3]
true_false [in PRFA.tp2c]
twice [in PRFA.tp1c]
Constructor Index
A
Acc_intro [in PRFA.live_coding5]All_cons [in PRFA.tp3c]
All_nil [in PRFA.tp3c]
B
box [in PRFA.live_coding5]bt_node [in PRFA.live_coding5]
bt_leaf [in PRFA.live_coding5]
C
C [in PRFA.live_coding3]C [in PRFA.tp3c]
D
define_nat.S [in PRFA.tp2c]define_nat.O [in PRFA.tp2c]
define_sigma.existT [in PRFA.live_coding2]
define_list.cons [in PRFA.live_coding2]
define_list.nil [in PRFA.live_coding2]
define_prod.pair [in PRFA.live_coding2]
define_bool.false [in PRFA.live_coding2]
define_bool.true [in PRFA.live_coding2]
define_nat.variant2.S [in PRFA.live_coding2]
define_nat.variant2.O [in PRFA.live_coding2]
define_nat.variant1.S [in PRFA.live_coding2]
define_nat.variant1.O [in PRFA.live_coding2]
define_nat.S [in PRFA.live_coding2]
define_nat.O [in PRFA.live_coding2]
E
evenO [in PRFA.review3]evenO [in PRFA.tp2c]
evenO [in PRFA.live_coding2]
evenO [in PRFA.live_coding3]
evenS [in PRFA.review3]
evenS [in PRFA.tp2c]
evenS [in PRFA.live_coding2]
evenS [in PRFA.live_coding3]
G
GI [in PRFA.live_coding5]H
Hierarchy.T [in PRFA.tp3c]I
incl [in PRFA.tp2c]incl [in PRFA.live_coding2]
in_tl [in PRFA.tp2c]
in_hd [in PRFA.tp2c]
L
leO [in PRFA.live_coding2]leO' [in PRFA.tp2c]
leS [in PRFA.live_coding2]
leS' [in PRFA.tp2c]
lt_S [in PRFA.review3]
lt_B [in PRFA.review3]
lt_S [in PRFA.tp3c]
lt_B [in PRFA.tp3c]
M
mult4_plus [in PRFA.live_coding6]mult4_0 [in PRFA.live_coding6]
N
N [in PRFA.live_coding3]N [in PRFA.tp3c]
ncons [in PRFA.live_coding3]
ncons [in PRFA.tp3c]
nnil [in PRFA.live_coding3]
nnil [in PRFA.tp3c]
nnode [in PRFA.live_coding3]
nnode [in PRFA.tp3c]
node [in PRFA.live_coding5]
not_mult4_plus [in PRFA.live_coding6]
not_mult4_3 [in PRFA.live_coding6]
not_mult4_2 [in PRFA.live_coding6]
not_mult4_1 [in PRFA.live_coding6]
Nx [in PRFA.tp3c]
P
pfalse [in PRFA.live_coding5]ptrue [in PRFA.live_coding5]
R
refl [in PRFA.tp2c]refl [in PRFA.live_coding2]
refl' [in PRFA.tp2c]
S
Show_Definitions.or_intror [in PRFA.live_coding3]Show_Definitions.or_introl [in PRFA.live_coding3]
Show_Definitions.conj [in PRFA.live_coding3]
Show_Definitions.I [in PRFA.live_coding3]
T
trans [in PRFA.tp2c]trans [in PRFA.live_coding2]
trans' [in PRFA.tp2c]
Axiom Index
D
DNE [in PRFA.live_coding4]Inductive Index
A
Acc [in PRFA.live_coding5]All [in PRFA.tp3c]
B
bad [in PRFA.live_coding3]bad [in PRFA.tp3c]
bintree [in PRFA.live_coding5]
Box [in PRFA.live_coding5]
D
define_nat.nat [in PRFA.tp2c]define_sigma.sigT [in PRFA.live_coding2]
define_list.list [in PRFA.live_coding2]
define_prod.prod [in PRFA.live_coding2]
define_bool.bool [in PRFA.live_coding2]
define_nat.variant2.nat [in PRFA.live_coding2]
define_nat.variant1.nat [in PRFA.live_coding2]
define_nat.nat [in PRFA.live_coding2]
E
even [in PRFA.review3]even [in PRFA.live_coding2]
even [in PRFA.live_coding3]
even4 [in PRFA.tp2c]
G
G [in PRFA.live_coding5]H
Hierarchy.tree [in PRFA.tp3c]I
In_i [in PRFA.tp2c]L
le [in PRFA.live_coding2]le' [in PRFA.tp2c]
lt [in PRFA.review3]
lt [in PRFA.tp3c]
M
mult4 [in PRFA.live_coding6]N
nforest [in PRFA.live_coding3]nforest [in PRFA.tp3c]
not_mult4 [in PRFA.live_coding6]
ntree [in PRFA.live_coding3]
ntree [in PRFA.tp3c]
P
prop_bool [in PRFA.live_coding5]R
rtclos [in PRFA.tp2c]rtclos [in PRFA.live_coding2]
rtclos' [in PRFA.tp2c]
S
Show_Definitions.or [in PRFA.live_coding3]Show_Definitions.and [in PRFA.live_coding3]
Show_Definitions.True [in PRFA.live_coding3]
Show_Definitions.False [in PRFA.live_coding3]
T
tree [in PRFA.live_coding5]tree [in PRFA.live_coding3]
tree [in PRFA.tp3c]
X
xtree [in PRFA.tp3c]Projection Index
D
denominator [in PRFA.live_coding4]denominator' [in PRFA.live_coding4]
denominator'' [in PRFA.live_coding4]
den_not_zero [in PRFA.live_coding4]
E
eqb [in PRFA.tp4c]eqb [in PRFA.live_coding4]
eqb_iff [in PRFA.tp4c]
eqb_iff [in PRFA.live_coding4]
F
fst' [in PRFA.review4]fst' [in PRFA.tp4c]
fst' [in PRFA.live_coding4]
G
group_inv [in PRFA.tp4c]group_assoc [in PRFA.tp4c]
group_right_neutral [in PRFA.tp4c]
group_left_neutral [in PRFA.tp4c]
g_inv [in PRFA.tp4c]
g_mon [in PRFA.tp4c]
M
mon_assoc [in PRFA.tp4c]mon_right_neutral [in PRFA.tp4c]
mon_left_neutral [in PRFA.tp4c]
mon_assoc [in PRFA.live_coding4]
mon_right_neutral [in PRFA.live_coding4]
mon_left_neutral [in PRFA.live_coding4]
m_assoc [in PRFA.tp4c]
m_r_ne [in PRFA.tp4c]
m_l_ne [in PRFA.tp4c]
m_op [in PRFA.tp4c]
m_ne [in PRFA.tp4c]
m_ty [in PRFA.tp4c]
m_assoc [in PRFA.live_coding4]
m_r_ne [in PRFA.live_coding4]
m_l_ne [in PRFA.live_coding4]
m_op [in PRFA.live_coding4]
m_ne [in PRFA.live_coding4]
m_ty [in PRFA.live_coding4]
N
numerator [in PRFA.live_coding4]numerator' [in PRFA.live_coding4]
numerator'' [in PRFA.live_coding4]
S
snd' [in PRFA.review4]snd' [in PRFA.tp4c]
snd' [in PRFA.live_coding4]
Section Index
A
Advanced [in PRFA.tp1c]D
Demo [in PRFA.live_coding3]L
Live [in PRFA.live_coding1]T
TP1 [in PRFA.tp1c]U
Universes [in PRFA.live_coding5]W
Well_founded [in PRFA.live_coding5]WO [in PRFA.live_coding5]
Instance Index
E
Eq_nat [in PRFA.tp4c]Eq_nat [in PRFA.live_coding4]
G
Group_Z [in PRFA.tp4c]L
list_set_eq_trans [in PRFA.tp4c]list_set_eq_sym [in PRFA.tp4c]
list_set_eq_refl [in PRFA.tp4c]
M
MonoidList [in PRFA.tp4c]MonoidNat [in PRFA.tp4c]
MonoidNat [in PRFA.live_coding4]
MonoidProd [in PRFA.tp4c]
MonoidProd [in PRFA.live_coding4]
Monoid_Group [in PRFA.tp4c]
Abbreviation Index
T
tLam [in PRFA.MetaCoqPrelude]tLet [in PRFA.MetaCoqPrelude]
Definition Index
A
Acc_sind [in PRFA.live_coding5]Acc_rec [in PRFA.live_coding5]
Acc_ind [in PRFA.live_coding5]
Acc_rect [in PRFA.live_coding5]
add [in PRFA.tp2c]
add [in PRFA.live_coding3]
All_sind [in PRFA.tp3c]
All_rec [in PRFA.tp3c]
All_ind [in PRFA.tp3c]
All_rect [in PRFA.tp3c]
B
bar [in PRFA.live_coding3]baz [in PRFA.live_coding3]
below [in PRFA.tp3c]
bintree_sind [in PRFA.live_coding5]
bintree_rec [in PRFA.live_coding5]
bintree_ind [in PRFA.live_coding5]
bintree_rect [in PRFA.live_coding5]
Box_sind [in PRFA.live_coding5]
Box_rec [in PRFA.live_coding5]
Box_ind [in PRFA.live_coding5]
Box_rect [in PRFA.live_coding5]
brec [in PRFA.tp3c]
brec' [in PRFA.tp3c]
bt_to_tree [in PRFA.live_coding5]
bt_map [in PRFA.live_coding5]
C
car [in PRFA.tp2c]car [in PRFA.live_coding2]
car' [in PRFA.tp2c]
car'' [in PRFA.tp2c]
count [in PRFA.live_coding3]
count [in PRFA.tp3c]
count_list [in PRFA.live_coding3]
count_list [in PRFA.tp3c]
cur [in PRFA.tp2c]
cur [in PRFA.live_coding2]
D
define_nat.sub [in PRFA.tp2c]define_nat.add [in PRFA.tp2c]
define_nat.nat_sind [in PRFA.tp2c]
define_nat.nat_rec [in PRFA.tp2c]
define_nat.nat_ind [in PRFA.tp2c]
define_nat.nat_rect [in PRFA.tp2c]
define_sigma.pair2 [in PRFA.live_coding2]
define_sigma.pair1 [in PRFA.live_coding2]
define_sigma.T [in PRFA.live_coding2]
define_sigma.sigT_sind [in PRFA.live_coding2]
define_sigma.sigT_rec [in PRFA.live_coding2]
define_sigma.sigT_ind [in PRFA.live_coding2]
define_sigma.sigT_rect [in PRFA.live_coding2]
define_list.list_sind [in PRFA.live_coding2]
define_list.list_rec [in PRFA.live_coding2]
define_list.list_ind [in PRFA.live_coding2]
define_list.list_rect [in PRFA.live_coding2]
define_prod.snd [in PRFA.live_coding2]
define_prod.fst [in PRFA.live_coding2]
define_prod.pair' [in PRFA.live_coding2]
define_prod.prod_sind [in PRFA.live_coding2]
define_prod.prod_rec [in PRFA.live_coding2]
define_prod.prod_ind [in PRFA.live_coding2]
define_prod.prod_rect [in PRFA.live_coding2]
define_bool.bool_sind [in PRFA.live_coding2]
define_bool.bool_rec [in PRFA.live_coding2]
define_bool.bool_ind [in PRFA.live_coding2]
define_bool.bool_rect [in PRFA.live_coding2]
define_nat.eq_nat [in PRFA.live_coding2]
define_nat.pred [in PRFA.live_coding2]
define_nat.is_zero [in PRFA.live_coding2]
define_nat.is_zerob [in PRFA.live_coding2]
define_nat.sub [in PRFA.live_coding2]
define_nat.add [in PRFA.live_coding2]
define_nat.variant2.nat_sind [in PRFA.live_coding2]
define_nat.variant2.nat_rec [in PRFA.live_coding2]
define_nat.variant2.nat_ind [in PRFA.live_coding2]
define_nat.variant2.nat_rect [in PRFA.live_coding2]
define_nat.variant1.nat_sind [in PRFA.live_coding2]
define_nat.variant1.nat_rec [in PRFA.live_coding2]
define_nat.variant1.nat_ind [in PRFA.live_coding2]
define_nat.variant1.nat_rect [in PRFA.live_coding2]
define_nat.nat_sind [in PRFA.live_coding2]
define_nat.nat_rec [in PRFA.live_coding2]
define_nat.nat_ind [in PRFA.live_coding2]
define_nat.nat_rect [in PRFA.live_coding2]
dependent [in PRFA.live_coding3]
DNS [in PRFA.tp1c]
double [in PRFA.live_coding1]
double_S [in PRFA.live_coding6]
E
elim_or [in PRFA.live_coding3]elim_and [in PRFA.live_coding3]
elim_False [in PRFA.live_coding3]
empty_tree [in PRFA.live_coding3]
eq_nat [in PRFA.tp2c]
eq_nat [in PRFA.review2]
evenb [in PRFA.live_coding2]
even_sind [in PRFA.review3]
even_ind [in PRFA.review3]
even_sind [in PRFA.live_coding2]
even_ind [in PRFA.live_coding2]
even_plus_four_term [in PRFA.live_coding3]
even_four' [in PRFA.live_coding3]
even_sind [in PRFA.live_coding3]
even_ind [in PRFA.live_coding3]
even1 [in PRFA.tp2c]
even2 [in PRFA.tp2c]
even2 [in PRFA.review2]
even3 [in PRFA.tp2c]
even3 [in PRFA.review2]
even4_sind [in PRFA.tp2c]
even4_ind [in PRFA.tp2c]
exfalso' [in PRFA.live_coding5]
exp [in PRFA.tp2c]
ex1 [in PRFA.tp3c]
ex2 [in PRFA.tp3c]
ex3 [in PRFA.tp3c]
ex3_alt [in PRFA.tp3c]
ex4 [in PRFA.tp3c]
F
f [in PRFA.live_coding3]f [in PRFA.tp3c]
fact_iter [in PRFA.tp2c]
fact_iter_f [in PRFA.tp2c]
fact_fix [in PRFA.tp2c]
fast_rev [in PRFA.tp2c]
fast_rev [in PRFA.live_coding2]
fib [in PRFA.tp3c]
Fib_Iter.fib [in PRFA.tp2c]
Fib_Iter.sigma [in PRFA.tp2c]
fib_brec [in PRFA.tp3c]
fib_natrec [in PRFA.tp3c]
fold_def [in PRFA.MetaCoqPrelude]
fold_branches [in PRFA.MetaCoqPrelude]
fold_branch [in PRFA.MetaCoqPrelude]
fold_predicate [in PRFA.MetaCoqPrelude]
fold_handler [in PRFA.MetaCoqPrelude]
foo [in PRFA.tp4c]
foo [in PRFA.live_coding3]
foo [in PRFA.live_coding4]
from_nat [in PRFA.tp2c]
from_to_tree_list [in PRFA.tp3c]
from_to_tree [in PRFA.tp3c]
from_tree_list [in PRFA.tp3c]
from_tree [in PRFA.tp3c]
G
get_kername [in PRFA.MetaCoqPrelude]G_sind [in PRFA.live_coding5]
G_rec [in PRFA.live_coding5]
G_ind [in PRFA.live_coding5]
G_rect [in PRFA.live_coding5]
H
half [in PRFA.live_coding4]half' [in PRFA.live_coding4]
Hierarchy.embeds [in PRFA.tp3c]
Hierarchy.sub [in PRFA.tp3c]
Hierarchy.tree_sind [in PRFA.tp3c]
Hierarchy.tree_rec [in PRFA.tp3c]
Hierarchy.tree_ind [in PRFA.tp3c]
Hierarchy.tree_rect [in PRFA.tp3c]
Hierarchy.Tyi [in PRFA.tp3c]
I
iAnd [in PRFA.review3]iAnd [in PRFA.tp3c]
idNat [in PRFA.live_coding6]
idnat [in PRFA.tp3c]
iEx [in PRFA.review3]
iEx [in PRFA.tp3c]
iFalse [in PRFA.review3]
iFalse [in PRFA.tp3c]
In [in PRFA.tp2c]
In_i_sind [in PRFA.tp2c]
In_i_ind [in PRFA.tp2c]
iOr [in PRFA.tp3c]
iter [in PRFA.tp2c]
iter [in PRFA.live_coding2]
iTrue [in PRFA.tp3c]
L
least [in PRFA.live_coding5]leb [in PRFA.tp2c]
LEM [in PRFA.tp1c]
le_sind [in PRFA.live_coding2]
le_ind [in PRFA.live_coding2]
le'_sind [in PRFA.tp2c]
le'_ind [in PRFA.tp2c]
list_set_eq [in PRFA.tp4c]
list_monoid [in PRFA.tp4c]
list_rect [in PRFA.live_coding3]
lt_plus_4' [in PRFA.review3]
lt_plus_4 [in PRFA.review3]
lt_sind [in PRFA.review3]
lt_ind [in PRFA.review3]
lt_plus_4' [in PRFA.tp3c]
lt_sind [in PRFA.tp3c]
lt_ind [in PRFA.tp3c]
M
memb [in PRFA.tp4c]memb [in PRFA.live_coding4]
min [in PRFA.tp1c]
mpow [in PRFA.live_coding6]
mpow' [in PRFA.live_coding6]
mul [in PRFA.tp2c]
mult4_sind [in PRFA.live_coding6]
mult4_ind [in PRFA.live_coding6]
N
nat_monoid [in PRFA.tp4c]nat_rect [in PRFA.live_coding3]
nat_monoid [in PRFA.live_coding4]
nforest_sind [in PRFA.live_coding3]
nforest_rec [in PRFA.live_coding3]
nforest_ind [in PRFA.live_coding3]
nforest_rect [in PRFA.live_coding3]
nforest_ntree_rec [in PRFA.tp3c]
nforest_map [in PRFA.tp3c]
nforest_sind [in PRFA.tp3c]
nforest_rec [in PRFA.tp3c]
nforest_ind [in PRFA.tp3c]
nforest_rect [in PRFA.tp3c]
not_mult4_sind [in PRFA.live_coding6]
not_mult4_ind [in PRFA.live_coding6]
ntree_sind [in PRFA.live_coding3]
ntree_rec [in PRFA.live_coding3]
ntree_ind [in PRFA.live_coding3]
ntree_rect [in PRFA.live_coding3]
ntree_nforest_rec [in PRFA.tp3c]
ntree_map [in PRFA.tp3c]
ntree_sind [in PRFA.tp3c]
ntree_rec [in PRFA.tp3c]
ntree_ind [in PRFA.tp3c]
ntree_rect [in PRFA.tp3c]
num [in PRFA.tp2c]
O
of_nat [in PRFA.tp2c]or_imp [in PRFA.review3]
or_comm [in PRFA.tp3c]
P
PI [in PRFA.live_coding5]PL [in PRFA.tp1c]
pneg [in PRFA.live_coding5]
pow13 [in PRFA.live_coding6]
pow3 [in PRFA.live_coding6]
pow5 [in PRFA.live_coding6]
pred [in PRFA.tp2c]
pred' [in PRFA.tp2c]
prod_monoid [in PRFA.tp4c]
prod_monoid [in PRFA.live_coding4]
prod'_ind [in PRFA.review4]
prop_bool_sind [in PRFA.live_coding5]
prop_bool_ind [in PRFA.live_coding5]
Q
quarter [in PRFA.live_coding4]quarter'' [in PRFA.live_coding4]
R
REPLACE_ME [in PRFA.tp1c]rtclos_sind [in PRFA.tp2c]
rtclos_ind [in PRFA.tp2c]
rtclos_sind [in PRFA.live_coding2]
rtclos_ind [in PRFA.live_coding2]
rtclos'_sind [in PRFA.tp2c]
rtclos'_ind [in PRFA.tp2c]
Russel [in PRFA.review3]
Russel [in PRFA.review3]
Russel [in PRFA.tp3c]
S
Show_Definitions.or_sind [in PRFA.live_coding3]Show_Definitions.or_ind [in PRFA.live_coding3]
Show_Definitions.and_sind [in PRFA.live_coding3]
Show_Definitions.and_rec [in PRFA.live_coding3]
Show_Definitions.and_ind [in PRFA.live_coding3]
Show_Definitions.and_rect [in PRFA.live_coding3]
Show_Definitions.True_sind [in PRFA.live_coding3]
Show_Definitions.True_rec [in PRFA.live_coding3]
Show_Definitions.True_ind [in PRFA.live_coding3]
Show_Definitions.True_rect [in PRFA.live_coding3]
Show_Definitions.False_sind [in PRFA.live_coding3]
Show_Definitions.False_rec [in PRFA.live_coding3]
Show_Definitions.False_ind [in PRFA.live_coding3]
Show_Definitions.False_rect [in PRFA.live_coding3]
some_other_pair [in PRFA.tp4c]
some_pair [in PRFA.tp4c]
some_tree [in PRFA.live_coding3]
some_other_pair [in PRFA.live_coding4]
some_pair [in PRFA.live_coding4]
succ [in PRFA.tp2c]
swap [in PRFA.tp2c]
T
T [in PRFA.live_coding3]term_eqb [in PRFA.MetaCoqPrelude]
theDNS [in PRFA.tp1c]
theLEM [in PRFA.tp1c]
thePL [in PRFA.tp1c]
tm_fold [in PRFA.MetaCoqPrelude]
tm_nb_handler [in PRFA.MetaCoqPrelude]
tm_handler [in PRFA.MetaCoqPrelude]
tNat [in PRFA.live_coding6]
to_nat [in PRFA.tp2c]
to_nat' [in PRFA.tp2c]
to_prod_alt3 [in PRFA.tp4c]
to_prod_alt2 [in PRFA.tp4c]
to_prod_alt [in PRFA.tp4c]
to_prod [in PRFA.tp4c]
to_bool [in PRFA.live_coding5]
to_prop_bool [in PRFA.live_coding5]
to_tree_list [in PRFA.tp3c]
to_tree [in PRFA.tp3c]
to_prod_alt3 [in PRFA.live_coding4]
to_prod_alt2 [in PRFA.live_coding4]
to_prod_alt [in PRFA.live_coding4]
to_prod [in PRFA.live_coding4]
transform [in PRFA.MetaCoqPrelude]
transform_nb [in PRFA.MetaCoqPrelude]
tree_map_id [in PRFA.live_coding5]
tree_map [in PRFA.live_coding5]
tree_sind [in PRFA.live_coding5]
tree_rec [in PRFA.live_coding5]
tree_ind [in PRFA.live_coding5]
tree_rect [in PRFA.live_coding5]
tree_sind [in PRFA.live_coding3]
tree_rec [in PRFA.live_coding3]
tree_ind [in PRFA.live_coding3]
tree_rect [in PRFA.live_coding3]
tree_rect_strong [in PRFA.tp3c]
tree_sind [in PRFA.tp3c]
tree_rec [in PRFA.tp3c]
tree_ind [in PRFA.tp3c]
tree_rect [in PRFA.tp3c]
U
unfold_toplevel [in PRFA.MetaCoqPrelude]Unnamed_thm2 [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.live_coding6]
Unnamed_thm0 [in PRFA.live_coding6]
Unnamed_thm [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.review4]
Unnamed_thm0 [in PRFA.review4]
Unnamed_thm [in PRFA.review4]
Unnamed_thm18 [in PRFA.tp4c]
Unnamed_thm17 [in PRFA.tp4c]
Unnamed_thm16 [in PRFA.tp4c]
Unnamed_thm15 [in PRFA.tp4c]
Unnamed_thm14 [in PRFA.tp4c]
Unnamed_thm13 [in PRFA.tp4c]
Unnamed_thm12 [in PRFA.tp4c]
Unnamed_thm11 [in PRFA.tp4c]
Unnamed_thm10 [in PRFA.tp4c]
Unnamed_thm9 [in PRFA.tp4c]
Unnamed_thm8 [in PRFA.tp4c]
Unnamed_thm7 [in PRFA.tp4c]
Unnamed_thm6 [in PRFA.tp4c]
Unnamed_thm5 [in PRFA.tp4c]
Unnamed_thm4 [in PRFA.tp4c]
Unnamed_thm3 [in PRFA.tp4c]
Unnamed_thm2 [in PRFA.tp4c]
Unnamed_thm1 [in PRFA.tp4c]
Unnamed_thm0 [in PRFA.tp4c]
Unnamed_thm [in PRFA.tp4c]
Unnamed_thm4 [in PRFA.live_coding2]
Unnamed_thm3 [in PRFA.live_coding2]
Unnamed_thm2 [in PRFA.live_coding2]
Unnamed_thm1 [in PRFA.live_coding2]
Unnamed_thm1 [in PRFA.live_coding2]
Unnamed_thm0 [in PRFA.live_coding2]
Unnamed_thm [in PRFA.live_coding2]
Unnamed_thm2 [in PRFA.live_coding5]
Unnamed_thm2 [in PRFA.live_coding5]
Unnamed_thm1 [in PRFA.live_coding5]
Unnamed_thm0 [in PRFA.live_coding5]
Unnamed_thm [in PRFA.live_coding5]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm5 [in PRFA.live_coding3]
Unnamed_thm4 [in PRFA.live_coding3]
Unnamed_thm3 [in PRFA.live_coding3]
Unnamed_thm2 [in PRFA.live_coding3]
Unnamed_thm1 [in PRFA.live_coding3]
Unnamed_thm0 [in PRFA.live_coding3]
Unnamed_thm [in PRFA.live_coding3]
Unnamed_thm0 [in PRFA.tp3c]
Unnamed_thm [in PRFA.tp3c]
Unnamed_thm2 [in PRFA.live_coding4]
Unnamed_thm1 [in PRFA.live_coding4]
Unnamed_thm0 [in PRFA.live_coding4]
Unnamed_thm [in PRFA.live_coding4]
Unnamed_thm [in PRFA.review2]
X
xtree_rect_strong [in PRFA.tp3c]xtree_sind [in PRFA.tp3c]
xtree_rec [in PRFA.tp3c]
xtree_ind [in PRFA.tp3c]
xtree_rect [in PRFA.tp3c]
Z
zero [in PRFA.tp2c]Record Index
B
bad_rational2 [in PRFA.live_coding4]bad_rational1 [in PRFA.live_coding4]
E
Eq [in PRFA.tp4c]Eq [in PRFA.live_coding4]
G
Group [in PRFA.tp4c]group [in PRFA.tp4c]
M
Monoid [in PRFA.tp4c]monoid [in PRFA.tp4c]
Monoid [in PRFA.live_coding4]
monoid [in PRFA.live_coding4]
P
prod' [in PRFA.review4]prod' [in PRFA.tp4c]
prod' [in PRFA.live_coding4]
R
rational [in PRFA.live_coding4]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 | (845 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 | (26 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 | (11 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 | (11 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 | (14 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 | (218 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 | (72 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 | (1 entry) |
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 | (43 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 | (41 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 | (7 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 | (12 entries) |
Abbreviation 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) |
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 | (373 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 | (14 entries) |
This page has been generated by coqdoc