| 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 | (876 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 | (2 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 | (108 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 | (5 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 | (381 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 | (53 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 | (42 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 | (8 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 | (49 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 | (43 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 | (173 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 | (5 entries) |
Global Index
A
And [constructor, in PropiL]AndFree [definition, in PropiL]
and_dec [instance, in Base]
app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]
B
base [definition, in PropiLFmodel]Base [library]
baseKD [definition, in PropiLFmodel]
baseKD_complete [lemma, in PropiLFmodel]
baseKD_sound [lemma, in PropiLFmodel]
baseKD_in [lemma, in PropiLFmodel]
baseVars [definition, in PropiLFmodel]
baseVars_in [lemma, in PropiLFmodel]
baseVars_incl [lemma, in PropiLFmodel]
Binter [definition, in PropiLFmodel]
Binter_sound [lemma, in PropiLFmodel]
bool_eq_dec [instance, in Base]
bot [projection, in PropiLmodel]
bot [projection, in PropiLmodel]
bot1 [projection, in PropiLmodel]
bot1 [projection, in PropiLmodel]
Bunion [definition, in PropiLFmodel]
Bunion_sound [lemma, in PropiLFmodel]
b2s [definition, in PropiL]
C
CanonicalDemo [section, in PropiLFmodel2]CanonicalDemo.sscU [variable, in PropiLFmodel2]
CanonicalDemo.U [variable, in PropiLFmodel2]
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]
CD [definition, in PropiLFmodel2]
CD_demo [lemma, in PropiLFmodel2]
CharAnd [definition, in PropiL]
CharFal [definition, in PropiL]
CharImp [definition, in PropiL]
CharOr [definition, in PropiL]
clause [definition, in PropiL]
clauseCD [definition, in PropiLFmodel2]
compactCD_restore [definition, in PropiLFmodel2]
compactCD_restore [definition, in PropiLFmodel2]
compactDemo [definition, in PropiLFmodel2]
compactDemo [definition, in PropiLFmodel2]
compact_restore_demo [lemma, in PropiLFmodel2]
compact_CD_equi [lemma, in PropiLFmodel2]
compact_sound [lemma, in PropiLFmodel2]
compact_cons [lemma, in PropiLFmodel2]
compact_CD [definition, in PropiLFmodel2]
compact_restore_demo [lemma, in PropiLFmodel2]
compact_CD_equi [lemma, in PropiLFmodel2]
compact_sound [lemma, in PropiLFmodel2]
compact_cons [lemma, in PropiLFmodel2]
compact_CD [definition, in PropiLFmodel2]
cons [definition, in PropiLFmodel]
Cons [definition, in PropiLFmodel2]
Consistency [definition, in PropiL]
consW [lemma, in PropiLFmodel]
cons_dec [instance, in PropiLFmodel]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
Cons_mono [lemma, in PropiLFmodel2]
Cons_dec [instance, in PropiLFmodel2]
context [definition, in PropiL]
CounterModels [section, in PropiLFmodel]
CounterModels.K1 [variable, in PropiLFmodel]
CounterModels.K2 [variable, in PropiLFmodel]
CounterModels.K3 [variable, in PropiLFmodel]
CounterModels.K4 [variable, in PropiLFmodel]
Cut [definition, in PropiL]
CVars [definition, in PropiLFmodel]
CVars_correct [lemma, in PropiLFmodel]
c2f [definition, in PropiL]
C2PC [definition, in PropiLFmodel]
D
dec [definition, in Base]Decidability [section, in PropiL]
Decidability.A0 [variable, in PropiL]
Decidability.s0 [variable, in PropiL]
decision [definition, in Base]
dec_ucsPred [lemma, in PropiLFmodel]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
Demo [definition, in PropiLFmodel]
Demo [section, in PropiLFmodel]
DemoFiniteKripke [section, in PropiLFmodel2]
DemoKBase [section, in PropiLFmodel]
DemoSat [lemma, in PropiLFmodel2]
DemoSatisAll [lemma, in PropiLFmodel2]
Demo_equi [lemma, in PropiLFmodel]
demo_extension [lemma, in PropiLFmodel2]
depth [definition, in PropiL]
dequi [definition, in PropiLFmodel]
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]
dsub [definition, in PropiLFmodel]
Dupfree [section, in Base]
dupfree [inductive, in Base]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
dupfreeC [constructor, in Base]
dupfreeN [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_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]
Dupfree.X [variable, in Base]
D2FKM [definition, in PropiLFmodel2]
E
EntailmentRelationProperties [section, in PropiL]EntailmentRelationProperties.E [variable, in PropiL]
EntailmentRelationProperties.F [variable, in PropiL]
EntailRelAllProps [definition, in PropiL]
EntailRelAllProps_ext [lemma, in PropiL]
eqH [definition, in PropiLmodel]
eqH [definition, in PropiLmodel]
Equi [definition, in PropiL]
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.X [variable, in Base]
eq_decW [projection, in PropiLFmodel]
evalFK [definition, in PropiLFmodel]
evalFK_OrAR [lemma, in PropiLFmodel]
evalFK_mono [lemma, in PropiLFmodel]
evalH [definition, in PropiLmodel]
evalH [definition, in PropiLmodel]
evalHf [lemma, in PropiLmodel]
evalHf [lemma, in PropiLmodel]
evalH' [definition, in PropiLmodel]
evalH' [definition, in PropiLmodel]
evalK [definition, in PropiLmodel]
evalK [definition, in PropiLmodel]
evalKA [definition, in PropiLmodel]
evalKA [definition, in PropiLmodel]
evalK_evalH_agree [lemma, in PropiLmodel]
evalK_mono [lemma, in PropiLmodel]
evalK_evalH_agree [lemma, in PropiLmodel]
evalK_mono [lemma, in PropiLmodel]
evalTK [definition, in PropiLFmodel]
evalTK' [definition, in PropiLFmodel]
extension [lemma, in PropiLFmodel2]
F
Fal [constructor, in PropiL]FalFree [definition, in PropiL]
False_dec [instance, in Base]
FCI [module, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [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_idempotent [lemma, in PropiLFmodel]
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]
filter_equi [lemma, in PropiLFmodel2]
FImp [definition, in PropiLFmodel]
FImpList [definition, in PropiLFmodel]
FImpList_in [lemma, in PropiLFmodel]
FImpList_ind [lemma, in PropiLFmodel]
FImpList_closure [lemma, in PropiLFmodel]
FImp_in4 [lemma, in PropiLFmodel]
FImp_in3 [lemma, in PropiLFmodel]
FImp_in2 [lemma, in PropiLFmodel]
FImp_in1 [lemma, in PropiLFmodel]
FImp_greatest [lemma, in PropiLFmodel]
FImp_Heyting [lemma, in PropiLFmodel]
FiniteClosure [section, in PropiLFmodel]
FiniteClosure.F [variable, in PropiLFmodel]
FiniteClosure.FE [variable, in PropiLFmodel]
FiniteClosure.FS [variable, in PropiLFmodel]
FiniteClosure.UCSFilter [variable, in PropiLFmodel]
FiniteKripke [section, in PropiLFmodel]
FiniteKripkeModel [record, in PropiLFmodel]
FiniteKripke.FKM [variable, in PropiLFmodel]
FiniteKripke.interp [variable, in PropiLFmodel]
FiniteKripke.pW [variable, in PropiLFmodel]
FiniteKripke.W [variable, in PropiLFmodel]
FiniteKripke.WR [variable, in PropiLFmodel]
FiniteKripke.WRref [variable, in PropiLFmodel]
FiniteKripke.WRtra [variable, in PropiLFmodel]
FK [definition, in PropiL]
FKImp [definition, in PropiLFmodel]
FKImp_in [lemma, in PropiLFmodel]
FKImp_ind [lemma, in PropiLFmodel]
FKImp_closure [lemma, in PropiLFmodel]
FK2K [definition, in PropiLFmodel]
form [inductive, in PropiL]
FormHA [definition, in PropiLmodel]
FormHA [definition, in PropiLmodel]
FormHeytingAlgebra [section, in PropiLmodel]
FormHeytingAlgebra [section, in PropiLmodel]
FormHeytingAlgebra.bot [variable, in PropiLmodel]
FormHeytingAlgebra.bot [variable, in PropiLmodel]
FormHeytingAlgebra.H [variable, in PropiLmodel]
FormHeytingAlgebra.H [variable, in PropiLmodel]
FormHeytingAlgebra.imp [variable, in PropiLmodel]
FormHeytingAlgebra.imp [variable, in PropiLmodel]
FormHeytingAlgebra.join [variable, in PropiLmodel]
FormHeytingAlgebra.join [variable, in PropiLmodel]
FormHeytingAlgebra.meet [variable, in PropiLmodel]
FormHeytingAlgebra.meet [variable, in PropiLmodel]
FormHeytingAlgebra.R [variable, in PropiLmodel]
FormHeytingAlgebra.R [variable, in PropiLmodel]
form_eq_dec [instance, in PropiL]
FP [definition, in Base]
FS [definition, in PropiL]
G
Gamma [definition, in PropiL]gen [inductive, in PropiL]
genA [lemma, in PropiL]
genAL [constructor, in PropiL]
genAR [constructor, in PropiL]
genCW [lemma, in PropiL]
genF [constructor, in PropiL]
genIL [constructor, in PropiL]
genIR [constructor, in PropiL]
genOL [constructor, in PropiL]
genOR1 [constructor, in PropiL]
genOR2 [constructor, in PropiL]
genV [constructor, in PropiL]
genW [lemma, in PropiL]
gen_DN [lemma, in PropiL]
gen_DN' [lemma, in PropiL]
gen_lambda [lemma, in PropiL]
gen_iff_tab [lemma, in PropiL]
gen_tab [lemma, in PropiL]
gen_iff_nd [lemma, in PropiL]
gen_nd [lemma, in PropiL]
gen_NoNVar [lemma, in PropiL]
gen_NoVar [lemma, in PropiL]
gen_EntailRelation [lemma, in PropiL]
gen_subst [lemma, in PropiL]
gen_or [lemma, in PropiL]
gen_and_both [lemma, in PropiL]
gen_and [lemma, in PropiL]
gen_fal [lemma, in PropiL]
gen_imp [lemma, in PropiL]
gen_cons [lemma, in PropiL]
gen_NoFal [lemma, in PropiL]
gen_cut [lemma, in PropiL]
gen_GCut [lemma, in PropiL]
gen_mono [lemma, in PropiL]
goal [definition, in PropiL]
goal_eq_dec [instance, in PropiL]
H
H [projection, in PropiLmodel]H [projection, in PropiLmodel]
HAequiv [lemma, in PropiLmodel]
HAequiv [lemma, in PropiLmodel]
HAProperty [section, in PropiLmodel]
HAProperty [section, in PropiLmodel]
HAProperty.HA [variable, in PropiLmodel]
HAProperty.HA [variable, in PropiLmodel]
HASound [section, in PropiLmodel]
HASound [section, in PropiLmodel]
HASound.HA [variable, in PropiLmodel]
HASound.HA [variable, in PropiLmodel]
HASound.interp [variable, in PropiLmodel]
HASound.interp [variable, in PropiLmodel]
HA_iff_nd [lemma, in PropiLmodel]
HA_nd [lemma, in PropiLmodel]
HA_iff_nd [lemma, in PropiLmodel]
HA_nd [lemma, in PropiLmodel]
hent [definition, in PropiLmodel]
hent [definition, in PropiLmodel]
hent_imp [lemma, in PropiLmodel]
hent_imp [lemma, in PropiLmodel]
HeytingAlgebra [record, in PropiLmodel]
HeytingAlgebra [record, in PropiLmodel]
hil [inductive, in PropiL]
hilA [constructor, in PropiL]
hilAI [constructor, in PropiL]
hilAK [lemma, in PropiL]
hilAL [constructor, in PropiL]
hilAR [constructor, in PropiL]
hilAS [lemma, in PropiL]
hilD [lemma, in PropiL]
hilE [constructor, in PropiL]
hilI [lemma, in PropiL]
hilK [constructor, in PropiL]
hilMP [constructor, in PropiL]
hilOE [constructor, in PropiL]
hilOL [constructor, in PropiL]
hilOR [constructor, in PropiL]
hilS [constructor, in PropiL]
hil_iff_nd [lemma, in PropiL]
hil_nd [lemma, in PropiL]
Hintikka [definition, in PropiLFmodel]
Hintikka_dec [instance, in PropiLFmodel]
Hintikka_equi [lemma, in PropiLFmodel]
I
iff_dec [instance, in Base]imp [projection, in PropiLmodel]
imp [projection, in PropiLmodel]
Imp [constructor, in PropiL]
ImpFree [definition, in PropiL]
impl_dec [instance, in Base]
imp1 [projection, in PropiLmodel]
imp1 [projection, in PropiLmodel]
imp2 [lemma, in PropiLmodel]
imp2 [lemma, in PropiLmodel]
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]
inter [definition, in PropiLFmodel]
interp [projection, in PropiLmodel]
interp [projection, in PropiLmodel]
interp [projection, in PropiLFmodel]
interpTK [definition, in PropiLFmodel]
inter_sub [lemma, in PropiLFmodel]
inter_sound [lemma, in PropiLFmodel]
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]
in_map_informative [lemma, in PropiLFmodel2]
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]
J
join [projection, in PropiLmodel]join [projection, in PropiLmodel]
join_com [lemma, in PropiLmodel]
join_com [lemma, in PropiLmodel]
join1 [projection, in PropiLmodel]
join1 [projection, in PropiLmodel]
join2 [lemma, in PropiLmodel]
join2 [lemma, in PropiLmodel]
join3 [lemma, in PropiLmodel]
join3 [lemma, in PropiLmodel]
K
KripkeModel [record, in PropiLmodel]KripkeModel [record, in PropiLmodel]
KripkeSemantics [section, in PropiLmodel]
KripkeSemantics [section, in PropiLmodel]
KripkeSemantics.KM [variable, in PropiLmodel]
KripkeSemantics.KM [variable, in PropiLmodel]
kripke_nd [lemma, in PropiLFmodel2]
Kripke2Heyting [section, in PropiLmodel]
Kripke2Heyting [section, in PropiLmodel]
Kripke2Heyting.bot [variable, in PropiLmodel]
Kripke2Heyting.bot [variable, in PropiLmodel]
Kripke2Heyting.H [variable, in PropiLmodel]
Kripke2Heyting.H [variable, in PropiLmodel]
Kripke2Heyting.imp [variable, in PropiLmodel]
Kripke2Heyting.imp [variable, in PropiLmodel]
Kripke2Heyting.join [variable, in PropiLmodel]
Kripke2Heyting.join [variable, in PropiLmodel]
Kripke2Heyting.KM [variable, in PropiLmodel]
Kripke2Heyting.KM [variable, in PropiLmodel]
Kripke2Heyting.meet [variable, in PropiLmodel]
Kripke2Heyting.meet [variable, in PropiLmodel]
Kripke2Heyting.R [variable, in PropiLmodel]
Kripke2Heyting.R [variable, in PropiLmodel]
Kripke2Heyting.UC [variable, in PropiLmodel]
Kripke2Heyting.UC [variable, in PropiLmodel]
Kripke2Heyting.UCS [variable, in PropiLmodel]
Kripke2Heyting.UCS [variable, in PropiLmodel]
K_Peirce [definition, in PropiLFmodel]
K_DN [definition, in PropiLFmodel]
K_XM [definition, in PropiLFmodel]
K_neg [definition, in PropiLFmodel]
K_orxy [definition, in PropiLFmodel]
K_var [definition, in PropiLFmodel]
K_Fal [definition, in PropiLFmodel]
K2H [definition, in PropiLmodel]
K2H [definition, in PropiLmodel]
K2Hinterp [definition, in PropiLmodel]
K2Hinterp [definition, in PropiLmodel]
L
Lambda [definition, in PropiL]lambda_gen [lemma, in PropiL]
lambda_ind [lemma, in PropiL]
lambda_closure [lemma, in PropiL]
lfpTab [definition, in PropiLFmodel]
lfpTab_ind [lemma, in PropiLFmodel]
lfpTab_closure [lemma, in PropiLFmodel]
lfp_tab [lemma, in PropiLFmodel]
ListOperation [section, in PropiLFmodel]
ListOperation.X [variable, in PropiLFmodel]
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]
ltr [definition, in PropiLmodel]
ltr [definition, in PropiLmodel]
ltr_CharImp [lemma, in PropiLmodel]
ltr_CharImp [lemma, in PropiLmodel]
M
maxCons_PartialOrder [lemma, in PropiLFmodel2]maxCons_ParOrd [lemma, in PropiLFmodel2]
maxCons_equi [lemma, in PropiLFmodel2]
maxCons_incl [lemma, in PropiLFmodel2]
maxCons_equi_Fal [lemma, in PropiLFmodel2]
maxCons_PartialOrder [lemma, in PropiLFmodel2]
maxCons_ParOrd [lemma, in PropiLFmodel2]
maxCons_equi [lemma, in PropiLFmodel2]
maxCons_incl [lemma, in PropiLFmodel2]
maxCons_equi_Fal [lemma, in PropiLFmodel2]
maxCons_equi_vars [lemma, in PropiLFmodel2]
maxCons_XM [lemma, in PropiLFmodel2]
maxext [definition, in PropiLFmodel2]
maxExtension [lemma, in PropiLFmodel2]
maxext_samebase [lemma, in PropiLFmodel2]
maxext_samebase [lemma, in PropiLFmodel2]
maxext_nomore [lemma, in PropiLFmodel2]
MaximalExtension [section, in PropiLFmodel2]
MaximalExtension.p [variable, in PropiLFmodel2]
MaximalExtension.p_mono [variable, in PropiLFmodel2]
MaximalExtension.U [variable, in PropiLFmodel2]
MaximalExtension.X [variable, in PropiLFmodel2]
MaximalIdentity [section, in PropiLFmodel2]
MaximalIdentity.sclU [variable, in PropiLFmodel2]
MaximalIdentity.SFL [variable, in PropiLFmodel2]
MaximalIdentity.SFL [variable, in PropiLFmodel2]
MaximalIdentity.U [variable, in PropiLFmodel2]
meet [projection, in PropiLmodel]
meet [projection, in PropiLmodel]
meet_com [lemma, in PropiLmodel]
meet_com [lemma, in PropiLmodel]
meet1 [projection, in PropiLmodel]
meet1 [projection, in PropiLmodel]
meet2 [lemma, in PropiLmodel]
meet2 [lemma, in PropiLmodel]
meet3 [lemma, in PropiLmodel]
meet3 [lemma, in PropiLmodel]
Membership [section, in Base]
Membership.X [variable, in Base]
mkFiniteKripkeModel [constructor, in PropiLFmodel]
mkHeytingAlgebra [constructor, in PropiLmodel]
mkHeytingAlgebra [constructor, in PropiLmodel]
mkKripkeModel [constructor, in PropiLmodel]
mkKripkeModel [constructor, in PropiLmodel]
Monotonicity [definition, in PropiL]
N
nat_le_dec [instance, in Base]nat_eq_dec [instance, in Base]
nd [inductive, in PropiL]
ndA [constructor, in PropiL]
ndAE [constructor, in PropiL]
ndAI [constructor, in PropiL]
ndCW [lemma, in PropiL]
ndE [constructor, in PropiL]
ndIE [constructor, in PropiL]
ndII [constructor, in PropiL]
ndOE [constructor, in PropiL]
ndOIL [constructor, in PropiL]
ndOIR [constructor, in PropiL]
ndW [lemma, in PropiL]
nd_soundKM [lemma, in PropiLmodel]
nd_soundHA [lemma, in PropiLmodel]
nd_soundKM [lemma, in PropiLmodel]
nd_soundHA [lemma, in PropiLmodel]
nd_soundFK [lemma, in PropiLFmodel]
nd_soundTK [lemma, in PropiLFmodel]
nd_dec [lemma, in PropiL]
nd_OrARcut [lemma, in PropiL]
nd_OrCut [lemma, in PropiL]
nd_hil [lemma, in PropiL]
nd_onesided [lemma, in PropiL]
nd_EntailRelation [lemma, in PropiL]
nd_cons [lemma, in PropiL]
nd_NoFal [lemma, in PropiL]
nd_gen [lemma, in PropiL]
nd_subst [lemma, in PropiL]
nd_or [lemma, in PropiL]
nd_and [lemma, in PropiL]
nd_fal [lemma, in PropiL]
nd_imp [lemma, in PropiL]
nd_cut [lemma, in PropiL]
nd_mono [lemma, in PropiL]
nd_refl [lemma, in PropiL]
Neg [constructor, in PropiL]
negative [definition, in PropiL]
negative_dec [instance, in PropiLFmodel]
negImp [definition, in PropiLFmodel2]
negImp [definition, in PropiLFmodel2]
negImp_dec [instance, in PropiLFmodel2]
negImp_dec [instance, in PropiLFmodel2]
negtrip_empty [lemma, in PropiLFmodel]
negtrip_in [lemma, in PropiLFmodel]
Not [definition, in PropiL]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
O
Or [constructor, in PropiL]OrAR [definition, in PropiL]
OrAR_mono_nd [lemma, in PropiL]
OrAR_mono [lemma, in PropiL]
OrFree [definition, in PropiL]
or_dec [instance, in Base]
P
PContext [definition, in PropiLFmodel]PContextRelation [section, in PropiLFmodel]
PContextRelation.pRC [variable, in PropiLFmodel]
PContextRelation.pRC_dec [variable, in PropiLFmodel]
PC2C [definition, in PropiLFmodel]
PC2C_pushpos [lemma, in PropiLFmodel]
PC2C_pushneg [lemma, in PropiLFmodel]
PC2C_neg [lemma, in PropiLFmodel]
PC2C_pos [lemma, in PropiLFmodel]
persist [projection, in PropiLmodel]
persist [projection, in PropiLmodel]
persist [projection, in PropiLFmodel]
pos [definition, in PropiLFmodel]
Pos [constructor, in PropiL]
positive [definition, in PropiL]
positive_dec [instance, in PropiLFmodel]
postrip_in [lemma, in PropiLFmodel]
posVar [definition, in PropiLFmodel2]
posVars [definition, in PropiLFmodel2]
posVar_dec [instance, in PropiLFmodel2]
pos_in [lemma, in PropiLFmodel2]
pos_in [lemma, in PropiLFmodel2]
power [definition, in Base]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
PowerRep.X [variable, in Base]
power_once [lemma, in PropiLFmodel]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
prod_eq_dec [instance, in PropiLFmodel]
PropiL [library]
PropiLFmodel [library]
PropiLFmodel2 [library]
PropiLmodel [library]
pVar_nImp_dec [instance, in PropiLFmodel2]
pVar_nImp [definition, in PropiLFmodel2]
pVar_nImp_dec [instance, in PropiLFmodel2]
pVar_nImp [definition, in PropiLFmodel2]
Q
qmax [definition, in PropiLFmodel2]qmax_Uequi [lemma, in PropiLFmodel2]
qmax_Uequi [lemma, in PropiLFmodel2]
qmax_maxext [lemma, in PropiLFmodel2]
qmax_exists [lemma, in PropiLFmodel2]
qmax_or [lemma, in PropiLFmodel2]
R
R [projection, in PropiLmodel]R [projection, in PropiLmodel]
RC [definition, in PropiLFmodel]
RCinterp [definition, in PropiLFmodel]
RCList [definition, in PropiLFmodel]
RC_dec [instance, in PropiLFmodel]
Reflexivity [definition, in PropiL]
RelationToList [section, in PropiLFmodel]
RelationToList.R [variable, in PropiLFmodel]
RelationToList.S [variable, in PropiLFmodel]
RelationToList.SS [variable, in PropiLFmodel]
RelationToList.X [variable, in PropiLFmodel]
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 Base]
rep_evalTK' [lemma, in PropiLFmodel]
rep_evalTK [lemma, in PropiLFmodel]
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_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]
RList [definition, in PropiLFmodel]
RList_in [lemma, in PropiLFmodel]
RList_ind [lemma, in PropiLFmodel]
RList_closure [lemma, in PropiLFmodel]
Rref [projection, in PropiLmodel]
Rref [projection, in PropiLmodel]
RTC [definition, in PropiLFmodel]
RTC_RCList [lemma, in PropiLFmodel]
RTC_iff [lemma, in PropiLFmodel]
RTC_in [lemma, in PropiLFmodel]
RTC_transitive [lemma, in PropiLFmodel]
RTC_reflexive [lemma, in PropiLFmodel]
RTC_ind [lemma, in PropiLFmodel]
RTC_closure [lemma, in PropiLFmodel]
Rtra [projection, in PropiLmodel]
Rtra [projection, in PropiLmodel]
S
satC [definition, in PropiLFmodel2]satisD [definition, in PropiLFmodel]
satisDFK [definition, in PropiLFmodel2]
satisFK [definition, in PropiLFmodel]
satisFK' [definition, in PropiLFmodel]
scl [definition, in PropiL]
sclNeg_in [lemma, in PropiLFmodel2]
sclPos_in [lemma, in PropiLFmodel2]
scl_closed [lemma, in PropiL]
scl_incl [lemma, in PropiL]
scl_incl' [lemma, in PropiL]
scl' [definition, in PropiL]
scl'_closed [lemma, in PropiL]
scl'_in [lemma, in PropiL]
sform [inductive, in PropiL]
sform_eq_dec [instance, in PropiL]
sfs [definition, in PropiLFmodel2]
sf_closed_cons [lemma, in PropiL]
sf_closed_app [lemma, in PropiL]
sf_closed [definition, in PropiL]
sigma_forall_list [lemma, in PropiLFmodel2]
size [definition, in PropiL]
sizeF [definition, in PropiL]
size_recursion [lemma, in Base]
ssc_scl [lemma, in PropiLFmodel2]
ssL [definition, in PropiL]
ssL [section, in PropiL]
ssLb [definition, in PropiL]
ssL_idempotent [lemma, in PropiL]
ssL_app [lemma, in PropiL]
ssL_mono [lemma, in PropiL]
ssL_in [lemma, in PropiL]
ssL_correct [lemma, in PropiL]
ssL' [definition, in PropiL]
ssL'_in_ssL2 [lemma, in PropiL]
ssL'_in_ssL [lemma, in PropiL]
ssL'_correct [lemma, in PropiL]
ssL'_in [lemma, in PropiL]
ssL'_self [lemma, in PropiL]
ss_closed_app [lemma, in PropiL]
ss_closed'_mono [lemma, in PropiL]
ss_closed [definition, in PropiL]
ss_closed' [definition, in PropiL]
state [definition, in PropiLFmodel]
step [definition, in PropiL]
stepFKImp [definition, in PropiLFmodel]
stepImp [definition, in PropiLFmodel]
stepRList [definition, in PropiLFmodel]
stepRList_dec [instance, in PropiLFmodel]
stepRTC [definition, in PropiLFmodel]
stepRTC_dec [instance, in PropiLFmodel]
stepTab [definition, in PropiLFmodel]
stepTab_mono [lemma, in PropiLFmodel]
stepTab_dec [instance, in PropiLFmodel]
stepTab' [definition, in PropiLFmodel]
stepUC [definition, in PropiLFmodel]
step_dec [instance, in PropiL]
subC [lemma, in PropiLFmodel]
SubClause [section, in PropiLFmodel]
subPC [definition, in PropiLFmodel]
subPos [definition, in PropiLFmodel2]
subPos [definition, in PropiLFmodel2]
subst [definition, in PropiL]
Substitution [definition, in PropiL]
sup [definition, in PropiLFmodel]
s2b [definition, in PropiL]
T
tab [inductive, in PropiL]tabAN [constructor, in PropiL]
tabAP [constructor, in PropiL]
tabC [constructor, in PropiL]
tabCS [lemma, in PropiL]
tabF [constructor, in PropiL]
tabIN [constructor, in PropiL]
tabIP [constructor, in PropiL]
TableauxConsistency [section, in PropiLFmodel]
TableauxDecidability [section, in PropiLFmodel]
TableauxDecidability.sscU [variable, in PropiLFmodel]
TableauxDecidability.U [variable, in PropiLFmodel]
tabLW [lemma, in PropiL]
TabND [section, in PropiLFmodel2]
tabON [constructor, in PropiL]
tabOP [constructor, in PropiL]
tabRW [lemma, in PropiL]
tabW [lemma, in PropiL]
tab_dec [lemma, in PropiLFmodel]
tab_dec' [lemma, in PropiLFmodel]
tab_lfp [lemma, in PropiLFmodel]
tab_nd [lemma, in PropiL]
tab_ndG [lemma, in PropiL]
tab_gen [lemma, in PropiL]
tab_genG [lemma, in PropiL]
tab_iff_ndG [lemma, in PropiLFmodel2]
tab_iff_nd [lemma, in PropiLFmodel2]
tab_nd_sat [lemma, in PropiLFmodel2]
TK [definition, in PropiLFmodel]
top [definition, in PropiLmodel]
top [definition, in PropiLmodel]
top1 [lemma, in PropiLmodel]
top1 [lemma, in PropiLmodel]
trip [definition, in PropiLFmodel]
True_dec [instance, in Base]
truthVal [definition, in PropiLFmodel]
TruthValues [section, in PropiLFmodel]
TruthValues.Implication [section, in PropiLFmodel]
TruthValues.K [variable, in PropiLFmodel]
TruthValues.Kdupfree [variable, in PropiLFmodel]
truthVal_evalTK' [lemma, in PropiLFmodel]
truthVal_evalTK [lemma, in PropiLFmodel]
truthVal_FImp [lemma, in PropiLFmodel]
truthVal_Binter [lemma, in PropiLFmodel]
truthVal_Bunion [lemma, in PropiLFmodel]
truthVal_inter [lemma, in PropiLFmodel]
truthVal_union [lemma, in PropiLFmodel]
U
U [definition, in PropiL]UCS [definition, in PropiLFmodel]
UCSE [definition, in PropiLFmodel]
UCSE_sound [lemma, in PropiLFmodel]
ucsPred [definition, in PropiLFmodel]
UCS_sub [lemma, in PropiLFmodel]
UCS_in [lemma, in PropiLFmodel]
UCS_ind [lemma, in PropiLFmodel]
UCS_closure [lemma, in PropiLFmodel]
undup [definition, in Base]
Undup [section, in Base]
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_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]
Undup.X [variable, in Base]
union [definition, in PropiLFmodel]
union_sub [lemma, in PropiLFmodel]
union_sound [lemma, in PropiLFmodel]
uns [definition, in PropiL]
uns_pos [lemma, in PropiL]
upset [definition, in PropiLFmodel]
UpwardClosure [section, in PropiLFmodel]
UpwardClosure.R [variable, in PropiLFmodel]
UpwardClosure.U [variable, in PropiLFmodel]
UpwardClosure.X [variable, in PropiLFmodel]
U_sfc [definition, in PropiL]
V
Var [constructor, in PropiL]var [definition, in PropiL]
Vf [definition, in PropiLmodel]
Vf [definition, in PropiLmodel]
W
W [projection, in PropiLmodel]W [projection, in PropiLmodel]
WE [projection, in PropiLFmodel]
WF [projection, in PropiLFmodel]
WR [projection, in PropiLmodel]
WR [projection, in PropiLmodel]
WRref [projection, in PropiLmodel]
WRref [projection, in PropiLmodel]
WRtra [projection, in PropiLmodel]
WRtra [projection, in PropiLmodel]
WS [projection, in PropiLFmodel]
other
_ === _ [notation, in Base]_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
+ _ [notation, in PropiL]
- _ [notation, in PropiL]
| _ | [notation, in Base]
Notation Index
other
_ === _ [in Base]_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
+ _ [in PropiL]
- _ [in PropiL]
| _ | [in Base]
Module Index
F
FCI [in Base]FCI [in Base]
Variable Index
C
CanonicalDemo.sscU [in PropiLFmodel2]CanonicalDemo.U [in PropiLFmodel2]
Cardinality.X [in Base]
CounterModels.K1 [in PropiLFmodel]
CounterModels.K2 [in PropiLFmodel]
CounterModels.K3 [in PropiLFmodel]
CounterModels.K4 [in PropiLFmodel]
D
Decidability.A0 [in PropiL]Decidability.s0 [in PropiL]
Dupfree.X [in Base]
Dupfree.X [in Base]
E
EntailmentRelationProperties.E [in PropiL]EntailmentRelationProperties.F [in PropiL]
Equi.X [in Base]
F
FCI.FCI.step [in Base]FCI.FCI.step [in Base]
FCI.FCI.V [in Base]
FCI.FCI.V [in Base]
FCI.FCI.X [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]
FiniteClosure.F [in PropiLFmodel]
FiniteClosure.FE [in PropiLFmodel]
FiniteClosure.FS [in PropiLFmodel]
FiniteClosure.UCSFilter [in PropiLFmodel]
FiniteKripke.FKM [in PropiLFmodel]
FiniteKripke.interp [in PropiLFmodel]
FiniteKripke.pW [in PropiLFmodel]
FiniteKripke.W [in PropiLFmodel]
FiniteKripke.WR [in PropiLFmodel]
FiniteKripke.WRref [in PropiLFmodel]
FiniteKripke.WRtra [in PropiLFmodel]
FormHeytingAlgebra.bot [in PropiLmodel]
FormHeytingAlgebra.bot [in PropiLmodel]
FormHeytingAlgebra.H [in PropiLmodel]
FormHeytingAlgebra.H [in PropiLmodel]
FormHeytingAlgebra.imp [in PropiLmodel]
FormHeytingAlgebra.imp [in PropiLmodel]
FormHeytingAlgebra.join [in PropiLmodel]
FormHeytingAlgebra.join [in PropiLmodel]
FormHeytingAlgebra.meet [in PropiLmodel]
FormHeytingAlgebra.meet [in PropiLmodel]
FormHeytingAlgebra.R [in PropiLmodel]
FormHeytingAlgebra.R [in PropiLmodel]
H
HAProperty.HA [in PropiLmodel]HAProperty.HA [in PropiLmodel]
HASound.HA [in PropiLmodel]
HASound.HA [in PropiLmodel]
HASound.interp [in PropiLmodel]
HASound.interp [in PropiLmodel]
I
Inclusion.X [in Base]Iteration.f [in Base]
Iteration.X [in Base]
K
KripkeSemantics.KM [in PropiLmodel]KripkeSemantics.KM [in PropiLmodel]
Kripke2Heyting.bot [in PropiLmodel]
Kripke2Heyting.bot [in PropiLmodel]
Kripke2Heyting.H [in PropiLmodel]
Kripke2Heyting.H [in PropiLmodel]
Kripke2Heyting.imp [in PropiLmodel]
Kripke2Heyting.imp [in PropiLmodel]
Kripke2Heyting.join [in PropiLmodel]
Kripke2Heyting.join [in PropiLmodel]
Kripke2Heyting.KM [in PropiLmodel]
Kripke2Heyting.KM [in PropiLmodel]
Kripke2Heyting.meet [in PropiLmodel]
Kripke2Heyting.meet [in PropiLmodel]
Kripke2Heyting.R [in PropiLmodel]
Kripke2Heyting.R [in PropiLmodel]
Kripke2Heyting.UC [in PropiLmodel]
Kripke2Heyting.UC [in PropiLmodel]
Kripke2Heyting.UCS [in PropiLmodel]
Kripke2Heyting.UCS [in PropiLmodel]
L
ListOperation.X [in PropiLFmodel]M
MaximalExtension.p [in PropiLFmodel2]MaximalExtension.p_mono [in PropiLFmodel2]
MaximalExtension.U [in PropiLFmodel2]
MaximalExtension.X [in PropiLFmodel2]
MaximalIdentity.sclU [in PropiLFmodel2]
MaximalIdentity.SFL [in PropiLFmodel2]
MaximalIdentity.SFL [in PropiLFmodel2]
MaximalIdentity.U [in PropiLFmodel2]
Membership.X [in Base]
P
PContextRelation.pRC [in PropiLFmodel]PContextRelation.pRC_dec [in PropiLFmodel]
PowerRep.X [in Base]
PowerRep.X [in Base]
R
RelationToList.R [in PropiLFmodel]RelationToList.S [in PropiLFmodel]
RelationToList.SS [in PropiLFmodel]
RelationToList.X [in PropiLFmodel]
Removal.X [in Base]
T
TableauxDecidability.sscU [in PropiLFmodel]TableauxDecidability.U [in PropiLFmodel]
TruthValues.K [in PropiLFmodel]
TruthValues.Kdupfree [in PropiLFmodel]
U
Undup.X [in Base]Undup.X [in Base]
UpwardClosure.R [in PropiLFmodel]
UpwardClosure.U [in PropiLFmodel]
UpwardClosure.X [in PropiLFmodel]
Library Index
B
BaseP
PropiLPropiLFmodel
PropiLFmodel2
PropiLmodel
Lemma Index
B
baseKD_complete [in PropiLFmodel]baseKD_sound [in PropiLFmodel]
baseKD_in [in PropiLFmodel]
baseVars_in [in PropiLFmodel]
baseVars_incl [in PropiLFmodel]
Binter_sound [in PropiLFmodel]
Bunion_sound [in PropiLFmodel]
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]
CD_demo [in PropiLFmodel2]
compact_restore_demo [in PropiLFmodel2]
compact_CD_equi [in PropiLFmodel2]
compact_sound [in PropiLFmodel2]
compact_cons [in PropiLFmodel2]
compact_restore_demo [in PropiLFmodel2]
compact_CD_equi [in PropiLFmodel2]
compact_sound [in PropiLFmodel2]
compact_cons [in PropiLFmodel2]
consW [in PropiLFmodel]
Cons_mono [in PropiLFmodel2]
CVars_correct [in PropiLFmodel]
D
dec_ucsPred [in PropiLFmodel]dec_prop_iff [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
DemoSat [in PropiLFmodel2]
DemoSatisAll [in PropiLFmodel2]
Demo_equi [in PropiLFmodel]
demo_extension [in PropiLFmodel2]
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]
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]
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
EntailRelAllProps_ext [in PropiL]equi_rotate [in Base]
equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
evalFK_OrAR [in PropiLFmodel]
evalFK_mono [in PropiLFmodel]
evalHf [in PropiLmodel]
evalHf [in PropiLmodel]
evalK_evalH_agree [in PropiLmodel]
evalK_mono [in PropiLmodel]
evalK_evalH_agree [in PropiLmodel]
evalK_mono [in PropiLmodel]
extension [in PropiLFmodel2]
F
FCI.closure [in Base]FCI.closure [in Base]
FCI.fp [in Base]
FCI.fp [in Base]
FCI.incl [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
FCI.pick [in Base]
filter_idempotent [in PropiLFmodel]
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]
filter_equi [in PropiLFmodel2]
FImpList_in [in PropiLFmodel]
FImpList_ind [in PropiLFmodel]
FImpList_closure [in PropiLFmodel]
FImp_in4 [in PropiLFmodel]
FImp_in3 [in PropiLFmodel]
FImp_in2 [in PropiLFmodel]
FImp_in1 [in PropiLFmodel]
FImp_greatest [in PropiLFmodel]
FImp_Heyting [in PropiLFmodel]
FKImp_in [in PropiLFmodel]
FKImp_ind [in PropiLFmodel]
FKImp_closure [in PropiLFmodel]
G
genA [in PropiL]genCW [in PropiL]
genW [in PropiL]
gen_DN [in PropiL]
gen_DN' [in PropiL]
gen_lambda [in PropiL]
gen_iff_tab [in PropiL]
gen_tab [in PropiL]
gen_iff_nd [in PropiL]
gen_nd [in PropiL]
gen_NoNVar [in PropiL]
gen_NoVar [in PropiL]
gen_EntailRelation [in PropiL]
gen_subst [in PropiL]
gen_or [in PropiL]
gen_and_both [in PropiL]
gen_and [in PropiL]
gen_fal [in PropiL]
gen_imp [in PropiL]
gen_cons [in PropiL]
gen_NoFal [in PropiL]
gen_cut [in PropiL]
gen_GCut [in PropiL]
gen_mono [in PropiL]
H
HAequiv [in PropiLmodel]HAequiv [in PropiLmodel]
HA_iff_nd [in PropiLmodel]
HA_nd [in PropiLmodel]
HA_iff_nd [in PropiLmodel]
HA_nd [in PropiLmodel]
hent_imp [in PropiLmodel]
hent_imp [in PropiLmodel]
hilAK [in PropiL]
hilAS [in PropiL]
hilD [in PropiL]
hilI [in PropiL]
hil_iff_nd [in PropiL]
hil_nd [in PropiL]
Hintikka_equi [in PropiLFmodel]
I
imp2 [in PropiLmodel]imp2 [in PropiLmodel]
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]
inter_sub [in PropiLFmodel]
inter_sound [in PropiLFmodel]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
in_map_informative [in PropiLFmodel2]
it_fp [in Base]
it_ind [in Base]
J
join_com [in PropiLmodel]join_com [in PropiLmodel]
join2 [in PropiLmodel]
join2 [in PropiLmodel]
join3 [in PropiLmodel]
join3 [in PropiLmodel]
K
kripke_nd [in PropiLFmodel2]L
lambda_gen [in PropiL]lambda_ind [in PropiL]
lambda_closure [in PropiL]
lfpTab_ind [in PropiLFmodel]
lfpTab_closure [in PropiLFmodel]
lfp_tab [in PropiLFmodel]
list_cc [in Base]
list_exists_not_incl [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
ltr_CharImp [in PropiLmodel]
ltr_CharImp [in PropiLmodel]
M
maxCons_PartialOrder [in PropiLFmodel2]maxCons_ParOrd [in PropiLFmodel2]
maxCons_equi [in PropiLFmodel2]
maxCons_incl [in PropiLFmodel2]
maxCons_equi_Fal [in PropiLFmodel2]
maxCons_PartialOrder [in PropiLFmodel2]
maxCons_ParOrd [in PropiLFmodel2]
maxCons_equi [in PropiLFmodel2]
maxCons_incl [in PropiLFmodel2]
maxCons_equi_Fal [in PropiLFmodel2]
maxCons_equi_vars [in PropiLFmodel2]
maxCons_XM [in PropiLFmodel2]
maxExtension [in PropiLFmodel2]
maxext_samebase [in PropiLFmodel2]
maxext_samebase [in PropiLFmodel2]
maxext_nomore [in PropiLFmodel2]
meet_com [in PropiLmodel]
meet_com [in PropiLmodel]
meet2 [in PropiLmodel]
meet2 [in PropiLmodel]
meet3 [in PropiLmodel]
meet3 [in PropiLmodel]
N
ndCW [in PropiL]ndW [in PropiL]
nd_soundKM [in PropiLmodel]
nd_soundHA [in PropiLmodel]
nd_soundKM [in PropiLmodel]
nd_soundHA [in PropiLmodel]
nd_soundFK [in PropiLFmodel]
nd_soundTK [in PropiLFmodel]
nd_dec [in PropiL]
nd_OrARcut [in PropiL]
nd_OrCut [in PropiL]
nd_hil [in PropiL]
nd_onesided [in PropiL]
nd_EntailRelation [in PropiL]
nd_cons [in PropiL]
nd_NoFal [in PropiL]
nd_gen [in PropiL]
nd_subst [in PropiL]
nd_or [in PropiL]
nd_and [in PropiL]
nd_fal [in PropiL]
nd_imp [in PropiL]
nd_cut [in PropiL]
nd_mono [in PropiL]
nd_refl [in PropiL]
negtrip_empty [in PropiLFmodel]
negtrip_in [in PropiLFmodel]
not_in_cons [in Base]
O
OrAR_mono_nd [in PropiL]OrAR_mono [in PropiL]
P
PC2C_pushpos [in PropiLFmodel]PC2C_pushneg [in PropiLFmodel]
PC2C_neg [in PropiLFmodel]
PC2C_pos [in PropiLFmodel]
postrip_in [in PropiLFmodel]
pos_in [in PropiLFmodel2]
pos_in [in PropiLFmodel2]
power_once [in PropiLFmodel]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
Q
qmax_Uequi [in PropiLFmodel2]qmax_Uequi [in PropiLFmodel2]
qmax_maxext [in PropiLFmodel2]
qmax_exists [in PropiLFmodel2]
qmax_or [in PropiLFmodel2]
R
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]
rep_evalTK' [in PropiLFmodel]
rep_evalTK [in PropiLFmodel]
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_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]
RList_in [in PropiLFmodel]
RList_ind [in PropiLFmodel]
RList_closure [in PropiLFmodel]
RTC_RCList [in PropiLFmodel]
RTC_iff [in PropiLFmodel]
RTC_in [in PropiLFmodel]
RTC_transitive [in PropiLFmodel]
RTC_reflexive [in PropiLFmodel]
RTC_ind [in PropiLFmodel]
RTC_closure [in PropiLFmodel]
S
sclNeg_in [in PropiLFmodel2]sclPos_in [in PropiLFmodel2]
scl_closed [in PropiL]
scl_incl [in PropiL]
scl_incl' [in PropiL]
scl'_closed [in PropiL]
scl'_in [in PropiL]
sf_closed_cons [in PropiL]
sf_closed_app [in PropiL]
sigma_forall_list [in PropiLFmodel2]
size_recursion [in Base]
ssc_scl [in PropiLFmodel2]
ssL_idempotent [in PropiL]
ssL_app [in PropiL]
ssL_mono [in PropiL]
ssL_in [in PropiL]
ssL_correct [in PropiL]
ssL'_in_ssL2 [in PropiL]
ssL'_in_ssL [in PropiL]
ssL'_correct [in PropiL]
ssL'_in [in PropiL]
ssL'_self [in PropiL]
ss_closed_app [in PropiL]
ss_closed'_mono [in PropiL]
stepTab_mono [in PropiLFmodel]
subC [in PropiLFmodel]
T
tabCS [in PropiL]tabLW [in PropiL]
tabRW [in PropiL]
tabW [in PropiL]
tab_dec [in PropiLFmodel]
tab_dec' [in PropiLFmodel]
tab_lfp [in PropiLFmodel]
tab_nd [in PropiL]
tab_ndG [in PropiL]
tab_gen [in PropiL]
tab_genG [in PropiL]
tab_iff_ndG [in PropiLFmodel2]
tab_iff_nd [in PropiLFmodel2]
tab_nd_sat [in PropiLFmodel2]
top1 [in PropiLmodel]
top1 [in PropiLmodel]
truthVal_evalTK' [in PropiLFmodel]
truthVal_evalTK [in PropiLFmodel]
truthVal_FImp [in PropiLFmodel]
truthVal_Binter [in PropiLFmodel]
truthVal_Bunion [in PropiLFmodel]
truthVal_inter [in PropiLFmodel]
truthVal_union [in PropiLFmodel]
U
UCSE_sound [in PropiLFmodel]UCS_sub [in PropiLFmodel]
UCS_in [in PropiLFmodel]
UCS_ind [in PropiLFmodel]
UCS_closure [in PropiLFmodel]
undup_idempotent [in Base]
undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
undup_idempotent [in Base]
undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
union_sub [in PropiLFmodel]
union_sound [in PropiLFmodel]
uns_pos [in PropiL]
Constructor Index
A
And [in PropiL]D
dupfreeC [in Base]dupfreeC [in Base]
dupfreeN [in Base]
dupfreeN [in Base]
F
Fal [in PropiL]G
genAL [in PropiL]genAR [in PropiL]
genF [in PropiL]
genIL [in PropiL]
genIR [in PropiL]
genOL [in PropiL]
genOR1 [in PropiL]
genOR2 [in PropiL]
genV [in PropiL]
H
hilA [in PropiL]hilAI [in PropiL]
hilAL [in PropiL]
hilAR [in PropiL]
hilE [in PropiL]
hilK [in PropiL]
hilMP [in PropiL]
hilOE [in PropiL]
hilOL [in PropiL]
hilOR [in PropiL]
hilS [in PropiL]
I
Imp [in PropiL]M
mkFiniteKripkeModel [in PropiLFmodel]mkHeytingAlgebra [in PropiLmodel]
mkHeytingAlgebra [in PropiLmodel]
mkKripkeModel [in PropiLmodel]
mkKripkeModel [in PropiLmodel]
N
ndA [in PropiL]ndAE [in PropiL]
ndAI [in PropiL]
ndE [in PropiL]
ndIE [in PropiL]
ndII [in PropiL]
ndOE [in PropiL]
ndOIL [in PropiL]
ndOIR [in PropiL]
Neg [in PropiL]
O
Or [in PropiL]P
Pos [in PropiL]T
tabAN [in PropiL]tabAP [in PropiL]
tabC [in PropiL]
tabF [in PropiL]
tabIN [in PropiL]
tabIP [in PropiL]
tabON [in PropiL]
tabOP [in PropiL]
V
Var [in PropiL]Projection Index
B
bot [in PropiLmodel]bot [in PropiLmodel]
bot1 [in PropiLmodel]
bot1 [in PropiLmodel]
E
eq_decW [in PropiLFmodel]H
H [in PropiLmodel]H [in PropiLmodel]
I
imp [in PropiLmodel]imp [in PropiLmodel]
imp1 [in PropiLmodel]
imp1 [in PropiLmodel]
interp [in PropiLmodel]
interp [in PropiLmodel]
interp [in PropiLFmodel]
J
join [in PropiLmodel]join [in PropiLmodel]
join1 [in PropiLmodel]
join1 [in PropiLmodel]
M
meet [in PropiLmodel]meet [in PropiLmodel]
meet1 [in PropiLmodel]
meet1 [in PropiLmodel]
P
persist [in PropiLmodel]persist [in PropiLmodel]
persist [in PropiLFmodel]
R
R [in PropiLmodel]R [in PropiLmodel]
Rref [in PropiLmodel]
Rref [in PropiLmodel]
Rtra [in PropiLmodel]
Rtra [in PropiLmodel]
W
W [in PropiLmodel]W [in PropiLmodel]
WE [in PropiLFmodel]
WF [in PropiLFmodel]
WR [in PropiLmodel]
WR [in PropiLmodel]
WRref [in PropiLmodel]
WRref [in PropiLmodel]
WRtra [in PropiLmodel]
WRtra [in PropiLmodel]
WS [in PropiLFmodel]
Inductive Index
D
dupfree [in Base]dupfree [in Base]
F
form [in PropiL]G
gen [in PropiL]H
hil [in PropiL]N
nd [in PropiL]S
sform [in PropiL]T
tab [in PropiL]Section Index
C
CanonicalDemo [in PropiLFmodel2]Cardinality [in Base]
CounterModels [in PropiLFmodel]
D
Decidability [in PropiL]Demo [in PropiLFmodel]
DemoFiniteKripke [in PropiLFmodel2]
DemoKBase [in PropiLFmodel]
Dupfree [in Base]
Dupfree [in Base]
E
EntailmentRelationProperties [in PropiL]Equi [in Base]
F
FCI.FCI [in Base]FCI.FCI [in Base]
FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
FiniteClosure [in PropiLFmodel]
FiniteKripke [in PropiLFmodel]
FormHeytingAlgebra [in PropiLmodel]
FormHeytingAlgebra [in PropiLmodel]
H
HAProperty [in PropiLmodel]HAProperty [in PropiLmodel]
HASound [in PropiLmodel]
HASound [in PropiLmodel]
I
Inclusion [in Base]Iteration [in Base]
K
KripkeSemantics [in PropiLmodel]KripkeSemantics [in PropiLmodel]
Kripke2Heyting [in PropiLmodel]
Kripke2Heyting [in PropiLmodel]
L
ListOperation [in PropiLFmodel]M
MaximalExtension [in PropiLFmodel2]MaximalIdentity [in PropiLFmodel2]
Membership [in Base]
P
PContextRelation [in PropiLFmodel]PowerRep [in Base]
PowerRep [in Base]
R
RelationToList [in PropiLFmodel]Removal [in Base]
S
ssL [in PropiL]SubClause [in PropiLFmodel]
T
TableauxConsistency [in PropiLFmodel]TableauxDecidability [in PropiLFmodel]
TabND [in PropiLFmodel2]
TruthValues [in PropiLFmodel]
TruthValues.Implication [in PropiLFmodel]
U
Undup [in Base]Undup [in Base]
UpwardClosure [in PropiLFmodel]
Instance Index
A
and_dec [in Base]app_equi_proper [in Base]
app_incl_proper [in Base]
B
bool_eq_dec [in Base]C
card_equi_proper [in Base]cons_dec [in PropiLFmodel]
cons_equi_proper [in Base]
cons_incl_proper [in Base]
Cons_dec [in PropiLFmodel2]
E
equi_Equivalence [in Base]F
False_dec [in Base]form_eq_dec [in PropiL]
G
goal_eq_dec [in PropiL]H
Hintikka_dec [in PropiLFmodel]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]
negative_dec [in PropiLFmodel]
negImp_dec [in PropiLFmodel2]
negImp_dec [in PropiLFmodel2]
not_dec [in Base]
O
or_dec [in Base]P
positive_dec [in PropiLFmodel]posVar_dec [in PropiLFmodel2]
prod_eq_dec [in PropiLFmodel]
pVar_nImp_dec [in PropiLFmodel2]
pVar_nImp_dec [in PropiLFmodel2]
R
RC_dec [in PropiLFmodel]S
sform_eq_dec [in PropiL]stepRList_dec [in PropiLFmodel]
stepRTC_dec [in PropiLFmodel]
stepTab_dec [in PropiLFmodel]
step_dec [in PropiL]
T
True_dec [in Base]Definition Index
A
AndFree [in PropiL]B
base [in PropiLFmodel]baseKD [in PropiLFmodel]
baseVars [in PropiLFmodel]
Binter [in PropiLFmodel]
Bunion [in PropiLFmodel]
b2s [in PropiL]
C
card [in Base]CD [in PropiLFmodel2]
CharAnd [in PropiL]
CharFal [in PropiL]
CharImp [in PropiL]
CharOr [in PropiL]
clause [in PropiL]
clauseCD [in PropiLFmodel2]
compactCD_restore [in PropiLFmodel2]
compactCD_restore [in PropiLFmodel2]
compactDemo [in PropiLFmodel2]
compactDemo [in PropiLFmodel2]
compact_CD [in PropiLFmodel2]
compact_CD [in PropiLFmodel2]
cons [in PropiLFmodel]
Cons [in PropiLFmodel2]
Consistency [in PropiL]
context [in PropiL]
Cut [in PropiL]
CVars [in PropiLFmodel]
c2f [in PropiL]
C2PC [in PropiLFmodel]
D
dec [in Base]decision [in Base]
Demo [in PropiLFmodel]
depth [in PropiL]
dequi [in PropiLFmodel]
disjoint [in Base]
dsub [in PropiLFmodel]
dupfree_inv [in Base]
dupfree_inv [in Base]
D2FKM [in PropiLFmodel2]
E
EntailRelAllProps [in PropiL]eqH [in PropiLmodel]
eqH [in PropiLmodel]
Equi [in PropiL]
equi [in Base]
evalFK [in PropiLFmodel]
evalH [in PropiLmodel]
evalH [in PropiLmodel]
evalH' [in PropiLmodel]
evalH' [in PropiLmodel]
evalK [in PropiLmodel]
evalK [in PropiLmodel]
evalKA [in PropiLmodel]
evalKA [in PropiLmodel]
evalTK [in PropiLFmodel]
evalTK' [in PropiLFmodel]
F
FalFree [in PropiL]FCI.C [in Base]
FCI.C [in Base]
FCI.F [in Base]
FCI.F [in Base]
filter [in Base]
FImp [in PropiLFmodel]
FImpList [in PropiLFmodel]
FK [in PropiL]
FKImp [in PropiLFmodel]
FK2K [in PropiLFmodel]
FormHA [in PropiLmodel]
FormHA [in PropiLmodel]
FP [in Base]
FS [in PropiL]
G
Gamma [in PropiL]goal [in PropiL]
H
hent [in PropiLmodel]hent [in PropiLmodel]
Hintikka [in PropiLFmodel]
I
ImpFree [in PropiL]inclp [in Base]
inter [in PropiLFmodel]
interpTK [in PropiLFmodel]
it [in Base]
K
K_Peirce [in PropiLFmodel]K_DN [in PropiLFmodel]
K_XM [in PropiLFmodel]
K_neg [in PropiLFmodel]
K_orxy [in PropiLFmodel]
K_var [in PropiLFmodel]
K_Fal [in PropiLFmodel]
K2H [in PropiLmodel]
K2H [in PropiLmodel]
K2Hinterp [in PropiLmodel]
K2Hinterp [in PropiLmodel]
L
Lambda [in PropiL]lfpTab [in PropiLFmodel]
ltr [in PropiLmodel]
ltr [in PropiLmodel]
M
maxext [in PropiLFmodel2]Monotonicity [in PropiL]
N
negative [in PropiL]negImp [in PropiLFmodel2]
negImp [in PropiLFmodel2]
Not [in PropiL]
O
OrAR [in PropiL]OrFree [in PropiL]
P
PContext [in PropiLFmodel]PC2C [in PropiLFmodel]
pos [in PropiLFmodel]
positive [in PropiL]
posVar [in PropiLFmodel2]
posVars [in PropiLFmodel2]
power [in Base]
power [in Base]
pVar_nImp [in PropiLFmodel2]
pVar_nImp [in PropiLFmodel2]
Q
qmax [in PropiLFmodel2]R
RC [in PropiLFmodel]RCinterp [in PropiLFmodel]
RCList [in PropiLFmodel]
Reflexivity [in PropiL]
rem [in Base]
rep [in Base]
rep [in Base]
RList [in PropiLFmodel]
RTC [in PropiLFmodel]
S
satC [in PropiLFmodel2]satisD [in PropiLFmodel]
satisDFK [in PropiLFmodel2]
satisFK [in PropiLFmodel]
satisFK' [in PropiLFmodel]
scl [in PropiL]
scl' [in PropiL]
sfs [in PropiLFmodel2]
sf_closed [in PropiL]
size [in PropiL]
sizeF [in PropiL]
ssL [in PropiL]
ssLb [in PropiL]
ssL' [in PropiL]
ss_closed [in PropiL]
ss_closed' [in PropiL]
state [in PropiLFmodel]
step [in PropiL]
stepFKImp [in PropiLFmodel]
stepImp [in PropiLFmodel]
stepRList [in PropiLFmodel]
stepRTC [in PropiLFmodel]
stepTab [in PropiLFmodel]
stepTab' [in PropiLFmodel]
stepUC [in PropiLFmodel]
subPC [in PropiLFmodel]
subPos [in PropiLFmodel2]
subPos [in PropiLFmodel2]
subst [in PropiL]
Substitution [in PropiL]
sup [in PropiLFmodel]
s2b [in PropiL]
T
TK [in PropiLFmodel]top [in PropiLmodel]
top [in PropiLmodel]
trip [in PropiLFmodel]
truthVal [in PropiLFmodel]
U
U [in PropiL]UCS [in PropiLFmodel]
UCSE [in PropiLFmodel]
ucsPred [in PropiLFmodel]
undup [in Base]
undup [in Base]
union [in PropiLFmodel]
uns [in PropiL]
upset [in PropiLFmodel]
U_sfc [in PropiL]
V
var [in PropiL]Vf [in PropiLmodel]
Vf [in PropiLmodel]
Record Index
F
FiniteKripkeModel [in PropiLFmodel]H
HeytingAlgebra [in PropiLmodel]HeytingAlgebra [in PropiLmodel]
K
KripkeModel [in PropiLmodel]KripkeModel [in PropiLmodel]
| 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 | (876 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 | (2 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 | (108 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 | (5 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 | (381 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 | (53 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 | (42 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 | (8 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 | (49 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 | (43 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 | (173 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 | (5 entries) |
This page has been generated by coqdoc