| 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 | (337 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 | (6 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 | (165 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 | (57 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 | (17 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 | (9 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 | (31 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 | (5 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 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
AllF [constructor, in SysF_PTS.sysf]AppF [constructor, in SysF_PTS.sysf]
AppL [constructor, in SysF_PTS.lambda2]
atn [inductive, in SysF_PTS.lib]
atnd [inductive, in SysF_PTS.lib]
AtndS [constructor, in SysF_PTS.lib]
atnd_type_eqPrp_f [lemma, in SysF_PTS.lambda2]
atnd_notPrp_eqPrp_f [lemma, in SysF_PTS.lambda2]
atnd_eqPrp_t [lemma, in SysF_PTS.lambda2]
atnd_getD [lemma, in SysF_PTS.lib]
Atnd0 [constructor, in SysF_PTS.lib]
AtnS [constructor, in SysF_PTS.lib]
atn_mmap [lemma, in SysF_PTS.lib]
atn_get [lemma, in SysF_PTS.lib]
Atn0 [constructor, in SysF_PTS.lib]
B
bfr [definition, in SysF_PTS.lib]bfr_ushift [lemma, in SysF_PTS.lib]
bfr_shift [lemma, in SysF_PTS.lib]
bfr_up [lemma, in SysF_PTS.lib]
bind [projection, in SysF_PTS.lib]
C
cm_typingL_beta [lemma, in SysF_PTS.lambda2]cm_typingL_id [lemma, in SysF_PTS.lambda2]
cm_typingL_up [lemma, in SysF_PTS.lambda2]
cm_typingL [definition, in SysF_PTS.lambda2]
cm_typingP_beta_type [lemma, in SysF_PTS.lambda2]
cm_typingP_beta_term [lemma, in SysF_PTS.lambda2]
cm_typingP_up [lemma, in SysF_PTS.lambda2]
cm_typingP [definition, in SysF_PTS.lambda2]
cm_istyP_beta_term [lemma, in SysF_PTS.lambda2]
cm_istyP_beta_type [lemma, in SysF_PTS.lambda2]
cm_istyP_up [lemma, in SysF_PTS.lambda2]
cm_istyP [definition, in SysF_PTS.lambda2]
cm_typingL_nat_beta [lemma, in SysF_PTS.lambda2]
cm_typingL_nat_id [lemma, in SysF_PTS.lambda2]
cm_typingL_nat_up [lemma, in SysF_PTS.lambda2]
cm_typingL_nat [definition, in SysF_PTS.lambda2]
cm_tyrel_beta [lemma, in SysF_PTS.RelEquiv]
cm_tyrel_ext [lemma, in SysF_PTS.RelEquiv]
cm_tyrel_rs [lemma, in SysF_PTS.RelEquiv]
cm_tyrel [definition, in SysF_PTS.RelEquiv]
cm_istyF_beta [lemma, in SysF_PTS.sysf]
cm_istyF_up [lemma, in SysF_PTS.sysf]
cm_istyF [definition, in SysF_PTS.sysf]
Coincidence [section, in SysF_PTS.lib]
CoincidenceHSubst [section, in SysF_PTS.lib]
comb [definition, in SysF_PTS.lib]
comb_comp [lemma, in SysF_PTS.lib]
comb_cons [lemma, in SysF_PTS.lib]
ContextRenamings [section, in SysF_PTS.lib]
Countable [record, in SysF_PTS.Decidable]
countableProp [projection, in SysF_PTS.Decidable]
cr [definition, in SysF_PTS.lib]
cr_typingP_shift [lemma, in SysF_PTS.lambda2]
cr_typingP_up [lemma, in SysF_PTS.lambda2]
cr_typingP [definition, in SysF_PTS.lambda2]
cr_cm_istyP [lemma, in SysF_PTS.lambda2]
cr_istyP_ushift [lemma, in SysF_PTS.lambda2]
cr_istyP_shift [lemma, in SysF_PTS.lambda2]
cr_istyP_up_id [lemma, in SysF_PTS.lambda2]
cr_istyP_up [lemma, in SysF_PTS.lambda2]
cr_istyP_id [lemma, in SysF_PTS.lambda2]
cr_cr_istyP [lemma, in SysF_PTS.lambda2]
cr_istyP [definition, in SysF_PTS.lambda2]
cr_typingL_shift [lemma, in SysF_PTS.lambda2]
cr_typingL_up [lemma, in SysF_PTS.lambda2]
cr_typingL [definition, in SysF_PTS.lambda2]
cr_shift [lemma, in SysF_PTS.lib]
cr_up [lemma, in SysF_PTS.lib]
cr_typingF_shift [lemma, in SysF_PTS.sysf]
cr_typingF_ren_ushift [lemma, in SysF_PTS.sysf]
cr_typingF_ren [lemma, in SysF_PTS.sysf]
cr_typingF_up [lemma, in SysF_PTS.sysf]
cr_typingF_id [lemma, in SysF_PTS.sysf]
cr_typingF [definition, in SysF_PTS.sysf]
cr_istyF_ushift [lemma, in SysF_PTS.sysf]
cr_istyF_shift [lemma, in SysF_PTS.sysf]
cr_istyF_up [lemma, in SysF_PTS.sysf]
cr_istyF_id [lemma, in SysF_PTS.sysf]
cr_istyF [definition, in SysF_PTS.sysf]
CtxBoolFun [section, in SysF_PTS.lib]
D
Dec [record, in SysF_PTS.Decidable]Dec [inductive, in SysF_PTS.Decidable]
dec [abbreviation, in SysF_PTS.Decidable]
Decidable [library]
decidable_neg [instance, in SysF_PTS.Decidable]
decide [projection, in SysF_PTS.Decidable]
decide [constructor, in SysF_PTS.Decidable]
decide_eq_termL [instance, in SysF_PTS.lambda2]
decide_eq_level [instance, in SysF_PTS.lambda2]
decide_eq_fin_domain [lemma, in SysF_PTS.Decidable]
decide_refl [lemma, in SysF_PTS.lib]
decide_eq_termF [instance, in SysF_PTS.sysf]
decide_eq_typeF [instance, in SysF_PTS.sysf]
Dec_eq_fin_domain [instance, in SysF_PTS.Decidable]
Dec_fin_quant [instance, in SysF_PTS.Decidable]
Dec_fin_quant_T [instance, in SysF_PTS.Decidable]
Dec_impl [instance, in SysF_PTS.Decidable]
Dec_or [instance, in SysF_PTS.Decidable]
Dec_and [instance, in SysF_PTS.Decidable]
Dec_lt_nat [instance, in SysF_PTS.Decidable]
Dec_le_nat [instance, in SysF_PTS.Decidable]
Dec_eq_option [instance, in SysF_PTS.Decidable]
Dec_eq_nat [instance, in SysF_PTS.Decidable]
E
enum [projection, in SysF_PTS.Decidable]eqPrp [definition, in SysF_PTS.lambda2]
eqPrp_t_subst_t [lemma, in SysF_PTS.lambda2]
eqPrp_ren [lemma, in SysF_PTS.lambda2]
eq_dec [abbreviation, in SysF_PTS.Decidable]
F
Finite [record, in SysF_PTS.Decidable]finiteProp [projection, in SysF_PTS.Decidable]
fmap [projection, in SysF_PTS.lib]
Functor [record, in SysF_PTS.lib]
Functor_Monad [instance, in SysF_PTS.lib]
G
gentypingP [definition, in SysF_PTS.lambda2]gentypingP_typingP [lemma, in SysF_PTS.lambda2]
get [definition, in SysF_PTS.lib]
getD [definition, in SysF_PTS.lib]
getD_cons [lemma, in SysF_PTS.lib]
getD_get [lemma, in SysF_PTS.lib]
getD_atnd [lemma, in SysF_PTS.lib]
get_mmap_None [lemma, in SysF_PTS.lib]
get_mmap [lemma, in SysF_PTS.lib]
get_atn [lemma, in SysF_PTS.lib]
H
HSubstLemmas_termF [instance, in SysF_PTS.sysf]HSubst_termF [instance, in SysF_PTS.sysf]
I
Ids_termL [instance, in SysF_PTS.lambda2]Ids_termF [instance, in SysF_PTS.sysf]
Ids_typeF [instance, in SysF_PTS.sysf]
ImpF [constructor, in SysF_PTS.sysf]
internF [definition, in SysF_PTS.sysf]
internF_correct [lemma, in SysF_PTS.sysf]
internF_ty [definition, in SysF_PTS.sysf]
internL [definition, in SysF_PTS.lambda2]
internLP_correct [lemma, in SysF_PTS.lambda2]
istyF [inductive, in SysF_PTS.sysf]
istyF_beta [lemma, in SysF_PTS.sysf]
istyF_subst [lemma, in SysF_PTS.sysf]
istyF_strengthen [lemma, in SysF_PTS.sysf]
istyF_weaken [lemma, in SysF_PTS.sysf]
istyF_ren [lemma, in SysF_PTS.sysf]
istyF_all [constructor, in SysF_PTS.sysf]
istyF_imp [constructor, in SysF_PTS.sysf]
istyF_var [constructor, in SysF_PTS.sysf]
istyP [inductive, in SysF_PTS.lambda2]
istyP_typingL [lemma, in SysF_PTS.lambda2]
istyP_subst [lemma, in SysF_PTS.lambda2]
istyP_strengthen [lemma, in SysF_PTS.lambda2]
istyP_weaken [lemma, in SysF_PTS.lambda2]
istyP_ren [lemma, in SysF_PTS.lambda2]
istyP_neqPrp [lemma, in SysF_PTS.lambda2]
istyP_notSort [lemma, in SysF_PTS.lambda2]
istyP_prod2 [constructor, in SysF_PTS.lambda2]
istyP_prod1 [constructor, in SysF_PTS.lambda2]
istyP_var [constructor, in SysF_PTS.lambda2]
L
lambda2 [library]LamF [constructor, in SysF_PTS.sysf]
LamL [constructor, in SysF_PTS.lambda2]
level [inductive, in SysF_PTS.lambda2]
lib [library]
M
mmap_get_None [lemma, in SysF_PTS.lib]mmap_get [lemma, in SysF_PTS.lib]
mmap_atn [lemma, in SysF_PTS.lib]
Monad [record, in SysF_PTS.lib]
N
numElems [projection, in SysF_PTS.Decidable]P
ProdL [constructor, in SysF_PTS.lambda2]Prp [constructor, in SysF_PTS.lambda2]
R
RelEquiv [library]Rename_termL [instance, in SysF_PTS.lambda2]
Rename_termF [instance, in SysF_PTS.sysf]
Rename_typeF [instance, in SysF_PTS.sysf]
repr [projection, in SysF_PTS.Decidable]
ret [projection, in SysF_PTS.lib]
S
SortL [constructor, in SysF_PTS.lambda2]sortL_add_subst [lemma, in SysF_PTS.lambda2]
sortL_p1 [lemma, in SysF_PTS.lambda2]
sortL_ren [lemma, in SysF_PTS.lambda2]
sortP_eqPrp_f [lemma, in SysF_PTS.lambda2]
sortP_neq_ren [lemma, in SysF_PTS.lambda2]
SubstHSubstComp_typeF_termF [instance, in SysF_PTS.sysf]
SubstInstance [section, in SysF_PTS.lib]
SubstLemmas_termL [instance, in SysF_PTS.lambda2]
SubstLemmas_termF [instance, in SysF_PTS.sysf]
SubstLemmas_typeF [instance, in SysF_PTS.sysf]
Subst_termL [instance, in SysF_PTS.lambda2]
subst_coinc_hcomp [lemma, in SysF_PTS.lib]
subst_coinc_hd_f [lemma, in SysF_PTS.lib]
subst_coinc_up [lemma, in SysF_PTS.lib]
subst_coinc_id [lemma, in SysF_PTS.lib]
subst_coinc [definition, in SysF_PTS.lib]
Subst_termF [instance, in SysF_PTS.sysf]
Subst_typeF [instance, in SysF_PTS.sysf]
sum2bool [definition, in SysF_PTS.lib]
sysf [library]
T
termF [inductive, in SysF_PTS.sysf]termL [inductive, in SysF_PTS.lambda2]
tmrel [inductive, in SysF_PTS.RelEquiv]
tmrel_lf_total_preserving [lemma, in SysF_PTS.RelEquiv]
tmrel_fl_total_preserving [lemma, in SysF_PTS.RelEquiv]
tmrel_injective [lemma, in SysF_PTS.RelEquiv]
tmrel_functional [lemma, in SysF_PTS.RelEquiv]
tmrel_lf_tot_pres [lemma, in SysF_PTS.RelEquiv]
tmrel_fl_tot_pres [lemma, in SysF_PTS.RelEquiv]
tmrel_inj [lemma, in SysF_PTS.RelEquiv]
tmrel_func [lemma, in SysF_PTS.RelEquiv]
tmrel_tyabs [constructor, in SysF_PTS.RelEquiv]
tmrel_tyspec [constructor, in SysF_PTS.RelEquiv]
tmrel_lam [constructor, in SysF_PTS.RelEquiv]
tmrel_app [constructor, in SysF_PTS.RelEquiv]
tmrel_var [constructor, in SysF_PTS.RelEquiv]
TmVarF [constructor, in SysF_PTS.sysf]
TyAbsF [constructor, in SysF_PTS.sysf]
Typ [constructor, in SysF_PTS.lambda2]
typeF [inductive, in SysF_PTS.sysf]
typingF [inductive, in SysF_PTS.sysf]
typingF_weaken_ty [lemma, in SysF_PTS.sysf]
typingF_ren_ty [lemma, in SysF_PTS.sysf]
typingF_weaken [lemma, in SysF_PTS.sysf]
typingF_ren [lemma, in SysF_PTS.sysf]
typingF_tyabs [constructor, in SysF_PTS.sysf]
typingF_tyspec [constructor, in SysF_PTS.sysf]
typingF_lam [constructor, in SysF_PTS.sysf]
typingF_app [constructor, in SysF_PTS.sysf]
typingF_var [constructor, in SysF_PTS.sysf]
typingL [inductive, in SysF_PTS.lambda2]
typingL_typ_degenerate [lemma, in SysF_PTS.lambda2]
typingL_propagation [lemma, in SysF_PTS.lambda2]
typingL_beta [lemma, in SysF_PTS.lambda2]
typingL_subst [lemma, in SysF_PTS.lambda2]
typingL_sort_strengthen [lemma, in SysF_PTS.lambda2]
typingL_typingP [lemma, in SysF_PTS.lambda2]
typingL_typ_degenerate_nat [lemma, in SysF_PTS.lambda2]
typingL_propagation_nat [lemma, in SysF_PTS.lambda2]
typingL_beta_nat [lemma, in SysF_PTS.lambda2]
typingL_subst_nat [lemma, in SysF_PTS.lambda2]
typingL_weaken [lemma, in SysF_PTS.lambda2]
typingL_ren [lemma, in SysF_PTS.lambda2]
typingL_prp_prp_contra [lemma, in SysF_PTS.lambda2]
typingL_lam [constructor, in SysF_PTS.lambda2]
typingL_app [constructor, in SysF_PTS.lambda2]
typingL_prod [constructor, in SysF_PTS.lambda2]
typingL_var [constructor, in SysF_PTS.lambda2]
typingL_ax [constructor, in SysF_PTS.lambda2]
typingP [inductive, in SysF_PTS.lambda2]
typingPL_equiv [lemma, in SysF_PTS.lambda2]
typingP_typingL [lemma, in SysF_PTS.lambda2]
typingP_istyP [lemma, in SysF_PTS.lambda2]
typingP_beta_type [lemma, in SysF_PTS.lambda2]
typingP_beta_term [lemma, in SysF_PTS.lambda2]
typingP_subst [lemma, in SysF_PTS.lambda2]
typingP_weaken [lemma, in SysF_PTS.lambda2]
typingP_ren [lemma, in SysF_PTS.lambda2]
typingP_lam2 [constructor, in SysF_PTS.lambda2]
typingP_app2 [constructor, in SysF_PTS.lambda2]
typingP_lam1 [constructor, in SysF_PTS.lambda2]
typingP_app1 [constructor, in SysF_PTS.lambda2]
typingP_var [constructor, in SysF_PTS.lambda2]
tyrel [inductive, in SysF_PTS.RelEquiv]
tyrel_lf_total_preserving [lemma, in SysF_PTS.RelEquiv]
tyrel_fl_total_preserving [lemma, in SysF_PTS.RelEquiv]
tyrel_injective [lemma, in SysF_PTS.RelEquiv]
tyrel_functional [lemma, in SysF_PTS.RelEquiv]
tyrel_tmrel_disjoint [lemma, in SysF_PTS.RelEquiv]
tyrel_beta [lemma, in SysF_PTS.RelEquiv]
tyrel_subst [lemma, in SysF_PTS.RelEquiv]
tyrel_unmap [lemma, in SysF_PTS.RelEquiv]
tyrel_weaken_hd [lemma, in SysF_PTS.RelEquiv]
tyrel_weaken [lemma, in SysF_PTS.RelEquiv]
tyrel_ren [lemma, in SysF_PTS.RelEquiv]
tyrel_lf_tot_pres [lemma, in SysF_PTS.RelEquiv]
tyrel_fl_tot_pres [lemma, in SysF_PTS.RelEquiv]
tyrel_inj [lemma, in SysF_PTS.RelEquiv]
tyrel_func [lemma, in SysF_PTS.RelEquiv]
tyrel_all [constructor, in SysF_PTS.RelEquiv]
tyrel_imp [constructor, in SysF_PTS.RelEquiv]
tyrel_var [constructor, in SysF_PTS.RelEquiv]
TySpecF [constructor, in SysF_PTS.sysf]
TyVarF [constructor, in SysF_PTS.sysf]
U
upren_comb [lemma, in SysF_PTS.lib]V
VarL [constructor, in SysF_PTS.lambda2]vr [definition, in SysF_PTS.RelEquiv]
vrel [definition, in SysF_PTS.RelEquiv]
vrm [definition, in SysF_PTS.RelEquiv]
vrm_app [lemma, in SysF_PTS.RelEquiv]
vrm_comb [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_nil [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf [definition, in SysF_PTS.RelEquiv]
vr_tmctx_fl_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl_nil [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl [definition, in SysF_PTS.RelEquiv]
vr_rdis_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_rdis_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_rdis_r_nil [lemma, in SysF_PTS.RelEquiv]
vr_rdis_l_nil [lemma, in SysF_PTS.RelEquiv]
vr_rdis_sym [lemma, in SysF_PTS.RelEquiv]
vr_rdis [definition, in SysF_PTS.RelEquiv]
vr_tyctx_lf_ext [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_lf_rs [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_lf_nil [definition, in SysF_PTS.RelEquiv]
vr_tyctx_lf [definition, in SysF_PTS.RelEquiv]
vr_tyctx_fl_ext [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_fl_rs [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_fl_nil [definition, in SysF_PTS.RelEquiv]
vr_tyctx_fl [definition, in SysF_PTS.RelEquiv]
vr_inj_ext [lemma, in SysF_PTS.RelEquiv]
vr_inj_rs [lemma, in SysF_PTS.RelEquiv]
vr_inj_nil [lemma, in SysF_PTS.RelEquiv]
vr_inj [definition, in SysF_PTS.RelEquiv]
vr_func_ext [lemma, in SysF_PTS.RelEquiv]
vr_func_rs [lemma, in SysF_PTS.RelEquiv]
vr_func_nil [lemma, in SysF_PTS.RelEquiv]
vr_func [definition, in SysF_PTS.RelEquiv]
vr_right_app [lemma, in SysF_PTS.RelEquiv]
vr_left_app [lemma, in SysF_PTS.RelEquiv]
vr_app_or [lemma, in SysF_PTS.RelEquiv]
vr_unmap [lemma, in SysF_PTS.RelEquiv]
vr_map [lemma, in SysF_PTS.RelEquiv]
W
wfF [inductive, in SysF_PTS.sysf]wfF_ext_tm [constructor, in SysF_PTS.sysf]
wfF_ext_ty [constructor, in SysF_PTS.sysf]
wfF_empty [constructor, in SysF_PTS.sysf]
wfL [inductive, in SysF_PTS.lambda2]
wfL_atnd_ok [lemma, in SysF_PTS.lambda2]
wfL_ext [constructor, in SysF_PTS.lambda2]
wfL_empty [constructor, in SysF_PTS.lambda2]
wfP [inductive, in SysF_PTS.lambda2]
wfP_ext_ty [constructor, in SysF_PTS.lambda2]
wfP_ext_prp [constructor, in SysF_PTS.lambda2]
wfP_empty [constructor, in SysF_PTS.lambda2]
other
_ <$> _ [notation, in SysF_PTS.lib]do _ <- _ ; _ [notation, in SysF_PTS.lib]
GET _ <- _ ; _ [notation, in SysF_PTS.lib]
$$( _ ) [notation, in SysF_PTS.lib]
$? [notation, in SysF_PTS.lib]
(-1) [notation, in SysF_PTS.lib]
Notation Index
other
_ <$> _ [in SysF_PTS.lib]do _ <- _ ; _ [in SysF_PTS.lib]
GET _ <- _ ; _ [in SysF_PTS.lib]
$$( _ ) [in SysF_PTS.lib]
$? [in SysF_PTS.lib]
(-1) [in SysF_PTS.lib]
Library Index
D
DecidableL
lambda2lib
R
RelEquivS
sysfLemma Index
A
atnd_type_eqPrp_f [in SysF_PTS.lambda2]atnd_notPrp_eqPrp_f [in SysF_PTS.lambda2]
atnd_eqPrp_t [in SysF_PTS.lambda2]
atnd_getD [in SysF_PTS.lib]
atn_mmap [in SysF_PTS.lib]
atn_get [in SysF_PTS.lib]
B
bfr_ushift [in SysF_PTS.lib]bfr_shift [in SysF_PTS.lib]
bfr_up [in SysF_PTS.lib]
C
cm_typingL_beta [in SysF_PTS.lambda2]cm_typingL_id [in SysF_PTS.lambda2]
cm_typingL_up [in SysF_PTS.lambda2]
cm_typingP_beta_type [in SysF_PTS.lambda2]
cm_typingP_beta_term [in SysF_PTS.lambda2]
cm_typingP_up [in SysF_PTS.lambda2]
cm_istyP_beta_term [in SysF_PTS.lambda2]
cm_istyP_beta_type [in SysF_PTS.lambda2]
cm_istyP_up [in SysF_PTS.lambda2]
cm_typingL_nat_beta [in SysF_PTS.lambda2]
cm_typingL_nat_id [in SysF_PTS.lambda2]
cm_typingL_nat_up [in SysF_PTS.lambda2]
cm_tyrel_beta [in SysF_PTS.RelEquiv]
cm_tyrel_ext [in SysF_PTS.RelEquiv]
cm_tyrel_rs [in SysF_PTS.RelEquiv]
cm_istyF_beta [in SysF_PTS.sysf]
cm_istyF_up [in SysF_PTS.sysf]
comb_comp [in SysF_PTS.lib]
comb_cons [in SysF_PTS.lib]
cr_typingP_shift [in SysF_PTS.lambda2]
cr_typingP_up [in SysF_PTS.lambda2]
cr_cm_istyP [in SysF_PTS.lambda2]
cr_istyP_ushift [in SysF_PTS.lambda2]
cr_istyP_shift [in SysF_PTS.lambda2]
cr_istyP_up_id [in SysF_PTS.lambda2]
cr_istyP_up [in SysF_PTS.lambda2]
cr_istyP_id [in SysF_PTS.lambda2]
cr_cr_istyP [in SysF_PTS.lambda2]
cr_typingL_shift [in SysF_PTS.lambda2]
cr_typingL_up [in SysF_PTS.lambda2]
cr_shift [in SysF_PTS.lib]
cr_up [in SysF_PTS.lib]
cr_typingF_shift [in SysF_PTS.sysf]
cr_typingF_ren_ushift [in SysF_PTS.sysf]
cr_typingF_ren [in SysF_PTS.sysf]
cr_typingF_up [in SysF_PTS.sysf]
cr_typingF_id [in SysF_PTS.sysf]
cr_istyF_ushift [in SysF_PTS.sysf]
cr_istyF_shift [in SysF_PTS.sysf]
cr_istyF_up [in SysF_PTS.sysf]
cr_istyF_id [in SysF_PTS.sysf]
D
decide_eq_fin_domain [in SysF_PTS.Decidable]decide_refl [in SysF_PTS.lib]
E
eqPrp_t_subst_t [in SysF_PTS.lambda2]eqPrp_ren [in SysF_PTS.lambda2]
G
gentypingP_typingP [in SysF_PTS.lambda2]getD_cons [in SysF_PTS.lib]
getD_get [in SysF_PTS.lib]
getD_atnd [in SysF_PTS.lib]
get_mmap_None [in SysF_PTS.lib]
get_mmap [in SysF_PTS.lib]
get_atn [in SysF_PTS.lib]
I
internF_correct [in SysF_PTS.sysf]internLP_correct [in SysF_PTS.lambda2]
istyF_beta [in SysF_PTS.sysf]
istyF_subst [in SysF_PTS.sysf]
istyF_strengthen [in SysF_PTS.sysf]
istyF_weaken [in SysF_PTS.sysf]
istyF_ren [in SysF_PTS.sysf]
istyP_typingL [in SysF_PTS.lambda2]
istyP_subst [in SysF_PTS.lambda2]
istyP_strengthen [in SysF_PTS.lambda2]
istyP_weaken [in SysF_PTS.lambda2]
istyP_ren [in SysF_PTS.lambda2]
istyP_neqPrp [in SysF_PTS.lambda2]
istyP_notSort [in SysF_PTS.lambda2]
M
mmap_get_None [in SysF_PTS.lib]mmap_get [in SysF_PTS.lib]
mmap_atn [in SysF_PTS.lib]
S
sortL_add_subst [in SysF_PTS.lambda2]sortL_p1 [in SysF_PTS.lambda2]
sortL_ren [in SysF_PTS.lambda2]
sortP_eqPrp_f [in SysF_PTS.lambda2]
sortP_neq_ren [in SysF_PTS.lambda2]
subst_coinc_hcomp [in SysF_PTS.lib]
subst_coinc_hd_f [in SysF_PTS.lib]
subst_coinc_up [in SysF_PTS.lib]
subst_coinc_id [in SysF_PTS.lib]
T
tmrel_lf_total_preserving [in SysF_PTS.RelEquiv]tmrel_fl_total_preserving [in SysF_PTS.RelEquiv]
tmrel_injective [in SysF_PTS.RelEquiv]
tmrel_functional [in SysF_PTS.RelEquiv]
tmrel_lf_tot_pres [in SysF_PTS.RelEquiv]
tmrel_fl_tot_pres [in SysF_PTS.RelEquiv]
tmrel_inj [in SysF_PTS.RelEquiv]
tmrel_func [in SysF_PTS.RelEquiv]
typingF_weaken_ty [in SysF_PTS.sysf]
typingF_ren_ty [in SysF_PTS.sysf]
typingF_weaken [in SysF_PTS.sysf]
typingF_ren [in SysF_PTS.sysf]
typingL_typ_degenerate [in SysF_PTS.lambda2]
typingL_propagation [in SysF_PTS.lambda2]
typingL_beta [in SysF_PTS.lambda2]
typingL_subst [in SysF_PTS.lambda2]
typingL_sort_strengthen [in SysF_PTS.lambda2]
typingL_typingP [in SysF_PTS.lambda2]
typingL_typ_degenerate_nat [in SysF_PTS.lambda2]
typingL_propagation_nat [in SysF_PTS.lambda2]
typingL_beta_nat [in SysF_PTS.lambda2]
typingL_subst_nat [in SysF_PTS.lambda2]
typingL_weaken [in SysF_PTS.lambda2]
typingL_ren [in SysF_PTS.lambda2]
typingL_prp_prp_contra [in SysF_PTS.lambda2]
typingPL_equiv [in SysF_PTS.lambda2]
typingP_typingL [in SysF_PTS.lambda2]
typingP_istyP [in SysF_PTS.lambda2]
typingP_beta_type [in SysF_PTS.lambda2]
typingP_beta_term [in SysF_PTS.lambda2]
typingP_subst [in SysF_PTS.lambda2]
typingP_weaken [in SysF_PTS.lambda2]
typingP_ren [in SysF_PTS.lambda2]
tyrel_lf_total_preserving [in SysF_PTS.RelEquiv]
tyrel_fl_total_preserving [in SysF_PTS.RelEquiv]
tyrel_injective [in SysF_PTS.RelEquiv]
tyrel_functional [in SysF_PTS.RelEquiv]
tyrel_tmrel_disjoint [in SysF_PTS.RelEquiv]
tyrel_beta [in SysF_PTS.RelEquiv]
tyrel_subst [in SysF_PTS.RelEquiv]
tyrel_unmap [in SysF_PTS.RelEquiv]
tyrel_weaken_hd [in SysF_PTS.RelEquiv]
tyrel_weaken [in SysF_PTS.RelEquiv]
tyrel_ren [in SysF_PTS.RelEquiv]
tyrel_lf_tot_pres [in SysF_PTS.RelEquiv]
tyrel_fl_tot_pres [in SysF_PTS.RelEquiv]
tyrel_inj [in SysF_PTS.RelEquiv]
tyrel_func [in SysF_PTS.RelEquiv]
U
upren_comb [in SysF_PTS.lib]V
vrm_app [in SysF_PTS.RelEquiv]vrm_comb [in SysF_PTS.RelEquiv]
vr_tmctx_lf_ext_rs [in SysF_PTS.RelEquiv]
vr_tmctx_lf_rs_ext [in SysF_PTS.RelEquiv]
vr_tmctx_lf_nil [in SysF_PTS.RelEquiv]
vr_tmctx_fl_ext_rs [in SysF_PTS.RelEquiv]
vr_tmctx_fl_rs_ext [in SysF_PTS.RelEquiv]
vr_tmctx_fl_nil [in SysF_PTS.RelEquiv]
vr_rdis_ext_rs [in SysF_PTS.RelEquiv]
vr_rdis_rs_ext [in SysF_PTS.RelEquiv]
vr_rdis_r_nil [in SysF_PTS.RelEquiv]
vr_rdis_l_nil [in SysF_PTS.RelEquiv]
vr_rdis_sym [in SysF_PTS.RelEquiv]
vr_tyctx_lf_ext [in SysF_PTS.RelEquiv]
vr_tyctx_lf_rs [in SysF_PTS.RelEquiv]
vr_tyctx_fl_ext [in SysF_PTS.RelEquiv]
vr_tyctx_fl_rs [in SysF_PTS.RelEquiv]
vr_inj_ext [in SysF_PTS.RelEquiv]
vr_inj_rs [in SysF_PTS.RelEquiv]
vr_inj_nil [in SysF_PTS.RelEquiv]
vr_func_ext [in SysF_PTS.RelEquiv]
vr_func_rs [in SysF_PTS.RelEquiv]
vr_func_nil [in SysF_PTS.RelEquiv]
vr_right_app [in SysF_PTS.RelEquiv]
vr_left_app [in SysF_PTS.RelEquiv]
vr_app_or [in SysF_PTS.RelEquiv]
vr_unmap [in SysF_PTS.RelEquiv]
vr_map [in SysF_PTS.RelEquiv]
W
wfL_atnd_ok [in SysF_PTS.lambda2]Constructor Index
A
AllF [in SysF_PTS.sysf]AppF [in SysF_PTS.sysf]
AppL [in SysF_PTS.lambda2]
AtndS [in SysF_PTS.lib]
Atnd0 [in SysF_PTS.lib]
AtnS [in SysF_PTS.lib]
Atn0 [in SysF_PTS.lib]
D
decide [in SysF_PTS.Decidable]I
ImpF [in SysF_PTS.sysf]istyF_all [in SysF_PTS.sysf]
istyF_imp [in SysF_PTS.sysf]
istyF_var [in SysF_PTS.sysf]
istyP_prod2 [in SysF_PTS.lambda2]
istyP_prod1 [in SysF_PTS.lambda2]
istyP_var [in SysF_PTS.lambda2]
L
LamF [in SysF_PTS.sysf]LamL [in SysF_PTS.lambda2]
P
ProdL [in SysF_PTS.lambda2]Prp [in SysF_PTS.lambda2]
S
SortL [in SysF_PTS.lambda2]T
tmrel_tyabs [in SysF_PTS.RelEquiv]tmrel_tyspec [in SysF_PTS.RelEquiv]
tmrel_lam [in SysF_PTS.RelEquiv]
tmrel_app [in SysF_PTS.RelEquiv]
tmrel_var [in SysF_PTS.RelEquiv]
TmVarF [in SysF_PTS.sysf]
TyAbsF [in SysF_PTS.sysf]
Typ [in SysF_PTS.lambda2]
typingF_tyabs [in SysF_PTS.sysf]
typingF_tyspec [in SysF_PTS.sysf]
typingF_lam [in SysF_PTS.sysf]
typingF_app [in SysF_PTS.sysf]
typingF_var [in SysF_PTS.sysf]
typingL_lam [in SysF_PTS.lambda2]
typingL_app [in SysF_PTS.lambda2]
typingL_prod [in SysF_PTS.lambda2]
typingL_var [in SysF_PTS.lambda2]
typingL_ax [in SysF_PTS.lambda2]
typingP_lam2 [in SysF_PTS.lambda2]
typingP_app2 [in SysF_PTS.lambda2]
typingP_lam1 [in SysF_PTS.lambda2]
typingP_app1 [in SysF_PTS.lambda2]
typingP_var [in SysF_PTS.lambda2]
tyrel_all [in SysF_PTS.RelEquiv]
tyrel_imp [in SysF_PTS.RelEquiv]
tyrel_var [in SysF_PTS.RelEquiv]
TySpecF [in SysF_PTS.sysf]
TyVarF [in SysF_PTS.sysf]
V
VarL [in SysF_PTS.lambda2]W
wfF_ext_tm [in SysF_PTS.sysf]wfF_ext_ty [in SysF_PTS.sysf]
wfF_empty [in SysF_PTS.sysf]
wfL_ext [in SysF_PTS.lambda2]
wfL_empty [in SysF_PTS.lambda2]
wfP_ext_ty [in SysF_PTS.lambda2]
wfP_ext_prp [in SysF_PTS.lambda2]
wfP_empty [in SysF_PTS.lambda2]
Inductive Index
A
atn [in SysF_PTS.lib]atnd [in SysF_PTS.lib]
D
Dec [in SysF_PTS.Decidable]I
istyF [in SysF_PTS.sysf]istyP [in SysF_PTS.lambda2]
L
level [in SysF_PTS.lambda2]T
termF [in SysF_PTS.sysf]termL [in SysF_PTS.lambda2]
tmrel [in SysF_PTS.RelEquiv]
typeF [in SysF_PTS.sysf]
typingF [in SysF_PTS.sysf]
typingL [in SysF_PTS.lambda2]
typingP [in SysF_PTS.lambda2]
tyrel [in SysF_PTS.RelEquiv]
W
wfF [in SysF_PTS.sysf]wfL [in SysF_PTS.lambda2]
wfP [in SysF_PTS.lambda2]
Projection Index
B
bind [in SysF_PTS.lib]C
countableProp [in SysF_PTS.Decidable]D
decide [in SysF_PTS.Decidable]E
enum [in SysF_PTS.Decidable]F
finiteProp [in SysF_PTS.Decidable]fmap [in SysF_PTS.lib]
N
numElems [in SysF_PTS.Decidable]R
repr [in SysF_PTS.Decidable]ret [in SysF_PTS.lib]
Instance Index
D
decidable_neg [in SysF_PTS.Decidable]decide_eq_termL [in SysF_PTS.lambda2]
decide_eq_level [in SysF_PTS.lambda2]
decide_eq_termF [in SysF_PTS.sysf]
decide_eq_typeF [in SysF_PTS.sysf]
Dec_eq_fin_domain [in SysF_PTS.Decidable]
Dec_fin_quant [in SysF_PTS.Decidable]
Dec_fin_quant_T [in SysF_PTS.Decidable]
Dec_impl [in SysF_PTS.Decidable]
Dec_or [in SysF_PTS.Decidable]
Dec_and [in SysF_PTS.Decidable]
Dec_lt_nat [in SysF_PTS.Decidable]
Dec_le_nat [in SysF_PTS.Decidable]
Dec_eq_option [in SysF_PTS.Decidable]
Dec_eq_nat [in SysF_PTS.Decidable]
F
Functor_Monad [in SysF_PTS.lib]H
HSubstLemmas_termF [in SysF_PTS.sysf]HSubst_termF [in SysF_PTS.sysf]
I
Ids_termL [in SysF_PTS.lambda2]Ids_termF [in SysF_PTS.sysf]
Ids_typeF [in SysF_PTS.sysf]
R
Rename_termL [in SysF_PTS.lambda2]Rename_termF [in SysF_PTS.sysf]
Rename_typeF [in SysF_PTS.sysf]
S
SubstHSubstComp_typeF_termF [in SysF_PTS.sysf]SubstLemmas_termL [in SysF_PTS.lambda2]
SubstLemmas_termF [in SysF_PTS.sysf]
SubstLemmas_typeF [in SysF_PTS.sysf]
Subst_termL [in SysF_PTS.lambda2]
Subst_termF [in SysF_PTS.sysf]
Subst_typeF [in SysF_PTS.sysf]
Section Index
C
Coincidence [in SysF_PTS.lib]CoincidenceHSubst [in SysF_PTS.lib]
ContextRenamings [in SysF_PTS.lib]
CtxBoolFun [in SysF_PTS.lib]
S
SubstInstance [in SysF_PTS.lib]Abbreviation Index
D
dec [in SysF_PTS.Decidable]E
eq_dec [in SysF_PTS.Decidable]Definition Index
B
bfr [in SysF_PTS.lib]C
cm_typingL [in SysF_PTS.lambda2]cm_typingP [in SysF_PTS.lambda2]
cm_istyP [in SysF_PTS.lambda2]
cm_typingL_nat [in SysF_PTS.lambda2]
cm_tyrel [in SysF_PTS.RelEquiv]
cm_istyF [in SysF_PTS.sysf]
comb [in SysF_PTS.lib]
cr [in SysF_PTS.lib]
cr_typingP [in SysF_PTS.lambda2]
cr_istyP [in SysF_PTS.lambda2]
cr_typingL [in SysF_PTS.lambda2]
cr_typingF [in SysF_PTS.sysf]
cr_istyF [in SysF_PTS.sysf]
E
eqPrp [in SysF_PTS.lambda2]G
gentypingP [in SysF_PTS.lambda2]get [in SysF_PTS.lib]
getD [in SysF_PTS.lib]
I
internF [in SysF_PTS.sysf]internF_ty [in SysF_PTS.sysf]
internL [in SysF_PTS.lambda2]
S
subst_coinc [in SysF_PTS.lib]sum2bool [in SysF_PTS.lib]
V
vr [in SysF_PTS.RelEquiv]vrel [in SysF_PTS.RelEquiv]
vrm [in SysF_PTS.RelEquiv]
vr_tmctx_lf [in SysF_PTS.RelEquiv]
vr_tmctx_fl [in SysF_PTS.RelEquiv]
vr_rdis [in SysF_PTS.RelEquiv]
vr_tyctx_lf_nil [in SysF_PTS.RelEquiv]
vr_tyctx_lf [in SysF_PTS.RelEquiv]
vr_tyctx_fl_nil [in SysF_PTS.RelEquiv]
vr_tyctx_fl [in SysF_PTS.RelEquiv]
vr_inj [in SysF_PTS.RelEquiv]
vr_func [in SysF_PTS.RelEquiv]
Record Index
C
Countable [in SysF_PTS.Decidable]D
Dec [in SysF_PTS.Decidable]F
Finite [in SysF_PTS.Decidable]Functor [in SysF_PTS.lib]
M
Monad [in SysF_PTS.lib]| 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 | (337 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 | (6 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 | (165 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 | (57 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 | (17 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 | (9 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 | (31 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 | (5 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 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) |