| 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 | (413 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 | (7 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 | (1 entry) |
| 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 | (25 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 | (4 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 | (203 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 | (35 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) |
| 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 | (6 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 | (15 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 | (34 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 | (72 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 | (1 entry) |
Global Index
A
andlist [definition, in PropL]andlistEq [lemma, in PropL]
and_dec [instance, in Base]
app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]
app_red_proper [instance, in unif]
assn [definition, in PropL]
B
bad_eqn [lemma, in unif]Base [library]
bent [definition, in ctab]
bent_iff_unsat [lemma, in ctab]
bool_eq_dec [instance, in Base]
bsc [definition, in PropL]
C
card [definition, in Base]Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_ex [lemma, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
card_not_in_rem [lemma, in Base]
card_in_rem [lemma, in Base]
cent [definition, in ctab]
cent_solved_sat [lemma, in ctab]
cent_sat [lemma, in ctab]
cent_weak [lemma, in ctab]
CharFal [definition, in PropL]
CharImp [definition, in PropL]
clause [definition, in ctab]
Consistency [definition, in PropL]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
cons_red_proper [instance, in unif]
context [definition, in PropL]
ctab [library]
Cut [definition, in PropL]
D
dec [definition, in Base]decider [definition, in ctab]
decision [definition, in Base]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
disjoint [definition, in Base]
disjoint_app [lemma, in Base]
disjoint_cons [lemma, in Base]
disjoint_nil' [lemma, in Base]
disjoint_nil [lemma, in Base]
disjoint_incl [lemma, in Base]
disjoint_symm [lemma, in Base]
disjoint_forall [lemma, in Base]
DM_exists [lemma, in Base]
DM_or [lemma, in Base]
dom [definition, in unif]
dom_varl [lemma, in unif]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
dupfreeN [constructor, in Base]
dupfree_inv [definition, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_card [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_cons [lemma, in Base]
Dupfree.X [variable, in Base]
E
EntailRelAllProps [definition, in PropL]eqn [definition, in unif]
Equi [section, in Base]
equi [definition, in Base]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
equi_red [instance, in unif]
Equi.X [variable, in Base]
eval [definition, in ctab]
F
F [section, in PropL]Fal [constructor, in PropL]
False_dec [instance, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_fst [lemma, in Base]
filter_app [lemma, in Base]
filter_id [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
FK [definition, in PropL]
form [inductive, in PropL]
form_eq_dec [instance, in PropL]
FP [definition, in Base]
FS [definition, in PropL]
F.E [variable, in PropL]
F.F [variable, in PropL]
G
Glivenko [lemma, in PropL]Glivenko_refute [lemma, in PropL]
H
hil [inductive, in PropL]hilA [constructor, in PropL]
hilAK [lemma, in PropL]
hilAS [lemma, in PropL]
hilD [lemma, in PropL]
hilE [constructor, in PropL]
hilI [lemma, in PropL]
hilK [constructor, in PropL]
hilMP [constructor, in PropL]
hilS [constructor, in PropL]
hil_iff_nd [lemma, in PropL]
hil_nd [lemma, in PropL]
I
idempotent [definition, in unif]iff_dec [instance, in Base]
Imp [constructor, in PropL]
impl_dec [instance, in Base]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_equi_proper [instance, in Base]
incl_preorder [instance, in Base]
incl_app_left [lemma, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_sing [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_incl_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
it [definition, in Base]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
it_fp [lemma, in Base]
it_ind [lemma, in Base]
L
list_cc [lemma, in Base]list_exists_not_incl [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
M
Membership [section, in Base]Membership.X [variable, in Base]
Monotonicity [definition, in PropL]
N
nat_le_dec [instance, in Base]nat_eq_dec [instance, in Base]
nd [inductive, in PropL]
ndA [constructor, in PropL]
ndapp [lemma, in PropL]
ndapp1 [lemma, in PropL]
ndapp2 [lemma, in PropL]
ndapp3 [lemma, in PropL]
ndc [inductive, in PropL]
ndcA [constructor, in PropL]
ndcC [constructor, in PropL]
ndcE [lemma, in PropL]
ndcIE [constructor, in PropL]
ndcII [constructor, in PropL]
ndcW [lemma, in PropL]
ndc_refute [lemma, in PropL]
ndc_weak [lemma, in PropL]
ndc_iff_sem [lemma, in ctab]
ndc_dec [lemma, in ctab]
ndc_bent [lemma, in ctab]
ndDN [lemma, in PropL]
ndE [constructor, in PropL]
ndIE [constructor, in PropL]
ndIE_weak [lemma, in PropL]
ndII [constructor, in PropL]
ndW [lemma, in PropL]
nd_hil [lemma, in PropL]
nd_embeds_ndc [lemma, in PropL]
nd_ndc [lemma, in PropL]
nd_subst [lemma, in PropL]
nd_con [lemma, in PropL]
nd_bool_sound [lemma, in PropL]
nd_weak [lemma, in PropL]
Neg [constructor, in ctab]
Not [definition, in PropL]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
O
or_dec [instance, in Base]P
phi [definition, in unif]phi [definition, in ctab]
phi_principal [lemma, in unif]
phi_unif [lemma, in unif]
phi_id [lemma, in unif]
phi_subst [lemma, in unif]
Pos [constructor, in ctab]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
pre [definition, in unif]
presolved [inductive, in unif]
presolvedC [constructor, in unif]
presolvedN [constructor, in unif]
presolved_app [lemma, in unif]
pre_presolved [lemma, in unif]
pre_red [lemma, in unif]
pre' [definition, in unif]
pre'_presolved [lemma, in unif]
pre'_red [lemma, in unif]
principal_unifier_exists [lemma, in unif]
principal_idempotent [lemma, in unif]
principal_unifier [definition, in unif]
PropL [library]
provider [definition, in ctab]
R
rec [inductive, in ctab]recNF [constructor, in ctab]
recNI [constructor, in ctab]
recNil [constructor, in ctab]
recNV [constructor, in ctab]
recNV' [constructor, in ctab]
recPF [constructor, in ctab]
recPI [constructor, in ctab]
recPV [constructor, in ctab]
recPV' [constructor, in ctab]
red [definition, in unif]
red_repl [lemma, in unif]
red_decompose [lemma, in unif]
red_swap [lemma, in unif]
red_delete [lemma, in unif]
red_preorder [instance, in unif]
Reflexivity [definition, in PropL]
refutation [lemma, in ctab]
ref_dec [lemma, in ctab]
ref_iff_unsat [lemma, in ctab]
ref_ndc [lemma, in ctab]
ref_unsat [lemma, in ctab]
ref_sound [projection, in ctab]
ref_neg_imp [projection, in ctab]
ref_pos_imp [projection, in ctab]
ref_clash [projection, in ctab]
ref_weak [projection, in ctab]
ref_Fal [projection, in ctab]
ref_pred [record, in ctab]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_inclr [lemma, in Base]
rem_reorder [lemma, in Base]
rem_id [lemma, in Base]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_comm [lemma, in Base]
rem_equi [lemma, in Base]
rem_app' [lemma, in Base]
rem_app [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_cons' [lemma, in Base]
rem_cons [lemma, in Base]
rem_mono [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
rep [definition, in Base]
rep [definition, in unif]
repe [definition, in unif]
repl [definition, in unif]
repl_ueq [lemma, in unif]
repl_unif [lemma, in unif]
repl_var_elim [lemma, in unif]
repl_var [lemma, in unif]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
rep_var_not_in [lemma, in unif]
rep_var [lemma, in unif]
rep_id_subst [lemma, in unif]
rep_id [lemma, in unif]
rep_xx [lemma, in unif]
RL [section, in ctab]
RL.Rho [variable, in ctab]
RL.rho [variable, in ctab]
S
sat [definition, in ctab]satis [definition, in PropL]
satis [definition, in ctab]
satis_dec [instance, in PropL]
satis_pos [lemma, in ctab]
satis_weak [lemma, in ctab]
satis_in [lemma, in ctab]
satis_iff [lemma, in ctab]
satis_neg_imp [lemma, in ctab]
satis_pos_imp [lemma, in ctab]
satis_dec [instance, in ctab]
satis_eval [lemma, in ctab]
satis' [definition, in ctab]
sat_weak [lemma, in ctab]
sform [inductive, in ctab]
sform_eq_dec [instance, in ctab]
size [definition, in unif]
size [definition, in ctab]
sizeF [definition, in ctab]
size_recursion [lemma, in Base]
solve [definition, in unif]
solved [inductive, in unif]
solved [definition, in ctab]
solvedC [constructor, in unif]
solvedN [constructor, in unif]
solved_form_exists [lemma, in unif]
solved_principal [lemma, in unif]
solved_ref [lemma, in ctab]
solved_neg_var [lemma, in ctab]
solved_pos_var [lemma, in ctab]
solved_nil [lemma, in ctab]
solved_sat [lemma, in ctab]
solved_phi [lemma, in ctab]
solveN [definition, in unif]
solveN_correct [lemma, in unif]
solve_correct [lemma, in unif]
subst [definition, in PropL]
subst [definition, in unif]
Substitution [definition, in PropL]
subst_size [lemma, in unif]
subst_id [lemma, in unif]
svar [definition, in ctab]
T
T [constructor, in unif]ter [inductive, in unif]
ter_eq_dec [instance, in unif]
True_dec [instance, in Base]
U
ueq [definition, in unif]ueq_principal_unifier [lemma, in unif]
ueq_sym [lemma, in unif]
undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_id [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_id_equi [lemma, in Base]
Undup.X [variable, in Base]
unif [definition, in unif]
unif [library]
unifiable [definition, in unif]
unif_red_proper [instance, in unif]
unif_app [lemma, in unif]
unif_cons [lemma, in unif]
uns [definition, in ctab]
uns_pos [lemma, in ctab]
V
V [constructor, in unif]valid [definition, in ctab]
valid_unsat [lemma, in ctab]
Var [constructor, in PropL]
var [definition, in PropL]
var [definition, in unif]
varl [definition, in unif]
varl_incl [lemma, in unif]
varl_app [lemma, in unif]
vars [definition, in PropL]
vart [definition, in unif]
vart_incl_varl [lemma, in unif]
other
_ === _ [notation, in Base]_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
+ _ [notation, in ctab]
- _ [notation, in ctab]
| _ | [notation, in Base]
Notation Index
other
_ === _ [in Base]_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
+ _ [in ctab]
- _ [in ctab]
| _ | [in Base]
Module Index
F
FCI [in Base]Variable Index
C
Cardinality.X [in Base]D
Dupfree.X [in Base]E
Equi.X [in Base]F
FCI.FCI.step [in Base]FCI.FCI.V [in Base]
FCI.FCI.X [in Base]
FilterComm.p [in Base]
FilterComm.q [in Base]
FilterComm.X [in Base]
FilterLemmas_pq.q [in Base]
FilterLemmas_pq.p [in Base]
FilterLemmas_pq.X [in Base]
FilterLemmas.p [in Base]
FilterLemmas.X [in Base]
F.E [in PropL]
F.F [in PropL]
I
Inclusion.X [in Base]Iteration.f [in Base]
Iteration.X [in Base]
M
Membership.X [in Base]P
PowerRep.X [in Base]R
Removal.X [in Base]RL.Rho [in ctab]
RL.rho [in ctab]
U
Undup.X [in Base]Library Index
B
BaseC
ctabP
PropLU
unifLemma Index
A
andlistEq [in PropL]B
bad_eqn [in unif]bent_iff_unsat [in ctab]
C
card_or [in Base]card_lt [in Base]
card_equi [in Base]
card_ex [in Base]
card_0 [in Base]
card_cons_rem [in Base]
card_eq [in Base]
card_le [in Base]
card_not_in_rem [in Base]
card_in_rem [in Base]
cent_solved_sat [in ctab]
cent_sat [in ctab]
cent_weak [in ctab]
D
dec_prop_iff [in Base]dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
disjoint_app [in Base]
disjoint_cons [in Base]
disjoint_nil' [in Base]
disjoint_nil [in Base]
disjoint_incl [in Base]
disjoint_symm [in Base]
disjoint_forall [in Base]
DM_exists [in Base]
DM_or [in Base]
dom_varl [in unif]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_undup [in Base]
dupfree_card [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_cons [in Base]
E
equi_rotate [in Base]equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
F
FCI.closure [in Base]FCI.fp [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
filter_comm [in Base]
filter_and [in Base]
filter_pq_eq [in Base]
filter_pq_mono [in Base]
filter_fst' [in Base]
filter_fst [in Base]
filter_app [in Base]
filter_id [in Base]
filter_mono [in Base]
filter_incl [in Base]
G
Glivenko [in PropL]Glivenko_refute [in PropL]
H
hilAK [in PropL]hilAS [in PropL]
hilD [in PropL]
hilI [in PropL]
hil_iff_nd [in PropL]
hil_nd [in PropL]
I
incl_app_left [in Base]incl_lrcons [in Base]
incl_rcons [in Base]
incl_sing [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
it_fp [in Base]
it_ind [in Base]
L
list_cc [in Base]list_exists_not_incl [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
N
ndapp [in PropL]ndapp1 [in PropL]
ndapp2 [in PropL]
ndapp3 [in PropL]
ndcE [in PropL]
ndcW [in PropL]
ndc_refute [in PropL]
ndc_weak [in PropL]
ndc_iff_sem [in ctab]
ndc_dec [in ctab]
ndc_bent [in ctab]
ndDN [in PropL]
ndIE_weak [in PropL]
ndW [in PropL]
nd_hil [in PropL]
nd_embeds_ndc [in PropL]
nd_ndc [in PropL]
nd_subst [in PropL]
nd_con [in PropL]
nd_bool_sound [in PropL]
nd_weak [in PropL]
not_in_cons [in Base]
P
phi_principal [in unif]phi_unif [in unif]
phi_id [in unif]
phi_subst [in unif]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
presolved_app [in unif]
pre_presolved [in unif]
pre_red [in unif]
pre'_presolved [in unif]
pre'_red [in unif]
principal_unifier_exists [in unif]
principal_idempotent [in unif]
R
red_repl [in unif]red_decompose [in unif]
red_swap [in unif]
red_delete [in unif]
refutation [in ctab]
ref_dec [in ctab]
ref_iff_unsat [in ctab]
ref_ndc [in ctab]
ref_unsat [in ctab]
rem_inclr [in Base]
rem_reorder [in Base]
rem_id [in Base]
rem_fst' [in Base]
rem_fst [in Base]
rem_comm [in Base]
rem_equi [in Base]
rem_app' [in Base]
rem_app [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_cons' [in Base]
rem_cons [in Base]
rem_mono [in Base]
rem_incl [in Base]
rem_not_in [in Base]
repl_ueq [in unif]
repl_unif [in unif]
repl_var_elim [in unif]
repl_var [in unif]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]
rep_var_not_in [in unif]
rep_var [in unif]
rep_id_subst [in unif]
rep_id [in unif]
rep_xx [in unif]
S
satis_pos [in ctab]satis_weak [in ctab]
satis_in [in ctab]
satis_iff [in ctab]
satis_neg_imp [in ctab]
satis_pos_imp [in ctab]
satis_eval [in ctab]
sat_weak [in ctab]
size_recursion [in Base]
solved_form_exists [in unif]
solved_principal [in unif]
solved_ref [in ctab]
solved_neg_var [in ctab]
solved_pos_var [in ctab]
solved_nil [in ctab]
solved_sat [in ctab]
solved_phi [in ctab]
solveN_correct [in unif]
solve_correct [in unif]
subst_size [in unif]
subst_id [in unif]
U
ueq_principal_unifier [in unif]ueq_sym [in unif]
undup_idempotent [in Base]
undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
unif_app [in unif]
unif_cons [in unif]
uns_pos [in ctab]
V
valid_unsat [in ctab]varl_incl [in unif]
varl_app [in unif]
vart_incl_varl [in unif]
Constructor Index
D
dupfreeC [in Base]dupfreeN [in Base]
F
Fal [in PropL]H
hilA [in PropL]hilE [in PropL]
hilK [in PropL]
hilMP [in PropL]
hilS [in PropL]
I
Imp [in PropL]N
ndA [in PropL]ndcA [in PropL]
ndcC [in PropL]
ndcIE [in PropL]
ndcII [in PropL]
ndE [in PropL]
ndIE [in PropL]
ndII [in PropL]
Neg [in ctab]
P
Pos [in ctab]presolvedC [in unif]
presolvedN [in unif]
R
recNF [in ctab]recNI [in ctab]
recNil [in ctab]
recNV [in ctab]
recNV' [in ctab]
recPF [in ctab]
recPI [in ctab]
recPV [in ctab]
recPV' [in ctab]
S
solvedC [in unif]solvedN [in unif]
T
T [in unif]V
V [in unif]Var [in PropL]
Inductive Index
D
dupfree [in Base]F
form [in PropL]H
hil [in PropL]N
nd [in PropL]ndc [in PropL]
P
presolved [in unif]R
rec [in ctab]S
sform [in ctab]solved [in unif]
T
ter [in unif]Projection Index
R
ref_sound [in ctab]ref_neg_imp [in ctab]
ref_pos_imp [in ctab]
ref_clash [in ctab]
ref_weak [in ctab]
ref_Fal [in ctab]
Section Index
C
Cardinality [in Base]D
Dupfree [in Base]E
Equi [in Base]F
F [in PropL]FCI.FCI [in Base]
FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
I
Inclusion [in Base]Iteration [in Base]
M
Membership [in Base]P
PowerRep [in Base]R
Removal [in Base]RL [in ctab]
U
Undup [in Base]Instance Index
A
and_dec [in Base]app_equi_proper [in Base]
app_incl_proper [in Base]
app_red_proper [in unif]
B
bool_eq_dec [in Base]C
card_equi_proper [in Base]cons_equi_proper [in Base]
cons_incl_proper [in Base]
cons_red_proper [in unif]
E
equi_Equivalence [in Base]equi_red [in unif]
F
False_dec [in Base]form_eq_dec [in PropL]
I
iff_dec [in Base]impl_dec [in Base]
incl_equi_proper [in Base]
incl_preorder [in Base]
in_equi_proper [in Base]
in_incl_proper [in Base]
L
list_exists_dec [in Base]list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]
N
nat_le_dec [in Base]nat_eq_dec [in Base]
not_dec [in Base]
O
or_dec [in Base]R
red_preorder [in unif]S
satis_dec [in PropL]satis_dec [in ctab]
sform_eq_dec [in ctab]
T
ter_eq_dec [in unif]True_dec [in Base]
U
unif_red_proper [in unif]Definition Index
A
andlist [in PropL]assn [in PropL]
B
bent [in ctab]bsc [in PropL]
C
card [in Base]cent [in ctab]
CharFal [in PropL]
CharImp [in PropL]
clause [in ctab]
Consistency [in PropL]
context [in PropL]
Cut [in PropL]
D
dec [in Base]decider [in ctab]
decision [in Base]
disjoint [in Base]
dom [in unif]
dupfree_inv [in Base]
E
EntailRelAllProps [in PropL]eqn [in unif]
equi [in Base]
eval [in ctab]
F
FCI.C [in Base]FCI.F [in Base]
filter [in Base]
FK [in PropL]
FP [in Base]
FS [in PropL]
I
idempotent [in unif]inclp [in Base]
it [in Base]
M
Monotonicity [in PropL]N
Not [in PropL]P
phi [in unif]phi [in ctab]
power [in Base]
pre [in unif]
pre' [in unif]
principal_unifier [in unif]
provider [in ctab]
R
red [in unif]Reflexivity [in PropL]
rem [in Base]
rep [in Base]
rep [in unif]
repe [in unif]
repl [in unif]
S
sat [in ctab]satis [in PropL]
satis [in ctab]
satis' [in ctab]
size [in unif]
size [in ctab]
sizeF [in ctab]
solve [in unif]
solved [in ctab]
solveN [in unif]
subst [in PropL]
subst [in unif]
Substitution [in PropL]
svar [in ctab]
U
ueq [in unif]undup [in Base]
unif [in unif]
unifiable [in unif]
uns [in ctab]
V
valid [in ctab]var [in PropL]
var [in unif]
varl [in unif]
vars [in PropL]
vart [in unif]
Record Index
R
ref_pred [in ctab]| 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 | (413 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 | (7 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 | (1 entry) |
| 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 | (25 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 | (4 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 | (203 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 | (35 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) |
| 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 | (6 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 | (15 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 | (34 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 | (72 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 | (1 entry) |
This page has been generated by coqdoc