| 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 | (676 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 | (58 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 | (12 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 | (309 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (55 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 | (13 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 | (65 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 | (6 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 | (20 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 | (125 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 | (12 entries) |
Global Index
A
abs [definition, in ImpAlg.ImplicativeStructures]abs_mon [lemma, in ImpAlg.ImplicativeStructures]
adequacy [lemma, in ImpAlg.Adequacy]
Adequacy [section, in ImpAlg.Adequacy]
Adequacy [library]
adequacy_empty [lemma, in ImpAlg.Adequacy]
λ- _ (ia_scope) [notation, in ImpAlg.Adequacy]
_ @ _ (ia_scope) [notation, in ImpAlg.Adequacy]
_ ^t _ [notation, in ImpAlg.Adequacy]
_ ^tc _ [notation, in ImpAlg.Adequacy]
_ ^t^ _ [notation, in ImpAlg.Adequacy]
_ ^v _ [notation, in ImpAlg.Adequacy]
_ ^c _ [notation, in ImpAlg.Adequacy]
_ ^^ _ [notation, in ImpAlg.Adequacy]
{ _ ~t> _ } _ [notation, in ImpAlg.Adequacy]
{ _ ~> _ } _ [notation, in ImpAlg.Adequacy]
adjunction [lemma, in ImpAlg.ImplicativeStructures]
AKS [record, in ImpAlg.AKS]
AKS [library]
AKS_IA [instance, in ImpAlg.AKS]
AKS_IS [instance, in ImpAlg.AKS]
anti_mon [definition, in ImpAlg.Lattices]
app [projection, in ImpAlg.AKS]
app [projection, in ImpAlg.OCA]
app [definition, in ImpAlg.ImplicativeStructures]
app_CHA [lemma, in ImpAlg.HeytingAlgebras]
app_mon [projection, in ImpAlg.OCA]
app_closed [lemma, in ImpAlg.ImplicativeAlgebras]
app_CBA [lemma, in ImpAlg.BooleanAlgebras]
app_closure [definition, in ImpAlg.ImplicativeStructures]
app_min [lemma, in ImpAlg.ImplicativeStructures]
app_eta [lemma, in ImpAlg.ImplicativeStructures]
app_beta [lemma, in ImpAlg.ImplicativeStructures]
app_mon [lemma, in ImpAlg.ImplicativeStructures]
app_mon_r [lemma, in ImpAlg.ImplicativeStructures]
app_mon_l [lemma, in ImpAlg.ImplicativeStructures]
arrow [definition, in ImpAlg.AKS]
arrow [projection, in ImpAlg.ImplicativeStructures]
arrowtop [definition, in ImpAlg.Dummies]
arrow_entails_mon [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_l [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_r [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_r [definition, in ImpAlg.Dummies]
arrow_bot [lemma, in ImpAlg.ImplicativeStructures]
arrow_prenex [lemma, in ImpAlg.ImplicativeStructures]
arrow_mon [lemma, in ImpAlg.ImplicativeStructures]
arrow_meet [projection, in ImpAlg.ImplicativeStructures]
arrow_mon_r [projection, in ImpAlg.ImplicativeStructures]
arrow_mon_l [projection, in ImpAlg.ImplicativeStructures]
arrow_set_Proper [instance, in ImpAlg.ImplicativeStructures]
arrow_set [definition, in ImpAlg.ImplicativeStructures]
arrow_set_r [definition, in ImpAlg.ImplicativeStructures]
arrow_set_l [definition, in ImpAlg.ImplicativeStructures]
B
B [definition, in ImpAlg.Combinators]BA_cc [lemma, in ImpAlg.BooleanAlgebras]
BA_S [lemma, in ImpAlg.BooleanAlgebras]
BA_K [lemma, in ImpAlg.BooleanAlgebras]
BA_HA [instance, in ImpAlg.BooleanAlgebras]
betared [inductive, in ImpAlg.Lambda]
betared_abs [constructor, in ImpAlg.Lambda]
betared_app2 [constructor, in ImpAlg.Lambda]
betared_app1 [constructor, in ImpAlg.Lambda]
betared_red [constructor, in ImpAlg.Lambda]
betarule [lemma, in ImpAlg.ImplicativeStructures]
beta_cvar [lemma, in ImpAlg.Lambda]
beta_subst [lemma, in ImpAlg.Lambda]
beta_subst_n [lemma, in ImpAlg.Lambda]
beta_red [lemma, in ImpAlg.ImplicativeStructures]
body [definition, in ImpAlg.Lambda]
BooleanAlgebra [record, in ImpAlg.BooleanAlgebras]
BooleanAlgebras [library]
bot [projection, in ImpAlg.Lattices]
bot_min [projection, in ImpAlg.Lattices]
bot_meet [lemma, in ImpAlg.BooleanAlgebras]
BoundedLattice [record, in ImpAlg.Lattices]
by_refl [lemma, in ImpAlg.Lattices]
C
carreer [definition, in ImpAlg.OCA]case [definition, in ImpAlg.ImplicativeAlgebras]
CBA_IA [instance, in ImpAlg.BooleanAlgebras]
CBA_IS [instance, in ImpAlg.BooleanAlgebras]
CBA_CHA [instance, in ImpAlg.BooleanAlgebras]
CBL [instance, in ImpAlg.Lattices]
cc [projection, in ImpAlg.AKS]
cc [definition, in ImpAlg.Adequacy]
CCreal [lemma, in ImpAlg.AKS]
cc_polymorph [lemma, in ImpAlg.Lambda]
CHA_IS [instance, in ImpAlg.HeytingAlgebras]
closed [definition, in ImpAlg.Lambda]
closed_typ [definition, in ImpAlg.ImplicativeAlgebras]
closed_typ [definition, in ImpAlg.Lambda]
codom [definition, in ImpAlg.Combinators]
codom [definition, in ImpAlg.ImplicativeAlgebras]
codom [definition, in ImpAlg.Lambda]
codom_concat [lemma, in ImpAlg.Lambda]
codom_push [lemma, in ImpAlg.Lambda]
codom_single [lemma, in ImpAlg.Lambda]
codom_empty [lemma, in ImpAlg.Lambda]
comb [inductive, in ImpAlg.Combinators]
combApp [constructor, in ImpAlg.Combinators]
combCC [constructor, in ImpAlg.Combinators]
combinator [inductive, in ImpAlg.Combinators]
Combinators [section, in ImpAlg.Combinators]
Combinators [library]
$ _ [notation, in ImpAlg.Combinators]
[ _ ] _ [notation, in ImpAlg.Combinators]
λ+ _ [notation, in ImpAlg.Combinators]
combinatory_completeness [axiom, in ImpAlg.Combinators]
combinator_trm_translated [lemma, in ImpAlg.Combinators]
combinator_comb [lemma, in ImpAlg.Combinators]
combK [constructor, in ImpAlg.Combinators]
combS [constructor, in ImpAlg.Combinators]
comb_app [constructor, in ImpAlg.Combinators]
comb_cc [constructor, in ImpAlg.Combinators]
comb_Id [constructor, in ImpAlg.Combinators]
comb_K [constructor, in ImpAlg.Combinators]
comb_S [constructor, in ImpAlg.Combinators]
compat_app [definition, in ImpAlg.Lambda]
CompleteBooleanAlgebra [record, in ImpAlg.BooleanAlgebras]
CompleteHeytingAlgebra [record, in ImpAlg.HeytingAlgebras]
CompleteLattice [record, in ImpAlg.Lattices]
composition [lemma, in ImpAlg.ImplicativeAlgebras]
consistent [projection, in ImpAlg.Lattices]
cont [projection, in ImpAlg.AKS]
contraposition_r [lemma, in ImpAlg.ImplicativeAlgebras]
contraposition_l [lemma, in ImpAlg.ImplicativeAlgebras]
D
Definitions [section, in ImpAlg.Lambda]_ |= _ : _ [notation, in ImpAlg.Lambda]
_ ^t _ [notation, in ImpAlg.Lambda]
_ ^tc _ [notation, in ImpAlg.Lambda]
_ ^t^ _ [notation, in ImpAlg.Lambda]
_ ^v _ [notation, in ImpAlg.Lambda]
_ ^c _ [notation, in ImpAlg.Lambda]
_ ^^ _ [notation, in ImpAlg.Lambda]
[ _ ~> _ ] _ [notation, in ImpAlg.Lambda]
[ _ ~> _ ] _ [notation, in ImpAlg.Lambda]
{ _ ~t> _ } _ [notation, in ImpAlg.Lambda]
{ _ ~> _ } _ [notation, in ImpAlg.Lambda]
dn [lemma, in ImpAlg.ImplicativeAlgebras]
dne [lemma, in ImpAlg.ImplicativeAlgebras]
dni [lemma, in ImpAlg.ImplicativeAlgebras]
double_meet_elim [lemma, in ImpAlg.Lattices]
double_meet [lemma, in ImpAlg.Lattices]
double_neg [lemma, in ImpAlg.BooleanAlgebras]
Dummies [library]
Dummy [section, in ImpAlg.Dummies]
dummy_top_abs [lemma, in ImpAlg.Dummies]
dummy_top_app [lemma, in ImpAlg.Dummies]
dummy_imp_top [instance, in ImpAlg.Dummies]
dummy_imp_r [instance, in ImpAlg.Dummies]
E
Easy [definition, in ImpAlg.Combinators]empty [definition, in ImpAlg.Lambda]
emptyset [definition, in ImpAlg.Lattices]
empty_eq [lemma, in ImpAlg.Lambda]
empty_fv_typ_subst [lemma, in ImpAlg.Adequacy]
empty_fv_trm_subst [lemma, in ImpAlg.Adequacy]
Ens [definition, in ImpAlg.Lattices]
entails [definition, in ImpAlg.ImplicativeAlgebras]
entails_half_adj [lemma, in ImpAlg.ImplicativeAlgebras]
entails_trans [lemma, in ImpAlg.ImplicativeAlgebras]
entails_refl [lemma, in ImpAlg.ImplicativeAlgebras]
env [definition, in ImpAlg.Combinators]
env [definition, in ImpAlg.ImplicativeAlgebras]
env [definition, in ImpAlg.Lambda]
equivalence [definition, in ImpAlg.ImplicativeAlgebras]
equiv_sep [lemma, in ImpAlg.ImplicativeAlgebras]
eta [definition, in ImpAlg.ImplicativeStructures]
etarule [lemma, in ImpAlg.ImplicativeStructures]
exfalso_S [lemma, in ImpAlg.ImplicativeAlgebras]
existst [definition, in ImpAlg.ImplicativeAlgebras]
ex_term [definition, in ImpAlg.ImplicativeAlgebras]
F
fn_typ_type [lemma, in ImpAlg.Lambda]fn_typ_type_aux [lemma, in ImpAlg.Lambda]
fn_typ_fall [lemma, in ImpAlg.Lambda]
fn_typ_fall_aux [lemma, in ImpAlg.Lambda]
fn_typ_fall_Aux [lemma, in ImpAlg.Lambda]
fn_typ_arrow [lemma, in ImpAlg.Lambda]
fn_typ_fall_bvar [lemma, in ImpAlg.Lambda]
fn_trm_term [lemma, in ImpAlg.Lambda]
fn_trm_term_aux [lemma, in ImpAlg.Lambda]
fn_trm_abs [lemma, in ImpAlg.Lambda]
fn_trm_abs_aux [lemma, in ImpAlg.Lambda]
fn_trm_abs_Aux [lemma, in ImpAlg.Lambda]
fn_trm_app [lemma, in ImpAlg.Lambda]
fn_typ [definition, in ImpAlg.Lambda]
fn_typ_aux [definition, in ImpAlg.Lambda]
fn_trm [definition, in ImpAlg.Lambda]
fn_trm_aux [definition, in ImpAlg.Lambda]
forallt [definition, in ImpAlg.ImplicativeAlgebras]
from_list_nil_inv [lemma, in ImpAlg.Lambda]
from_list_app [lemma, in ImpAlg.Lambda]
fv_typ [definition, in ImpAlg.Combinators]
fv_trm [definition, in ImpAlg.Combinators]
fv_typ [definition, in ImpAlg.ImplicativeAlgebras]
fv_trm [definition, in ImpAlg.ImplicativeAlgebras]
fv_open_trm [lemma, in ImpAlg.Lambda]
fv_trm_subst [lemma, in ImpAlg.Lambda]
fv_typ [definition, in ImpAlg.Lambda]
fv_trm [definition, in ImpAlg.Lambda]
fv_typ_subst [lemma, in ImpAlg.Adequacy]
G
geq_S_S [lemma, in ImpAlg.Lambda]geq_1_S [lemma, in ImpAlg.Lambda]
glb [definition, in ImpAlg.Lattices]
glb_elim_intro [lemma, in ImpAlg.Lattices]
glb_unique [lemma, in ImpAlg.Lattices]
H
ha_adjunction [lemma, in ImpAlg.ImplicativeAlgebras]HeytingAlgebra [record, in ImpAlg.HeytingAlgebras]
HeytingAlgebras [library]
I
IA [section, in ImpAlg.ImplicativeAlgebras]_ ⊕ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ × _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ≈ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ⊢ _ [notation, in ImpAlg.ImplicativeAlgebras]
$ _ [notation, in ImpAlg.ImplicativeAlgebras]
[ _ ] _ [notation, in ImpAlg.ImplicativeAlgebras]
[∀] _ [notation, in ImpAlg.ImplicativeAlgebras]
[∃] _ [notation, in ImpAlg.ImplicativeAlgebras]
¬ _ [notation, in ImpAlg.ImplicativeAlgebras]
λ+ _ [notation, in ImpAlg.ImplicativeAlgebras]
Id [definition, in ImpAlg.Combinators]
Idum [definition, in ImpAlg.Dummies]
Id_SK [lemma, in ImpAlg.Combinators]
II_neq_I [lemma, in ImpAlg.Dummies]
image_set [definition, in ImpAlg.Lattices]
imp [projection, in ImpAlg.HeytingAlgebras]
ImplicativeAlgebra [record, in ImpAlg.ImplicativeAlgebras]
ImplicativeAlgebras [library]
ImplicativeStructure [record, in ImpAlg.ImplicativeStructures]
ImplicativeStructures [library]
imp_comb [definition, in ImpAlg.Combinators]
imp_meet [lemma, in ImpAlg.HeytingAlgebras]
imp_is_join [lemma, in ImpAlg.HeytingAlgebras]
imp_mon_r [lemma, in ImpAlg.HeytingAlgebras]
imp_mon_l [lemma, in ImpAlg.HeytingAlgebras]
imp_adj [lemma, in ImpAlg.HeytingAlgebras]
imp_lub [lemma, in ImpAlg.HeytingAlgebras]
imp_intro [lemma, in ImpAlg.HeytingAlgebras]
imp_self [lemma, in ImpAlg.HeytingAlgebras]
imp_elim [lemma, in ImpAlg.HeytingAlgebras]
imp_sup [projection, in ImpAlg.HeytingAlgebras]
imp_betared [lemma, in ImpAlg.Adequacy]
imp_betared_n [lemma, in ImpAlg.Adequacy]
inf [definition, in ImpAlg.Lattices]
inf_comm [lemma, in ImpAlg.Lattices]
inf_comm_aux [lemma, in ImpAlg.Lattices]
inf_elim_trans [lemma, in ImpAlg.Lattices]
inj1 [definition, in ImpAlg.ImplicativeAlgebras]
inj2 [definition, in ImpAlg.ImplicativeAlgebras]
Intersection_set_glb [lemma, in ImpAlg.Powerset]
Intersection_set_lb [lemma, in ImpAlg.Powerset]
Intersection_set [definition, in ImpAlg.Powerset]
Intersection_included [lemma, in ImpAlg.Powerset]
Intersection_idempotent [lemma, in ImpAlg.Powerset]
Intersection_absorptive [lemma, in ImpAlg.Powerset]
Intersection_associative [lemma, in ImpAlg.Powerset]
Intersection_sym [lemma, in ImpAlg.Powerset]
in_list [definition, in ImpAlg.Lambda]
I_neq_SKK_dum [lemma, in ImpAlg.Dummies]
J
join [projection, in ImpAlg.Lattices]join_set_Proper [instance, in ImpAlg.Lattices]
join_same_set [lemma, in ImpAlg.Lattices]
join_subset [lemma, in ImpAlg.Lattices]
join_elim_trans [lemma, in ImpAlg.Lattices]
join_family [definition, in ImpAlg.Lattices]
join_set_lub [lemma, in ImpAlg.Lattices]
join_emptyset [lemma, in ImpAlg.Lattices]
join_intro [projection, in ImpAlg.Lattices]
join_elim [projection, in ImpAlg.Lattices]
join_set [projection, in ImpAlg.Lattices]
join_top_r [lemma, in ImpAlg.Lattices]
join_top_l [lemma, in ImpAlg.Lattices]
join_bot_r [lemma, in ImpAlg.Lattices]
join_bot_l [lemma, in ImpAlg.Lattices]
join_meet_completeness [lemma, in ImpAlg.Lattices]
join_complete [definition, in ImpAlg.Lattices]
join_mon_r [lemma, in ImpAlg.Lattices]
join_mon_l [lemma, in ImpAlg.Lattices]
join_lub [lemma, in ImpAlg.Lattices]
join_ub_r [lemma, in ImpAlg.Lattices]
join_ub_l [lemma, in ImpAlg.Lattices]
join_consistent [lemma, in ImpAlg.Lattices]
join_idempotent [projection, in ImpAlg.Lattices]
join_absorptive [projection, in ImpAlg.Lattices]
join_associative [projection, in ImpAlg.Lattices]
join_commutative [projection, in ImpAlg.Lattices]
join_meet_set [lemma, in ImpAlg.BooleanAlgebras]
join_neg [projection, in ImpAlg.BooleanAlgebras]
join_distributive [projection, in ImpAlg.BooleanAlgebras]
K
K [definition, in ImpAlg.Combinators]k [projection, in ImpAlg.AKS]
k [projection, in ImpAlg.OCA]
Kdum [definition, in ImpAlg.Dummies]
Kreal [lemma, in ImpAlg.AKS]
k_red [projection, in ImpAlg.OCA]
L
Lambda [library]lambdaB [definition, in ImpAlg.Combinators]
lambdaEasy [definition, in ImpAlg.Combinators]
lambdaId [definition, in ImpAlg.Combinators]
lambdaK [definition, in ImpAlg.Combinators]
lambdaS [definition, in ImpAlg.Combinators]
lambdaW [definition, in ImpAlg.Combinators]
lambda_B [lemma, in ImpAlg.Combinators]
lambda_Easy [lemma, in ImpAlg.Combinators]
lambda_W [lemma, in ImpAlg.Combinators]
lambda_S [lemma, in ImpAlg.Combinators]
lambda_K [lemma, in ImpAlg.Combinators]
lambda_Id [lemma, in ImpAlg.Combinators]
Lattice [record, in ImpAlg.Lattices]
Lattices [library]
lb [definition, in ImpAlg.Lattices]
lub [definition, in ImpAlg.Lattices]
lub_elim_intro [lemma, in ImpAlg.Lattices]
lub_unique [lemma, in ImpAlg.Lattices]
M
map_pred_S [lemma, in ImpAlg.Lambda]map_pred_app [lemma, in ImpAlg.Lambda]
map_pred_cons [lemma, in ImpAlg.Lambda]
map_pred [definition, in ImpAlg.Lambda]
meet [projection, in ImpAlg.Lattices]
meet_set_Proper [instance, in ImpAlg.Lattices]
meet_same_set [lemma, in ImpAlg.Lattices]
meet_same_set_le [lemma, in ImpAlg.Lattices]
meet_subset [lemma, in ImpAlg.Lattices]
meet_fam_intro [lemma, in ImpAlg.Lattices]
meet_fam_elim [lemma, in ImpAlg.Lattices]
meet_comm [lemma, in ImpAlg.Lattices]
meet_comm_aux [lemma, in ImpAlg.Lattices]
meet_elim_trans [lemma, in ImpAlg.Lattices]
meet_family [definition, in ImpAlg.Lattices]
meet_set_glb [lemma, in ImpAlg.Lattices]
meet_emptyset [lemma, in ImpAlg.Lattices]
meet_intro [projection, in ImpAlg.Lattices]
meet_elim [projection, in ImpAlg.Lattices]
meet_set [projection, in ImpAlg.Lattices]
meet_top_r [lemma, in ImpAlg.Lattices]
meet_top_l [lemma, in ImpAlg.Lattices]
meet_bot_r [lemma, in ImpAlg.Lattices]
meet_bot_l [lemma, in ImpAlg.Lattices]
meet_join_completeness [lemma, in ImpAlg.Lattices]
meet_complete [definition, in ImpAlg.Lattices]
meet_mon_r [lemma, in ImpAlg.Lattices]
meet_mon_l [lemma, in ImpAlg.Lattices]
meet_glb [lemma, in ImpAlg.Lattices]
meet_lb_r [lemma, in ImpAlg.Lattices]
meet_lb_l [lemma, in ImpAlg.Lattices]
meet_join [lemma, in ImpAlg.Lattices]
meet_idempotent [projection, in ImpAlg.Lattices]
meet_absorptive [projection, in ImpAlg.Lattices]
meet_associative [projection, in ImpAlg.Lattices]
meet_commutative [projection, in ImpAlg.Lattices]
meet_join_set [lemma, in ImpAlg.BooleanAlgebras]
meet_neg [projection, in ImpAlg.BooleanAlgebras]
meet_distributive [projection, in ImpAlg.BooleanAlgebras]
min [definition, in ImpAlg.Lattices]
modus_ponens_later [lemma, in ImpAlg.ImplicativeAlgebras]
modus_ponens [projection, in ImpAlg.ImplicativeAlgebras]
mod_ponens [lemma, in ImpAlg.ImplicativeAlgebras]
mod_pon_app [lemma, in ImpAlg.ImplicativeStructures]
mod_pon_closure [definition, in ImpAlg.ImplicativeStructures]
N
neg [definition, in ImpAlg.ImplicativeAlgebras]neg [projection, in ImpAlg.BooleanAlgebras]
neg_join_set [lemma, in ImpAlg.BooleanAlgebras]
neg_meet_set [lemma, in ImpAlg.BooleanAlgebras]
neg_mon [lemma, in ImpAlg.BooleanAlgebras]
neg_meet [lemma, in ImpAlg.BooleanAlgebras]
neg_join [lemma, in ImpAlg.BooleanAlgebras]
neg_bot [lemma, in ImpAlg.BooleanAlgebras]
neg_top [lemma, in ImpAlg.BooleanAlgebras]
neg_complement [lemma, in ImpAlg.BooleanAlgebras]
O
OCA [record, in ImpAlg.OCA]OCA [library]
OCA_IS [instance, in ImpAlg.OCA]
open_trm_term [lemma, in ImpAlg.Lambda]
open_typ_com_ct [lemma, in ImpAlg.Lambda]
open_typ_com_ff [lemma, in ImpAlg.Lambda]
open_typ_com_cc [lemma, in ImpAlg.Lambda]
open_typ_com_cf [lemma, in ImpAlg.Lambda]
open_typ_type [lemma, in ImpAlg.Lambda]
open_typ_fn [lemma, in ImpAlg.Lambda]
open_trm_com_v [lemma, in ImpAlg.Lambda]
open_trm_com_ct [lemma, in ImpAlg.Lambda]
open_term [lemma, in ImpAlg.Lambda]
open_trm_fn [lemma, in ImpAlg.Lambda]
open_typ_fvar [definition, in ImpAlg.Lambda]
open_typ [definition, in ImpAlg.Lambda]
open_rec_typ [definition, in ImpAlg.Lambda]
open_trm_def [lemma, in ImpAlg.Lambda]
open_trm_var [definition, in ImpAlg.Lambda]
open_trm [definition, in ImpAlg.Lambda]
open_rec_trm [definition, in ImpAlg.Lambda]
ord [projection, in ImpAlg.Lattices]
Order [record, in ImpAlg.Lattices]
ord_Antisymmetric [instance, in ImpAlg.Lattices]
ord_Transitive [instance, in ImpAlg.Lattices]
ord_Reflexive [instance, in ImpAlg.Lattices]
ord_trans [projection, in ImpAlg.Lattices]
ord_antisym [projection, in ImpAlg.Lattices]
ord_refl [projection, in ImpAlg.Lattices]
orth [definition, in ImpAlg.AKS]
P
pair [definition, in ImpAlg.ImplicativeAlgebras]PL [projection, in ImpAlg.AKS]
PL_app_closed [projection, in ImpAlg.AKS]
PL_cc [projection, in ImpAlg.AKS]
PL_k [projection, in ImpAlg.AKS]
PL_s [projection, in ImpAlg.AKS]
pole [projection, in ImpAlg.AKS]
Powerset [section, in ImpAlg.Powerset]
Powerset [library]
Powerset_CompleteLattice [instance, in ImpAlg.Powerset]
Powerset_Lattice [instance, in ImpAlg.Powerset]
Powerset_Order [instance, in ImpAlg.Powerset]
_ ⊆ _ [notation, in ImpAlg.Powerset]
preimage [definition, in ImpAlg.Lattices]
preimage_set [definition, in ImpAlg.Lattices]
pre_upclosed_rev [lemma, in ImpAlg.Lattices]
prodt [definition, in ImpAlg.ImplicativeAlgebras]
prodt_intro [lemma, in ImpAlg.ImplicativeAlgebras]
prodt_r [lemma, in ImpAlg.ImplicativeAlgebras]
prodt_l [lemma, in ImpAlg.ImplicativeAlgebras]
proj1 [definition, in ImpAlg.ImplicativeAlgebras]
proj2 [definition, in ImpAlg.ImplicativeAlgebras]
push [projection, in ImpAlg.AKS]
R
realize [definition, in ImpAlg.OCA]realize [inductive, in ImpAlg.Adequacy]
realizer_later [lemma, in ImpAlg.ImplicativeAlgebras]
realize_update [lemma, in ImpAlg.Adequacy]
realize_inv [lemma, in ImpAlg.Adequacy]
real_push [constructor, in ImpAlg.Adequacy]
real_empty [constructor, in ImpAlg.Adequacy]
red_cont [projection, in ImpAlg.AKS]
red_cc [projection, in ImpAlg.AKS]
red_s [projection, in ImpAlg.AKS]
red_k [projection, in ImpAlg.AKS]
red_push [projection, in ImpAlg.AKS]
remove [definition, in ImpAlg.Lambda]
remove_pred_0 [lemma, in ImpAlg.Lambda]
remove_pred [lemma, in ImpAlg.Lambda]
remove_comm [lemma, in ImpAlg.Lambda]
remove_0_def [lemma, in ImpAlg.Lambda]
remove_app [lemma, in ImpAlg.Lambda]
remove_0_incl [lemma, in ImpAlg.Lambda]
remove_0_cons_0 [lemma, in ImpAlg.Lambda]
remove_0 [definition, in ImpAlg.Lambda]
rev [definition, in ImpAlg.Lattices]
RevBooleanAlgebra [definition, in ImpAlg.BooleanAlgebras]
RevBoundedLattice [definition, in ImpAlg.Lattices]
RevCompleteBooleanAlgebra [definition, in ImpAlg.BooleanAlgebras]
RevCompleteLattice [definition, in ImpAlg.Lattices]
reverse [definition, in ImpAlg.Lattices]
revinc [definition, in ImpAlg.AKS]
revinc_orth [lemma, in ImpAlg.AKS]
RevLattice [definition, in ImpAlg.Lattices]
RevOrd [definition, in ImpAlg.Lattices]
rev_consistent [lemma, in ImpAlg.Lattices]
rev_trans [lemma, in ImpAlg.Lattices]
rev_antisym [lemma, in ImpAlg.Lattices]
rev_refl [lemma, in ImpAlg.Lattices]
S
S [definition, in ImpAlg.Combinators]s [projection, in ImpAlg.AKS]
s [projection, in ImpAlg.OCA]
same_set_sym [lemma, in ImpAlg.Lattices]
same_set [definition, in ImpAlg.Lattices]
sclosed [definition, in ImpAlg.Combinators]
sclosed_translated [lemma, in ImpAlg.ImplicativeAlgebras]
sclosed_translated_n [lemma, in ImpAlg.ImplicativeAlgebras]
Sdum [definition, in ImpAlg.Dummies]
separator [projection, in ImpAlg.ImplicativeAlgebras]
sep_Easy [lemma, in ImpAlg.ImplicativeAlgebras]
sep_W [lemma, in ImpAlg.ImplicativeAlgebras]
sep_typ [lemma, in ImpAlg.ImplicativeAlgebras]
sep_sclosed [lemma, in ImpAlg.ImplicativeAlgebras]
sep_term [lemma, in ImpAlg.ImplicativeAlgebras]
sep_comb [lemma, in ImpAlg.ImplicativeAlgebras]
sep_Id [lemma, in ImpAlg.ImplicativeAlgebras]
sep_cc [projection, in ImpAlg.ImplicativeAlgebras]
sep_S [projection, in ImpAlg.ImplicativeAlgebras]
sep_K [projection, in ImpAlg.ImplicativeAlgebras]
size [definition, in ImpAlg.Lambda]
size_typ_arrow_le_r [lemma, in ImpAlg.Lambda]
size_typ_arrow_le_l [lemma, in ImpAlg.Lambda]
size_typ_arrow [lemma, in ImpAlg.Lambda]
size_typ_plus_S [lemma, in ImpAlg.Lambda]
size_typ_S [lemma, in ImpAlg.Lambda]
size_typ_open_f [lemma, in ImpAlg.Lambda]
size_typ_open [lemma, in ImpAlg.Lambda]
size_typ_le_1 [lemma, in ImpAlg.Lambda]
size_typ_ind [lemma, in ImpAlg.Lambda]
size_typ_ind_gen [lemma, in ImpAlg.Lambda]
size_typ_induction [lemma, in ImpAlg.Lambda]
size_typ_not_0 [lemma, in ImpAlg.Lambda]
size_typ [definition, in ImpAlg.Lambda]
size_plus_S [lemma, in ImpAlg.Lambda]
size_S [lemma, in ImpAlg.Lambda]
size_app_le_r [lemma, in ImpAlg.Lambda]
size_app_le_l [lemma, in ImpAlg.Lambda]
size_open_v [lemma, in ImpAlg.Lambda]
size_open_c [lemma, in ImpAlg.Lambda]
size_le_1 [lemma, in ImpAlg.Lambda]
size_ind [lemma, in ImpAlg.Lambda]
size_ind_gen [lemma, in ImpAlg.Lambda]
size_induction [lemma, in ImpAlg.Lambda]
size_not_0 [lemma, in ImpAlg.Lambda]
Sreal [lemma, in ImpAlg.AKS]
sterm [inductive, in ImpAlg.Combinators]
sterm_term [lemma, in ImpAlg.Combinators]
sterm_cc [constructor, in ImpAlg.Combinators]
sterm_app [constructor, in ImpAlg.Combinators]
sterm_abs [constructor, in ImpAlg.Combinators]
sterm_var [constructor, in ImpAlg.Combinators]
stype [inductive, in ImpAlg.Lambda]
stype_arrow [constructor, in ImpAlg.Lambda]
stype_fall [constructor, in ImpAlg.Lambda]
stype_fvar [constructor, in ImpAlg.Lambda]
subset [definition, in ImpAlg.Lattices]
subset_trans [lemma, in ImpAlg.Lambda]
subst [definition, in ImpAlg.Lambda]
substitution [definition, in ImpAlg.Adequacy]
subst_term [lemma, in ImpAlg.Lambda]
subst_intro [lemma, in ImpAlg.Lambda]
subst_open_var [lemma, in ImpAlg.Lambda]
subst_open [lemma, in ImpAlg.Lambda]
subst_fresh [lemma, in ImpAlg.Lambda]
subst_trm [definition, in ImpAlg.Lambda]
subst_trm_update [lemma, in ImpAlg.Adequacy]
subst_trm_update_open [lemma, in ImpAlg.Adequacy]
subst_typ_update [lemma, in ImpAlg.Adequacy]
subst_typ_var [lemma, in ImpAlg.Adequacy]
subst_closed [lemma, in ImpAlg.Adequacy]
subst_trm_var [lemma, in ImpAlg.Adequacy]
subst_typ [definition, in ImpAlg.Adequacy]
subst_trm [definition, in ImpAlg.Adequacy]
subtyping [lemma, in ImpAlg.ImplicativeAlgebras]
Succ [definition, in ImpAlg.Combinators]
sumt [definition, in ImpAlg.ImplicativeAlgebras]
sumt_elim [lemma, in ImpAlg.ImplicativeAlgebras]
sumt_r [lemma, in ImpAlg.ImplicativeAlgebras]
sumt_l [lemma, in ImpAlg.ImplicativeAlgebras]
sup [definition, in ImpAlg.Lattices]
s_red [projection, in ImpAlg.OCA]
T
term [inductive, in ImpAlg.Lambda]term_subst [lemma, in ImpAlg.Lambda]
term_subst_n [lemma, in ImpAlg.Lambda]
term_cc [constructor, in ImpAlg.Lambda]
term_app [constructor, in ImpAlg.Lambda]
term_abs [constructor, in ImpAlg.Lambda]
term_cvar [constructor, in ImpAlg.Lambda]
term_var [constructor, in ImpAlg.Lambda]
top [projection, in ImpAlg.Lattices]
top_max [projection, in ImpAlg.Lattices]
top_join [lemma, in ImpAlg.BooleanAlgebras]
translated [inductive, in ImpAlg.Adequacy]
translated_comb [lemma, in ImpAlg.Combinators]
translated_Easy [lemma, in ImpAlg.Combinators]
translated_W [lemma, in ImpAlg.Combinators]
translated_S [lemma, in ImpAlg.Combinators]
translated_K [lemma, in ImpAlg.Combinators]
translated_Id [lemma, in ImpAlg.Combinators]
translated_peirce [lemma, in ImpAlg.Adequacy]
translated_typ_unique [lemma, in ImpAlg.Adequacy]
translated_typ [inductive, in ImpAlg.Adequacy]
translated_subst [lemma, in ImpAlg.Adequacy]
translated_subst_n [lemma, in ImpAlg.Adequacy]
translated_term [lemma, in ImpAlg.Adequacy]
translated_term_n [lemma, in ImpAlg.Adequacy]
translated_abs_inv [lemma, in ImpAlg.Adequacy]
translated_unique [lemma, in ImpAlg.Adequacy]
translated_closed [lemma, in ImpAlg.Adequacy]
trans_typ_open [lemma, in ImpAlg.Adequacy]
trans_typ_update [lemma, in ImpAlg.Adequacy]
trans_typ_correct [lemma, in ImpAlg.Adequacy]
trans_typ_var [lemma, in ImpAlg.Adequacy]
trans_typ_arrow [lemma, in ImpAlg.Adequacy]
trans_typ_fold [lemma, in ImpAlg.Adequacy]
trans_typ_fioul [lemma, in ImpAlg.Adequacy]
trans_typ_fall [lemma, in ImpAlg.Adequacy]
trans_typ [definition, in ImpAlg.Adequacy]
trans_typ_aux [definition, in ImpAlg.Adequacy]
trans_correct [lemma, in ImpAlg.Adequacy]
trans_trm_var [lemma, in ImpAlg.Adequacy]
trans_trm_abs [lemma, in ImpAlg.Adequacy]
trans_trm_app [lemma, in ImpAlg.Adequacy]
trans_trm_fold [lemma, in ImpAlg.Adequacy]
trans_trm_fioul [lemma, in ImpAlg.Adequacy]
trans_trm_fioul_aux [lemma, in ImpAlg.Adequacy]
trans_trm [definition, in ImpAlg.Adequacy]
trans_trm_aux [definition, in ImpAlg.Adequacy]
trm [inductive, in ImpAlg.Lambda]
trm_comb [definition, in ImpAlg.Combinators]
trm_cc [constructor, in ImpAlg.Lambda]
trm_app [constructor, in ImpAlg.Lambda]
trm_abs [constructor, in ImpAlg.Lambda]
trm_cvar [constructor, in ImpAlg.Lambda]
trm_fvar [constructor, in ImpAlg.Lambda]
trm_bvar [constructor, in ImpAlg.Lambda]
true_S [lemma, in ImpAlg.ImplicativeAlgebras]
tr_typ_fall [constructor, in ImpAlg.Adequacy]
tr_typ_arrow [constructor, in ImpAlg.Adequacy]
tr_typ_var [constructor, in ImpAlg.Adequacy]
tr_cc [constructor, in ImpAlg.Adequacy]
tr_app [constructor, in ImpAlg.Adequacy]
tr_abs [constructor, in ImpAlg.Adequacy]
tr_cvar [constructor, in ImpAlg.Adequacy]
typ [inductive, in ImpAlg.Lambda]
type [inductive, in ImpAlg.Lambda]
type_case [lemma, in ImpAlg.ImplicativeAlgebras]
type_inj2 [lemma, in ImpAlg.ImplicativeAlgebras]
type_inj1 [lemma, in ImpAlg.ImplicativeAlgebras]
type_proj2 [lemma, in ImpAlg.ImplicativeAlgebras]
type_proj1 [lemma, in ImpAlg.ImplicativeAlgebras]
type_pair [lemma, in ImpAlg.ImplicativeAlgebras]
type_ex_elim [lemma, in ImpAlg.ImplicativeAlgebras]
type_ex_intro [lemma, in ImpAlg.ImplicativeAlgebras]
type_fa_elim [lemma, in ImpAlg.ImplicativeAlgebras]
type_fa_intro [lemma, in ImpAlg.ImplicativeAlgebras]
type_subst [lemma, in ImpAlg.Lambda]
type_peirce [lemma, in ImpAlg.Lambda]
type_arrow [constructor, in ImpAlg.Lambda]
type_fall [constructor, in ImpAlg.Lambda]
type_cvar [constructor, in ImpAlg.Lambda]
type_fvar [constructor, in ImpAlg.Lambda]
typing_empty_closed [lemma, in ImpAlg.Lambda]
typing_fv_trm [lemma, in ImpAlg.Lambda]
typing_fv_trm_aux [lemma, in ImpAlg.Lambda]
typing_term [lemma, in ImpAlg.Lambda]
typing_type [lemma, in ImpAlg.Lambda]
typing_cc [constructor, in ImpAlg.Lambda]
typing_fallE [constructor, in ImpAlg.Lambda]
typing_fallI [constructor, in ImpAlg.Lambda]
typing_app [constructor, in ImpAlg.Lambda]
typing_abs [constructor, in ImpAlg.Lambda]
typing_prf_var [constructor, in ImpAlg.Lambda]
typing_trm [inductive, in ImpAlg.Lambda]
typing_subst_trm [lemma, in ImpAlg.Adequacy]
typ_eq_subst [lemma, in ImpAlg.Lambda]
typ_peirce [definition, in ImpAlg.Lambda]
typ_arrow [constructor, in ImpAlg.Lambda]
typ_fall [constructor, in ImpAlg.Lambda]
typ_cvar [constructor, in ImpAlg.Lambda]
typ_fvar [constructor, in ImpAlg.Lambda]
typ_bvar [constructor, in ImpAlg.Lambda]
U
ub [definition, in ImpAlg.Lattices]Union_set_lub [lemma, in ImpAlg.Powerset]
Union_set_ub [lemma, in ImpAlg.Powerset]
Union_set [definition, in ImpAlg.Powerset]
Union_idempotent [lemma, in ImpAlg.Powerset]
Union_absorptive [lemma, in ImpAlg.Powerset]
Union_associative [lemma, in ImpAlg.Powerset]
Union_sym [lemma, in ImpAlg.Powerset]
union_empty [lemma, in ImpAlg.Lambda]
update [definition, in ImpAlg.Adequacy]
upwards_closure [definition, in ImpAlg.ImplicativeStructures]
up_closed [projection, in ImpAlg.ImplicativeAlgebras]
up_closed_set [definition, in ImpAlg.Lattices]
V
var_eq_dec [lemma, in ImpAlg.Lambda]W
W [definition, in ImpAlg.Combinators]other
_ ⋁ _ (ia_scope) [notation, in ImpAlg.Lattices]_ ⋀ _ (ia_scope) [notation, in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [notation, in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [notation, in ImpAlg.Lattices]
λ- _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ ↪ _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ ↦ _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ · _ [notation, in ImpAlg.AKS]
_ @ _ [notation, in ImpAlg.AKS]
_ @ _ [notation, in ImpAlg.OCA]
_ @ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ∈ʆ [notation, in ImpAlg.ImplicativeAlgebras]
_ @ _ [notation, in ImpAlg.ImplicativeStructures]
_ ≅ _ [notation, in ImpAlg.ImplicativeStructures]
k[ _ ] [notation, in ImpAlg.AKS]
∩ _ [notation, in ImpAlg.Lattices]
⊓ [notation, in ImpAlg.Lattices]
⊔ [notation, in ImpAlg.Lattices]
⊤ [notation, in ImpAlg.Lattices]
⊥ [notation, in ImpAlg.Lattices]
⋂[ _ ] _ [notation, in ImpAlg.Lattices]
¬ _ [notation, in ImpAlg.BooleanAlgebras]
λ- _ [notation, in ImpAlg.ImplicativeAlgebras]
Notation Index
A
λ- _ (ia_scope) [in ImpAlg.Adequacy]_ @ _ (ia_scope) [in ImpAlg.Adequacy]
_ ^t _ [in ImpAlg.Adequacy]
_ ^tc _ [in ImpAlg.Adequacy]
_ ^t^ _ [in ImpAlg.Adequacy]
_ ^v _ [in ImpAlg.Adequacy]
_ ^c _ [in ImpAlg.Adequacy]
_ ^^ _ [in ImpAlg.Adequacy]
{ _ ~t> _ } _ [in ImpAlg.Adequacy]
{ _ ~> _ } _ [in ImpAlg.Adequacy]
C
$ _ [in ImpAlg.Combinators][ _ ] _ [in ImpAlg.Combinators]
λ+ _ [in ImpAlg.Combinators]
D
_ |= _ : _ [in ImpAlg.Lambda]_ ^t _ [in ImpAlg.Lambda]
_ ^tc _ [in ImpAlg.Lambda]
_ ^t^ _ [in ImpAlg.Lambda]
_ ^v _ [in ImpAlg.Lambda]
_ ^c _ [in ImpAlg.Lambda]
_ ^^ _ [in ImpAlg.Lambda]
[ _ ~> _ ] _ [in ImpAlg.Lambda]
[ _ ~> _ ] _ [in ImpAlg.Lambda]
{ _ ~t> _ } _ [in ImpAlg.Lambda]
{ _ ~> _ } _ [in ImpAlg.Lambda]
I
_ ⊕ _ [in ImpAlg.ImplicativeAlgebras]_ × _ [in ImpAlg.ImplicativeAlgebras]
_ ≈ _ [in ImpAlg.ImplicativeAlgebras]
_ ⊢ _ [in ImpAlg.ImplicativeAlgebras]
$ _ [in ImpAlg.ImplicativeAlgebras]
[ _ ] _ [in ImpAlg.ImplicativeAlgebras]
[∀] _ [in ImpAlg.ImplicativeAlgebras]
[∃] _ [in ImpAlg.ImplicativeAlgebras]
¬ _ [in ImpAlg.ImplicativeAlgebras]
λ+ _ [in ImpAlg.ImplicativeAlgebras]
P
_ ⊆ _ [in ImpAlg.Powerset]other
_ ⋁ _ (ia_scope) [in ImpAlg.Lattices]_ ⋀ _ (ia_scope) [in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [in ImpAlg.Lattices]
λ- _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ ↪ _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ ↦ _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ · _ [in ImpAlg.AKS]
_ @ _ [in ImpAlg.AKS]
_ @ _ [in ImpAlg.OCA]
_ @ _ [in ImpAlg.ImplicativeAlgebras]
_ ∈ʆ [in ImpAlg.ImplicativeAlgebras]
_ @ _ [in ImpAlg.ImplicativeStructures]
_ ≅ _ [in ImpAlg.ImplicativeStructures]
k[ _ ] [in ImpAlg.AKS]
∩ _ [in ImpAlg.Lattices]
⊓ [in ImpAlg.Lattices]
⊔ [in ImpAlg.Lattices]
⊤ [in ImpAlg.Lattices]
⊥ [in ImpAlg.Lattices]
⋂[ _ ] _ [in ImpAlg.Lattices]
¬ _ [in ImpAlg.BooleanAlgebras]
λ- _ [in ImpAlg.ImplicativeAlgebras]
Library Index
A
AdequacyAKS
B
BooleanAlgebrasC
CombinatorsD
DummiesH
HeytingAlgebrasI
ImplicativeAlgebrasImplicativeStructures
L
LambdaLattices
O
OCAP
PowersetLemma Index
A
abs_mon [in ImpAlg.ImplicativeStructures]adequacy [in ImpAlg.Adequacy]
adequacy_empty [in ImpAlg.Adequacy]
adjunction [in ImpAlg.ImplicativeStructures]
app_CHA [in ImpAlg.HeytingAlgebras]
app_closed [in ImpAlg.ImplicativeAlgebras]
app_CBA [in ImpAlg.BooleanAlgebras]
app_min [in ImpAlg.ImplicativeStructures]
app_eta [in ImpAlg.ImplicativeStructures]
app_beta [in ImpAlg.ImplicativeStructures]
app_mon [in ImpAlg.ImplicativeStructures]
app_mon_r [in ImpAlg.ImplicativeStructures]
app_mon_l [in ImpAlg.ImplicativeStructures]
arrow_entails_mon [in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_l [in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_r [in ImpAlg.ImplicativeAlgebras]
arrow_bot [in ImpAlg.ImplicativeStructures]
arrow_prenex [in ImpAlg.ImplicativeStructures]
arrow_mon [in ImpAlg.ImplicativeStructures]
B
BA_cc [in ImpAlg.BooleanAlgebras]BA_S [in ImpAlg.BooleanAlgebras]
BA_K [in ImpAlg.BooleanAlgebras]
betarule [in ImpAlg.ImplicativeStructures]
beta_cvar [in ImpAlg.Lambda]
beta_subst [in ImpAlg.Lambda]
beta_subst_n [in ImpAlg.Lambda]
beta_red [in ImpAlg.ImplicativeStructures]
bot_meet [in ImpAlg.BooleanAlgebras]
by_refl [in ImpAlg.Lattices]
C
CCreal [in ImpAlg.AKS]cc_polymorph [in ImpAlg.Lambda]
codom_concat [in ImpAlg.Lambda]
codom_push [in ImpAlg.Lambda]
codom_single [in ImpAlg.Lambda]
codom_empty [in ImpAlg.Lambda]
combinator_trm_translated [in ImpAlg.Combinators]
combinator_comb [in ImpAlg.Combinators]
composition [in ImpAlg.ImplicativeAlgebras]
contraposition_r [in ImpAlg.ImplicativeAlgebras]
contraposition_l [in ImpAlg.ImplicativeAlgebras]
D
dn [in ImpAlg.ImplicativeAlgebras]dne [in ImpAlg.ImplicativeAlgebras]
dni [in ImpAlg.ImplicativeAlgebras]
double_meet_elim [in ImpAlg.Lattices]
double_meet [in ImpAlg.Lattices]
double_neg [in ImpAlg.BooleanAlgebras]
dummy_top_abs [in ImpAlg.Dummies]
dummy_top_app [in ImpAlg.Dummies]
E
empty_eq [in ImpAlg.Lambda]empty_fv_typ_subst [in ImpAlg.Adequacy]
empty_fv_trm_subst [in ImpAlg.Adequacy]
entails_half_adj [in ImpAlg.ImplicativeAlgebras]
entails_trans [in ImpAlg.ImplicativeAlgebras]
entails_refl [in ImpAlg.ImplicativeAlgebras]
equiv_sep [in ImpAlg.ImplicativeAlgebras]
etarule [in ImpAlg.ImplicativeStructures]
exfalso_S [in ImpAlg.ImplicativeAlgebras]
F
fn_typ_type [in ImpAlg.Lambda]fn_typ_type_aux [in ImpAlg.Lambda]
fn_typ_fall [in ImpAlg.Lambda]
fn_typ_fall_aux [in ImpAlg.Lambda]
fn_typ_fall_Aux [in ImpAlg.Lambda]
fn_typ_arrow [in ImpAlg.Lambda]
fn_typ_fall_bvar [in ImpAlg.Lambda]
fn_trm_term [in ImpAlg.Lambda]
fn_trm_term_aux [in ImpAlg.Lambda]
fn_trm_abs [in ImpAlg.Lambda]
fn_trm_abs_aux [in ImpAlg.Lambda]
fn_trm_abs_Aux [in ImpAlg.Lambda]
fn_trm_app [in ImpAlg.Lambda]
from_list_nil_inv [in ImpAlg.Lambda]
from_list_app [in ImpAlg.Lambda]
fv_open_trm [in ImpAlg.Lambda]
fv_trm_subst [in ImpAlg.Lambda]
fv_typ_subst [in ImpAlg.Adequacy]
G
geq_S_S [in ImpAlg.Lambda]geq_1_S [in ImpAlg.Lambda]
glb_elim_intro [in ImpAlg.Lattices]
glb_unique [in ImpAlg.Lattices]
H
ha_adjunction [in ImpAlg.ImplicativeAlgebras]I
Id_SK [in ImpAlg.Combinators]II_neq_I [in ImpAlg.Dummies]
imp_meet [in ImpAlg.HeytingAlgebras]
imp_is_join [in ImpAlg.HeytingAlgebras]
imp_mon_r [in ImpAlg.HeytingAlgebras]
imp_mon_l [in ImpAlg.HeytingAlgebras]
imp_adj [in ImpAlg.HeytingAlgebras]
imp_lub [in ImpAlg.HeytingAlgebras]
imp_intro [in ImpAlg.HeytingAlgebras]
imp_self [in ImpAlg.HeytingAlgebras]
imp_elim [in ImpAlg.HeytingAlgebras]
imp_betared [in ImpAlg.Adequacy]
imp_betared_n [in ImpAlg.Adequacy]
inf_comm [in ImpAlg.Lattices]
inf_comm_aux [in ImpAlg.Lattices]
inf_elim_trans [in ImpAlg.Lattices]
Intersection_set_glb [in ImpAlg.Powerset]
Intersection_set_lb [in ImpAlg.Powerset]
Intersection_included [in ImpAlg.Powerset]
Intersection_idempotent [in ImpAlg.Powerset]
Intersection_absorptive [in ImpAlg.Powerset]
Intersection_associative [in ImpAlg.Powerset]
Intersection_sym [in ImpAlg.Powerset]
I_neq_SKK_dum [in ImpAlg.Dummies]
J
join_same_set [in ImpAlg.Lattices]join_subset [in ImpAlg.Lattices]
join_elim_trans [in ImpAlg.Lattices]
join_set_lub [in ImpAlg.Lattices]
join_emptyset [in ImpAlg.Lattices]
join_top_r [in ImpAlg.Lattices]
join_top_l [in ImpAlg.Lattices]
join_bot_r [in ImpAlg.Lattices]
join_bot_l [in ImpAlg.Lattices]
join_meet_completeness [in ImpAlg.Lattices]
join_mon_r [in ImpAlg.Lattices]
join_mon_l [in ImpAlg.Lattices]
join_lub [in ImpAlg.Lattices]
join_ub_r [in ImpAlg.Lattices]
join_ub_l [in ImpAlg.Lattices]
join_consistent [in ImpAlg.Lattices]
join_meet_set [in ImpAlg.BooleanAlgebras]
K
Kreal [in ImpAlg.AKS]L
lambda_B [in ImpAlg.Combinators]lambda_Easy [in ImpAlg.Combinators]
lambda_W [in ImpAlg.Combinators]
lambda_S [in ImpAlg.Combinators]
lambda_K [in ImpAlg.Combinators]
lambda_Id [in ImpAlg.Combinators]
lub_elim_intro [in ImpAlg.Lattices]
lub_unique [in ImpAlg.Lattices]
M
map_pred_S [in ImpAlg.Lambda]map_pred_app [in ImpAlg.Lambda]
map_pred_cons [in ImpAlg.Lambda]
meet_same_set [in ImpAlg.Lattices]
meet_same_set_le [in ImpAlg.Lattices]
meet_subset [in ImpAlg.Lattices]
meet_fam_intro [in ImpAlg.Lattices]
meet_fam_elim [in ImpAlg.Lattices]
meet_comm [in ImpAlg.Lattices]
meet_comm_aux [in ImpAlg.Lattices]
meet_elim_trans [in ImpAlg.Lattices]
meet_set_glb [in ImpAlg.Lattices]
meet_emptyset [in ImpAlg.Lattices]
meet_top_r [in ImpAlg.Lattices]
meet_top_l [in ImpAlg.Lattices]
meet_bot_r [in ImpAlg.Lattices]
meet_bot_l [in ImpAlg.Lattices]
meet_join_completeness [in ImpAlg.Lattices]
meet_mon_r [in ImpAlg.Lattices]
meet_mon_l [in ImpAlg.Lattices]
meet_glb [in ImpAlg.Lattices]
meet_lb_r [in ImpAlg.Lattices]
meet_lb_l [in ImpAlg.Lattices]
meet_join [in ImpAlg.Lattices]
meet_join_set [in ImpAlg.BooleanAlgebras]
modus_ponens_later [in ImpAlg.ImplicativeAlgebras]
mod_ponens [in ImpAlg.ImplicativeAlgebras]
mod_pon_app [in ImpAlg.ImplicativeStructures]
N
neg_join_set [in ImpAlg.BooleanAlgebras]neg_meet_set [in ImpAlg.BooleanAlgebras]
neg_mon [in ImpAlg.BooleanAlgebras]
neg_meet [in ImpAlg.BooleanAlgebras]
neg_join [in ImpAlg.BooleanAlgebras]
neg_bot [in ImpAlg.BooleanAlgebras]
neg_top [in ImpAlg.BooleanAlgebras]
neg_complement [in ImpAlg.BooleanAlgebras]
O
open_trm_term [in ImpAlg.Lambda]open_typ_com_ct [in ImpAlg.Lambda]
open_typ_com_ff [in ImpAlg.Lambda]
open_typ_com_cc [in ImpAlg.Lambda]
open_typ_com_cf [in ImpAlg.Lambda]
open_typ_type [in ImpAlg.Lambda]
open_typ_fn [in ImpAlg.Lambda]
open_trm_com_v [in ImpAlg.Lambda]
open_trm_com_ct [in ImpAlg.Lambda]
open_term [in ImpAlg.Lambda]
open_trm_fn [in ImpAlg.Lambda]
open_trm_def [in ImpAlg.Lambda]
P
pre_upclosed_rev [in ImpAlg.Lattices]prodt_intro [in ImpAlg.ImplicativeAlgebras]
prodt_r [in ImpAlg.ImplicativeAlgebras]
prodt_l [in ImpAlg.ImplicativeAlgebras]
R
realizer_later [in ImpAlg.ImplicativeAlgebras]realize_update [in ImpAlg.Adequacy]
realize_inv [in ImpAlg.Adequacy]
remove_pred_0 [in ImpAlg.Lambda]
remove_pred [in ImpAlg.Lambda]
remove_comm [in ImpAlg.Lambda]
remove_0_def [in ImpAlg.Lambda]
remove_app [in ImpAlg.Lambda]
remove_0_incl [in ImpAlg.Lambda]
remove_0_cons_0 [in ImpAlg.Lambda]
revinc_orth [in ImpAlg.AKS]
rev_consistent [in ImpAlg.Lattices]
rev_trans [in ImpAlg.Lattices]
rev_antisym [in ImpAlg.Lattices]
rev_refl [in ImpAlg.Lattices]
S
same_set_sym [in ImpAlg.Lattices]sclosed_translated [in ImpAlg.ImplicativeAlgebras]
sclosed_translated_n [in ImpAlg.ImplicativeAlgebras]
sep_Easy [in ImpAlg.ImplicativeAlgebras]
sep_W [in ImpAlg.ImplicativeAlgebras]
sep_typ [in ImpAlg.ImplicativeAlgebras]
sep_sclosed [in ImpAlg.ImplicativeAlgebras]
sep_term [in ImpAlg.ImplicativeAlgebras]
sep_comb [in ImpAlg.ImplicativeAlgebras]
sep_Id [in ImpAlg.ImplicativeAlgebras]
size_typ_arrow_le_r [in ImpAlg.Lambda]
size_typ_arrow_le_l [in ImpAlg.Lambda]
size_typ_arrow [in ImpAlg.Lambda]
size_typ_plus_S [in ImpAlg.Lambda]
size_typ_S [in ImpAlg.Lambda]
size_typ_open_f [in ImpAlg.Lambda]
size_typ_open [in ImpAlg.Lambda]
size_typ_le_1 [in ImpAlg.Lambda]
size_typ_ind [in ImpAlg.Lambda]
size_typ_ind_gen [in ImpAlg.Lambda]
size_typ_induction [in ImpAlg.Lambda]
size_typ_not_0 [in ImpAlg.Lambda]
size_plus_S [in ImpAlg.Lambda]
size_S [in ImpAlg.Lambda]
size_app_le_r [in ImpAlg.Lambda]
size_app_le_l [in ImpAlg.Lambda]
size_open_v [in ImpAlg.Lambda]
size_open_c [in ImpAlg.Lambda]
size_le_1 [in ImpAlg.Lambda]
size_ind [in ImpAlg.Lambda]
size_ind_gen [in ImpAlg.Lambda]
size_induction [in ImpAlg.Lambda]
size_not_0 [in ImpAlg.Lambda]
Sreal [in ImpAlg.AKS]
sterm_term [in ImpAlg.Combinators]
subset_trans [in ImpAlg.Lambda]
subst_term [in ImpAlg.Lambda]
subst_intro [in ImpAlg.Lambda]
subst_open_var [in ImpAlg.Lambda]
subst_open [in ImpAlg.Lambda]
subst_fresh [in ImpAlg.Lambda]
subst_trm_update [in ImpAlg.Adequacy]
subst_trm_update_open [in ImpAlg.Adequacy]
subst_typ_update [in ImpAlg.Adequacy]
subst_typ_var [in ImpAlg.Adequacy]
subst_closed [in ImpAlg.Adequacy]
subst_trm_var [in ImpAlg.Adequacy]
subtyping [in ImpAlg.ImplicativeAlgebras]
sumt_elim [in ImpAlg.ImplicativeAlgebras]
sumt_r [in ImpAlg.ImplicativeAlgebras]
sumt_l [in ImpAlg.ImplicativeAlgebras]
T
term_subst [in ImpAlg.Lambda]term_subst_n [in ImpAlg.Lambda]
top_join [in ImpAlg.BooleanAlgebras]
translated_comb [in ImpAlg.Combinators]
translated_Easy [in ImpAlg.Combinators]
translated_W [in ImpAlg.Combinators]
translated_S [in ImpAlg.Combinators]
translated_K [in ImpAlg.Combinators]
translated_Id [in ImpAlg.Combinators]
translated_peirce [in ImpAlg.Adequacy]
translated_typ_unique [in ImpAlg.Adequacy]
translated_subst [in ImpAlg.Adequacy]
translated_subst_n [in ImpAlg.Adequacy]
translated_term [in ImpAlg.Adequacy]
translated_term_n [in ImpAlg.Adequacy]
translated_abs_inv [in ImpAlg.Adequacy]
translated_unique [in ImpAlg.Adequacy]
translated_closed [in ImpAlg.Adequacy]
trans_typ_open [in ImpAlg.Adequacy]
trans_typ_update [in ImpAlg.Adequacy]
trans_typ_correct [in ImpAlg.Adequacy]
trans_typ_var [in ImpAlg.Adequacy]
trans_typ_arrow [in ImpAlg.Adequacy]
trans_typ_fold [in ImpAlg.Adequacy]
trans_typ_fioul [in ImpAlg.Adequacy]
trans_typ_fall [in ImpAlg.Adequacy]
trans_correct [in ImpAlg.Adequacy]
trans_trm_var [in ImpAlg.Adequacy]
trans_trm_abs [in ImpAlg.Adequacy]
trans_trm_app [in ImpAlg.Adequacy]
trans_trm_fold [in ImpAlg.Adequacy]
trans_trm_fioul [in ImpAlg.Adequacy]
trans_trm_fioul_aux [in ImpAlg.Adequacy]
true_S [in ImpAlg.ImplicativeAlgebras]
type_case [in ImpAlg.ImplicativeAlgebras]
type_inj2 [in ImpAlg.ImplicativeAlgebras]
type_inj1 [in ImpAlg.ImplicativeAlgebras]
type_proj2 [in ImpAlg.ImplicativeAlgebras]
type_proj1 [in ImpAlg.ImplicativeAlgebras]
type_pair [in ImpAlg.ImplicativeAlgebras]
type_ex_elim [in ImpAlg.ImplicativeAlgebras]
type_ex_intro [in ImpAlg.ImplicativeAlgebras]
type_fa_elim [in ImpAlg.ImplicativeAlgebras]
type_fa_intro [in ImpAlg.ImplicativeAlgebras]
type_subst [in ImpAlg.Lambda]
type_peirce [in ImpAlg.Lambda]
typing_empty_closed [in ImpAlg.Lambda]
typing_fv_trm [in ImpAlg.Lambda]
typing_fv_trm_aux [in ImpAlg.Lambda]
typing_term [in ImpAlg.Lambda]
typing_type [in ImpAlg.Lambda]
typing_subst_trm [in ImpAlg.Adequacy]
typ_eq_subst [in ImpAlg.Lambda]
U
Union_set_lub [in ImpAlg.Powerset]Union_set_ub [in ImpAlg.Powerset]
Union_idempotent [in ImpAlg.Powerset]
Union_absorptive [in ImpAlg.Powerset]
Union_associative [in ImpAlg.Powerset]
Union_sym [in ImpAlg.Powerset]
union_empty [in ImpAlg.Lambda]
V
var_eq_dec [in ImpAlg.Lambda]Axiom Index
C
combinatory_completeness [in ImpAlg.Combinators]Constructor Index
B
betared_abs [in ImpAlg.Lambda]betared_app2 [in ImpAlg.Lambda]
betared_app1 [in ImpAlg.Lambda]
betared_red [in ImpAlg.Lambda]
C
combApp [in ImpAlg.Combinators]combCC [in ImpAlg.Combinators]
combK [in ImpAlg.Combinators]
combS [in ImpAlg.Combinators]
comb_app [in ImpAlg.Combinators]
comb_cc [in ImpAlg.Combinators]
comb_Id [in ImpAlg.Combinators]
comb_K [in ImpAlg.Combinators]
comb_S [in ImpAlg.Combinators]
R
real_push [in ImpAlg.Adequacy]real_empty [in ImpAlg.Adequacy]
S
sterm_cc [in ImpAlg.Combinators]sterm_app [in ImpAlg.Combinators]
sterm_abs [in ImpAlg.Combinators]
sterm_var [in ImpAlg.Combinators]
stype_arrow [in ImpAlg.Lambda]
stype_fall [in ImpAlg.Lambda]
stype_fvar [in ImpAlg.Lambda]
T
term_cc [in ImpAlg.Lambda]term_app [in ImpAlg.Lambda]
term_abs [in ImpAlg.Lambda]
term_cvar [in ImpAlg.Lambda]
term_var [in ImpAlg.Lambda]
trm_cc [in ImpAlg.Lambda]
trm_app [in ImpAlg.Lambda]
trm_abs [in ImpAlg.Lambda]
trm_cvar [in ImpAlg.Lambda]
trm_fvar [in ImpAlg.Lambda]
trm_bvar [in ImpAlg.Lambda]
tr_typ_fall [in ImpAlg.Adequacy]
tr_typ_arrow [in ImpAlg.Adequacy]
tr_typ_var [in ImpAlg.Adequacy]
tr_cc [in ImpAlg.Adequacy]
tr_app [in ImpAlg.Adequacy]
tr_abs [in ImpAlg.Adequacy]
tr_cvar [in ImpAlg.Adequacy]
type_arrow [in ImpAlg.Lambda]
type_fall [in ImpAlg.Lambda]
type_cvar [in ImpAlg.Lambda]
type_fvar [in ImpAlg.Lambda]
typing_cc [in ImpAlg.Lambda]
typing_fallE [in ImpAlg.Lambda]
typing_fallI [in ImpAlg.Lambda]
typing_app [in ImpAlg.Lambda]
typing_abs [in ImpAlg.Lambda]
typing_prf_var [in ImpAlg.Lambda]
typ_arrow [in ImpAlg.Lambda]
typ_fall [in ImpAlg.Lambda]
typ_cvar [in ImpAlg.Lambda]
typ_fvar [in ImpAlg.Lambda]
typ_bvar [in ImpAlg.Lambda]
Inductive Index
B
betared [in ImpAlg.Lambda]C
comb [in ImpAlg.Combinators]combinator [in ImpAlg.Combinators]
R
realize [in ImpAlg.Adequacy]S
sterm [in ImpAlg.Combinators]stype [in ImpAlg.Lambda]
T
term [in ImpAlg.Lambda]translated [in ImpAlg.Adequacy]
translated_typ [in ImpAlg.Adequacy]
trm [in ImpAlg.Lambda]
typ [in ImpAlg.Lambda]
type [in ImpAlg.Lambda]
typing_trm [in ImpAlg.Lambda]
Projection Index
A
app [in ImpAlg.AKS]app [in ImpAlg.OCA]
app_mon [in ImpAlg.OCA]
arrow [in ImpAlg.ImplicativeStructures]
arrow_meet [in ImpAlg.ImplicativeStructures]
arrow_mon_r [in ImpAlg.ImplicativeStructures]
arrow_mon_l [in ImpAlg.ImplicativeStructures]
B
bot [in ImpAlg.Lattices]bot_min [in ImpAlg.Lattices]
C
cc [in ImpAlg.AKS]consistent [in ImpAlg.Lattices]
cont [in ImpAlg.AKS]
I
imp [in ImpAlg.HeytingAlgebras]imp_sup [in ImpAlg.HeytingAlgebras]
J
join [in ImpAlg.Lattices]join_intro [in ImpAlg.Lattices]
join_elim [in ImpAlg.Lattices]
join_set [in ImpAlg.Lattices]
join_idempotent [in ImpAlg.Lattices]
join_absorptive [in ImpAlg.Lattices]
join_associative [in ImpAlg.Lattices]
join_commutative [in ImpAlg.Lattices]
join_neg [in ImpAlg.BooleanAlgebras]
join_distributive [in ImpAlg.BooleanAlgebras]
K
k [in ImpAlg.AKS]k [in ImpAlg.OCA]
k_red [in ImpAlg.OCA]
M
meet [in ImpAlg.Lattices]meet_intro [in ImpAlg.Lattices]
meet_elim [in ImpAlg.Lattices]
meet_set [in ImpAlg.Lattices]
meet_idempotent [in ImpAlg.Lattices]
meet_absorptive [in ImpAlg.Lattices]
meet_associative [in ImpAlg.Lattices]
meet_commutative [in ImpAlg.Lattices]
meet_neg [in ImpAlg.BooleanAlgebras]
meet_distributive [in ImpAlg.BooleanAlgebras]
modus_ponens [in ImpAlg.ImplicativeAlgebras]
N
neg [in ImpAlg.BooleanAlgebras]O
ord [in ImpAlg.Lattices]ord_trans [in ImpAlg.Lattices]
ord_antisym [in ImpAlg.Lattices]
ord_refl [in ImpAlg.Lattices]
P
PL [in ImpAlg.AKS]PL_app_closed [in ImpAlg.AKS]
PL_cc [in ImpAlg.AKS]
PL_k [in ImpAlg.AKS]
PL_s [in ImpAlg.AKS]
pole [in ImpAlg.AKS]
push [in ImpAlg.AKS]
R
red_cont [in ImpAlg.AKS]red_cc [in ImpAlg.AKS]
red_s [in ImpAlg.AKS]
red_k [in ImpAlg.AKS]
red_push [in ImpAlg.AKS]
S
s [in ImpAlg.AKS]s [in ImpAlg.OCA]
separator [in ImpAlg.ImplicativeAlgebras]
sep_cc [in ImpAlg.ImplicativeAlgebras]
sep_S [in ImpAlg.ImplicativeAlgebras]
sep_K [in ImpAlg.ImplicativeAlgebras]
s_red [in ImpAlg.OCA]
T
top [in ImpAlg.Lattices]top_max [in ImpAlg.Lattices]
U
up_closed [in ImpAlg.ImplicativeAlgebras]Section Index
A
Adequacy [in ImpAlg.Adequacy]C
Combinators [in ImpAlg.Combinators]D
Definitions [in ImpAlg.Lambda]Dummy [in ImpAlg.Dummies]
I
IA [in ImpAlg.ImplicativeAlgebras]P
Powerset [in ImpAlg.Powerset]Instance Index
A
AKS_IA [in ImpAlg.AKS]AKS_IS [in ImpAlg.AKS]
arrow_set_Proper [in ImpAlg.ImplicativeStructures]
B
BA_HA [in ImpAlg.BooleanAlgebras]C
CBA_IA [in ImpAlg.BooleanAlgebras]CBA_IS [in ImpAlg.BooleanAlgebras]
CBA_CHA [in ImpAlg.BooleanAlgebras]
CBL [in ImpAlg.Lattices]
CHA_IS [in ImpAlg.HeytingAlgebras]
D
dummy_imp_top [in ImpAlg.Dummies]dummy_imp_r [in ImpAlg.Dummies]
J
join_set_Proper [in ImpAlg.Lattices]M
meet_set_Proper [in ImpAlg.Lattices]O
OCA_IS [in ImpAlg.OCA]ord_Antisymmetric [in ImpAlg.Lattices]
ord_Transitive [in ImpAlg.Lattices]
ord_Reflexive [in ImpAlg.Lattices]
P
Powerset_CompleteLattice [in ImpAlg.Powerset]Powerset_Lattice [in ImpAlg.Powerset]
Powerset_Order [in ImpAlg.Powerset]
Definition Index
A
abs [in ImpAlg.ImplicativeStructures]anti_mon [in ImpAlg.Lattices]
app [in ImpAlg.ImplicativeStructures]
app_closure [in ImpAlg.ImplicativeStructures]
arrow [in ImpAlg.AKS]
arrowtop [in ImpAlg.Dummies]
arrow_r [in ImpAlg.Dummies]
arrow_set [in ImpAlg.ImplicativeStructures]
arrow_set_r [in ImpAlg.ImplicativeStructures]
arrow_set_l [in ImpAlg.ImplicativeStructures]
B
B [in ImpAlg.Combinators]body [in ImpAlg.Lambda]
C
carreer [in ImpAlg.OCA]case [in ImpAlg.ImplicativeAlgebras]
cc [in ImpAlg.Adequacy]
closed [in ImpAlg.Lambda]
closed_typ [in ImpAlg.ImplicativeAlgebras]
closed_typ [in ImpAlg.Lambda]
codom [in ImpAlg.Combinators]
codom [in ImpAlg.ImplicativeAlgebras]
codom [in ImpAlg.Lambda]
compat_app [in ImpAlg.Lambda]
E
Easy [in ImpAlg.Combinators]empty [in ImpAlg.Lambda]
emptyset [in ImpAlg.Lattices]
Ens [in ImpAlg.Lattices]
entails [in ImpAlg.ImplicativeAlgebras]
env [in ImpAlg.Combinators]
env [in ImpAlg.ImplicativeAlgebras]
env [in ImpAlg.Lambda]
equivalence [in ImpAlg.ImplicativeAlgebras]
eta [in ImpAlg.ImplicativeStructures]
existst [in ImpAlg.ImplicativeAlgebras]
ex_term [in ImpAlg.ImplicativeAlgebras]
F
fn_typ [in ImpAlg.Lambda]fn_typ_aux [in ImpAlg.Lambda]
fn_trm [in ImpAlg.Lambda]
fn_trm_aux [in ImpAlg.Lambda]
forallt [in ImpAlg.ImplicativeAlgebras]
fv_typ [in ImpAlg.Combinators]
fv_trm [in ImpAlg.Combinators]
fv_typ [in ImpAlg.ImplicativeAlgebras]
fv_trm [in ImpAlg.ImplicativeAlgebras]
fv_typ [in ImpAlg.Lambda]
fv_trm [in ImpAlg.Lambda]
G
glb [in ImpAlg.Lattices]I
Id [in ImpAlg.Combinators]Idum [in ImpAlg.Dummies]
image_set [in ImpAlg.Lattices]
imp_comb [in ImpAlg.Combinators]
inf [in ImpAlg.Lattices]
inj1 [in ImpAlg.ImplicativeAlgebras]
inj2 [in ImpAlg.ImplicativeAlgebras]
Intersection_set [in ImpAlg.Powerset]
in_list [in ImpAlg.Lambda]
J
join_family [in ImpAlg.Lattices]join_complete [in ImpAlg.Lattices]
K
K [in ImpAlg.Combinators]Kdum [in ImpAlg.Dummies]
L
lambdaB [in ImpAlg.Combinators]lambdaEasy [in ImpAlg.Combinators]
lambdaId [in ImpAlg.Combinators]
lambdaK [in ImpAlg.Combinators]
lambdaS [in ImpAlg.Combinators]
lambdaW [in ImpAlg.Combinators]
lb [in ImpAlg.Lattices]
lub [in ImpAlg.Lattices]
M
map_pred [in ImpAlg.Lambda]meet_family [in ImpAlg.Lattices]
meet_complete [in ImpAlg.Lattices]
min [in ImpAlg.Lattices]
mod_pon_closure [in ImpAlg.ImplicativeStructures]
N
neg [in ImpAlg.ImplicativeAlgebras]O
open_typ_fvar [in ImpAlg.Lambda]open_typ [in ImpAlg.Lambda]
open_rec_typ [in ImpAlg.Lambda]
open_trm_var [in ImpAlg.Lambda]
open_trm [in ImpAlg.Lambda]
open_rec_trm [in ImpAlg.Lambda]
orth [in ImpAlg.AKS]
P
pair [in ImpAlg.ImplicativeAlgebras]preimage [in ImpAlg.Lattices]
preimage_set [in ImpAlg.Lattices]
prodt [in ImpAlg.ImplicativeAlgebras]
proj1 [in ImpAlg.ImplicativeAlgebras]
proj2 [in ImpAlg.ImplicativeAlgebras]
R
realize [in ImpAlg.OCA]remove [in ImpAlg.Lambda]
remove_0 [in ImpAlg.Lambda]
rev [in ImpAlg.Lattices]
RevBooleanAlgebra [in ImpAlg.BooleanAlgebras]
RevBoundedLattice [in ImpAlg.Lattices]
RevCompleteBooleanAlgebra [in ImpAlg.BooleanAlgebras]
RevCompleteLattice [in ImpAlg.Lattices]
reverse [in ImpAlg.Lattices]
revinc [in ImpAlg.AKS]
RevLattice [in ImpAlg.Lattices]
RevOrd [in ImpAlg.Lattices]
S
S [in ImpAlg.Combinators]same_set [in ImpAlg.Lattices]
sclosed [in ImpAlg.Combinators]
Sdum [in ImpAlg.Dummies]
size [in ImpAlg.Lambda]
size_typ [in ImpAlg.Lambda]
subset [in ImpAlg.Lattices]
subst [in ImpAlg.Lambda]
substitution [in ImpAlg.Adequacy]
subst_trm [in ImpAlg.Lambda]
subst_typ [in ImpAlg.Adequacy]
subst_trm [in ImpAlg.Adequacy]
Succ [in ImpAlg.Combinators]
sumt [in ImpAlg.ImplicativeAlgebras]
sup [in ImpAlg.Lattices]
T
trans_typ [in ImpAlg.Adequacy]trans_typ_aux [in ImpAlg.Adequacy]
trans_trm [in ImpAlg.Adequacy]
trans_trm_aux [in ImpAlg.Adequacy]
trm_comb [in ImpAlg.Combinators]
typ_peirce [in ImpAlg.Lambda]
U
ub [in ImpAlg.Lattices]Union_set [in ImpAlg.Powerset]
update [in ImpAlg.Adequacy]
upwards_closure [in ImpAlg.ImplicativeStructures]
up_closed_set [in ImpAlg.Lattices]
W
W [in ImpAlg.Combinators]Record Index
A
AKS [in ImpAlg.AKS]B
BooleanAlgebra [in ImpAlg.BooleanAlgebras]BoundedLattice [in ImpAlg.Lattices]
C
CompleteBooleanAlgebra [in ImpAlg.BooleanAlgebras]CompleteHeytingAlgebra [in ImpAlg.HeytingAlgebras]
CompleteLattice [in ImpAlg.Lattices]
H
HeytingAlgebra [in ImpAlg.HeytingAlgebras]I
ImplicativeAlgebra [in ImpAlg.ImplicativeAlgebras]ImplicativeStructure [in ImpAlg.ImplicativeStructures]
L
Lattice [in ImpAlg.Lattices]O
OCA [in ImpAlg.OCA]Order [in ImpAlg.Lattices]
| 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 | (676 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 | (58 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 | (12 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 | (309 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (55 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 | (13 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 | (65 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 | (6 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 | (20 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 | (125 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 | (12 entries) |