| 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 | (194 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 | (2 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 | (7 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 | (3 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 | (83 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 | (19 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 | (10 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 | (3 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 | (67 entries) |
Global Index
A
Advanced [section, in PRFA.tp1c]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_comm [lemma, in PRFA.live_coding1]
anything_goes [lemma, in PRFA.tp1c]
anything_goes [lemma, in PRFA.live_coding1]
app_nil_r [lemma, in PRFA.live_coding2]
C
calc_12_3 [lemma, in PRFA.tp1c]calc_12_3 [lemma, in PRFA.live_coding1]
car [definition, in PRFA.live_coding2]
car_cur [lemma, in PRFA.live_coding2]
classical_impl [lemma, in PRFA.tp1c]
classical_or_contra_r [lemma, in PRFA.tp1c]
contrad [lemma, in PRFA.tp1c]
contrapositive [lemma, in PRFA.tp1c]
cur [definition, in PRFA.live_coding2]
cur_car [lemma, in PRFA.live_coding2]
D
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]
de_morgan [lemma, in PRFA.tp1c]
distr [lemma, in PRFA.tp1c]
DNS [definition, in PRFA.tp1c]
dns_lem [lemma, in PRFA.tp1c]
dn_functorial [lemma, in PRFA.tp1c]
double [definition, in PRFA.live_coding1]
double_eq [lemma, in PRFA.tp1c]
double_eq2 [lemma, in PRFA.live_coding1]
double_eq [lemma, in PRFA.live_coding1]
E
even [inductive, in PRFA.live_coding2]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.live_coding2]
evenS [constructor, in PRFA.live_coding2]
even_to_evenb [lemma, in PRFA.live_coding2]
even_sind [definition, in PRFA.live_coding2]
even_ind [definition, in PRFA.live_coding2]
F
falsefalse [lemma, in PRFA.live_coding1]False_forall [lemma, in PRFA.tp1c]
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]
forall_or [lemma, in PRFA.tp1c]
forall_False' [lemma, in PRFA.tp1c]
forall_False [lemma, in PRFA.tp1c]
I
imp_trans [lemma, in PRFA.tp1c]incl [constructor, in PRFA.live_coding2]
iter [definition, in PRFA.live_coding2]
iter_mul [lemma, in PRFA.live_coding2]
iter_add [lemma, in PRFA.live_coding2]
L
le [inductive, in PRFA.live_coding2]LEM [definition, in PRFA.tp1c]
lem_dns [lemma, in PRFA.tp1c]
lem_pl [lemma, in PRFA.tp1c]
leO [constructor, in PRFA.live_coding2]
leS [constructor, in PRFA.live_coding2]
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]
Live [section, in PRFA.live_coding1]
live_coding2 [library]
live_coding1 [library]
M
min [definition, in PRFA.tp1c]min_comm [lemma, in PRFA.tp1c]
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]
N
negb_invol [lemma, in PRFA.live_coding1]negb_true [lemma, in PRFA.live_coding1]
nofalse [lemma, in PRFA.tp1c]
nofalse [lemma, in PRFA.live_coding1]
n_plus_0 [lemma, in PRFA.tp1c]
O
or_imp [lemma, in PRFA.tp1c]or_comm [lemma, in PRFA.tp1c]
or_comm [lemma, in PRFA.live_coding1]
P
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]
P_iff_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.live_coding1]
R
refl [constructor, in PRFA.live_coding2]REPLACE_ME [definition, in PRFA.tp1c]
rev_rev [lemma, in PRFA.live_coding2]
rev_app_distr [lemma, in PRFA.live_coding2]
rtclos [inductive, in PRFA.live_coding2]
rtclos_sind [definition, in PRFA.live_coding2]
rtclos_ind [definition, in PRFA.live_coding2]
Russel [lemma, in PRFA.tp1c]
S
strong_nat_ind [lemma, in PRFA.live_coding2]T
theDNS [definition, in PRFA.tp1c]theLEM [definition, in PRFA.tp1c]
thePL [definition, in PRFA.tp1c]
to_not_not [lemma, in PRFA.tp1c]
TP1 [section, in PRFA.tp1c]
tp1c [library]
trans [constructor, in PRFA.live_coding2]
truetrue [lemma, in PRFA.tp1c]
truetrue [lemma, in PRFA.live_coding1]
twice [lemma, in PRFA.tp1c]
U
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]
Notation Index
D
_ - _ [in PRFA.live_coding2]_ + _ [in PRFA.live_coding2]
Module Index
D
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]
Library Index
L
live_coding2live_coding1
T
tp1cLemma Index
A
andb_orb_distr [in PRFA.tp1c]andb_comm' [in PRFA.live_coding1]
andb_comm [in PRFA.live_coding1]
and_comm [in PRFA.tp1c]
and_comm [in PRFA.live_coding1]
anything_goes [in PRFA.tp1c]
anything_goes [in PRFA.live_coding1]
app_nil_r [in PRFA.live_coding2]
C
calc_12_3 [in PRFA.tp1c]calc_12_3 [in PRFA.live_coding1]
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.live_coding2]
D
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
evenb_to_even [in PRFA.live_coding2]evenb_to_even [in PRFA.live_coding2]
even_to_evenb [in PRFA.live_coding2]
F
falsefalse [in PRFA.live_coding1]False_forall [in PRFA.tp1c]
fast_rev_eq_alt [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
forall_or [in PRFA.tp1c]
forall_False' [in PRFA.tp1c]
forall_False [in PRFA.tp1c]
I
imp_trans [in PRFA.tp1c]iter_mul [in PRFA.live_coding2]
iter_add [in PRFA.live_coding2]
L
lem_dns [in PRFA.tp1c]lem_pl [in PRFA.tp1c]
le_rtclos [in PRFA.live_coding2]
le_trans [in PRFA.live_coding2]
le_iff [in PRFA.live_coding2]
M
min_comm [in PRFA.tp1c]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]
N
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
or_imp [in PRFA.tp1c]or_comm [in PRFA.tp1c]
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]
P_iff_P [in PRFA.tp1c]
P_imp_P [in PRFA.tp1c]
P_imp_P [in PRFA.live_coding1]
R
rev_rev [in PRFA.live_coding2]rev_app_distr [in PRFA.live_coding2]
Russel [in PRFA.tp1c]
S
strong_nat_ind [in PRFA.live_coding2]T
to_not_not [in PRFA.tp1c]truetrue [in PRFA.tp1c]
truetrue [in PRFA.live_coding1]
twice [in PRFA.tp1c]
Constructor Index
D
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.live_coding2]evenS [in PRFA.live_coding2]
I
incl [in PRFA.live_coding2]L
leO [in PRFA.live_coding2]leS [in PRFA.live_coding2]
R
refl [in PRFA.live_coding2]T
trans [in PRFA.live_coding2]Inductive Index
D
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.live_coding2]L
le [in PRFA.live_coding2]R
rtclos [in PRFA.live_coding2]Section Index
A
Advanced [in PRFA.tp1c]L
Live [in PRFA.live_coding1]T
TP1 [in PRFA.tp1c]Definition Index
C
car [in PRFA.live_coding2]cur [in PRFA.live_coding2]
D
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]
DNS [in PRFA.tp1c]
double [in PRFA.live_coding1]
E
evenb [in PRFA.live_coding2]even_sind [in PRFA.live_coding2]
even_ind [in PRFA.live_coding2]
F
fast_rev [in PRFA.live_coding2]I
iter [in PRFA.live_coding2]L
LEM [in PRFA.tp1c]le_sind [in PRFA.live_coding2]
le_ind [in PRFA.live_coding2]
M
min [in PRFA.tp1c]P
PL [in PRFA.tp1c]R
REPLACE_ME [in PRFA.tp1c]rtclos_sind [in PRFA.live_coding2]
rtclos_ind [in PRFA.live_coding2]
T
theDNS [in PRFA.tp1c]theLEM [in PRFA.tp1c]
thePL [in PRFA.tp1c]
U
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]
| 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 | (194 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 | (2 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 | (7 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 | (3 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 | (83 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 | (19 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 | (10 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 | (3 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 | (67 entries) |
This page has been generated by coqdoc