| 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 | (269 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 | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (130 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 | (41 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) |
| 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 | (12 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) |
| 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) |
| 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 | (25 entries) |
Global Index
A
AllF [constructor, in SysF_PTS.sysf_pts]AppF [constructor, in SysF_PTS.sysf_pts]
AppL [constructor, in SysF_PTS.sysf_pts]
atn [inductive, in SysF_PTS.lib]
atnd [inductive, in SysF_PTS.lib]
AtndS [constructor, in SysF_PTS.lib]
atnd_getD [lemma, in SysF_PTS.lib]
atnd_type_eqPrp_f [lemma, in SysF_PTS.sysf_pts]
atnd_notPrp_eqPrp_f [lemma, in SysF_PTS.sysf_pts]
atnd_eqPrp_t [lemma, in SysF_PTS.sysf_pts]
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
cancellation_trTermFPF [lemma, in SysF_PTS.sysf_pts]cancellation_trTypeFPF [lemma, in SysF_PTS.sysf_pts]
cancellation_trTermPFP [lemma, in SysF_PTS.sysf_pts]
cancellation_trTypePFP [lemma, in SysF_PTS.sysf_pts]
cm_vdP_shift_up [lemma, in SysF_PTS.sysf_pts]
cm_vdP_up_shift [lemma, in SysF_PTS.sysf_pts]
cm_vdP_vac [lemma, in SysF_PTS.sysf_pts]
cm_vdP [definition, in SysF_PTS.sysf_pts]
cm_trTypePF_beta [lemma, in SysF_PTS.sysf_pts]
cm_trTypePF_up [lemma, in SysF_PTS.sysf_pts]
cm_trTypePF [definition, in SysF_PTS.sysf_pts]
cm_typingP_beta_type [lemma, in SysF_PTS.sysf_pts]
cm_typingP_beta_term [lemma, in SysF_PTS.sysf_pts]
cm_typingP_up [lemma, in SysF_PTS.sysf_pts]
cm_typingP [definition, in SysF_PTS.sysf_pts]
cm_istyP_beta_term [lemma, in SysF_PTS.sysf_pts]
cm_istyP_beta_type [lemma, in SysF_PTS.sysf_pts]
cm_istyP_up [lemma, in SysF_PTS.sysf_pts]
cm_istyP [definition, in SysF_PTS.sysf_pts]
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_shift [lemma, in SysF_PTS.lib]
cr_up [lemma, in SysF_PTS.lib]
cr_typingPF_ushift_up [lemma, in SysF_PTS.sysf_pts]
cr_typingPF_up_ushift [lemma, in SysF_PTS.sysf_pts]
cr_typingPF_vac [lemma, in SysF_PTS.sysf_pts]
cr_typingPF [definition, in SysF_PTS.sysf_pts]
cr_istyPF_ushift [lemma, in SysF_PTS.sysf_pts]
cr_istyPF_up [lemma, in SysF_PTS.sysf_pts]
cr_istyPF_vac [lemma, in SysF_PTS.sysf_pts]
cr_istyPF [definition, in SysF_PTS.sysf_pts]
cr_typingFP_shift_up [lemma, in SysF_PTS.sysf_pts]
cr_typingFP_up_shift [lemma, in SysF_PTS.sysf_pts]
cr_typingFP_vac [lemma, in SysF_PTS.sysf_pts]
cr_typingFP [definition, in SysF_PTS.sysf_pts]
cr_istyFP_shift [lemma, in SysF_PTS.sysf_pts]
cr_istyFP_up [lemma, in SysF_PTS.sysf_pts]
cr_istyFP_vac [lemma, in SysF_PTS.sysf_pts]
cr_istyFP [definition, in SysF_PTS.sysf_pts]
cr_typingP_shift [lemma, in SysF_PTS.sysf_pts]
cr_typingP_up [lemma, in SysF_PTS.sysf_pts]
cr_typingP [definition, in SysF_PTS.sysf_pts]
cr_cm_istyP [lemma, in SysF_PTS.sysf_pts]
cr_istyP_ushift [lemma, in SysF_PTS.sysf_pts]
cr_istyP_shift [lemma, in SysF_PTS.sysf_pts]
cr_istyP_up_id [lemma, in SysF_PTS.sysf_pts]
cr_istyP_up [lemma, in SysF_PTS.sysf_pts]
cr_istyP_id [lemma, in SysF_PTS.sysf_pts]
cr_cr_istyP [lemma, in SysF_PTS.sysf_pts]
cr_istyP [definition, in SysF_PTS.sysf_pts]
cr_typingF_shift [lemma, in SysF_PTS.sysf_pts]
cr_typingF_ren_ushift [lemma, in SysF_PTS.sysf_pts]
cr_typingF_ren [lemma, in SysF_PTS.sysf_pts]
cr_typingF_up [lemma, in SysF_PTS.sysf_pts]
cr_typingF_id [lemma, in SysF_PTS.sysf_pts]
cr_typingF [definition, in SysF_PTS.sysf_pts]
cr_istyF_ushift [lemma, in SysF_PTS.sysf_pts]
cr_istyF_shift [lemma, in SysF_PTS.sysf_pts]
cr_istyF_up [lemma, in SysF_PTS.sysf_pts]
cr_istyF_id [lemma, in SysF_PTS.sysf_pts]
cr_istyF [definition, in SysF_PTS.sysf_pts]
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_fin_domain [lemma, in SysF_PTS.Decidable]
decide_refl [lemma, in SysF_PTS.lib]
decide_eq_termL [instance, in SysF_PTS.sysf_pts]
decide_eq_level [instance, in SysF_PTS.sysf_pts]
decide_eq_termF [instance, in SysF_PTS.sysf_pts]
decide_eq_typeF [instance, in SysF_PTS.sysf_pts]
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.sysf_pts]
eqPrp_t_subst_t [lemma, in SysF_PTS.sysf_pts]
eqPrp_ren [lemma, in SysF_PTS.sysf_pts]
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.sysf_pts]gentypingP_typingP [lemma, in SysF_PTS.sysf_pts]
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_pts]HSubst_termF [instance, in SysF_PTS.sysf_pts]
I
Ids_termL [instance, in SysF_PTS.sysf_pts]Ids_termF [instance, in SysF_PTS.sysf_pts]
Ids_typeF [instance, in SysF_PTS.sysf_pts]
ImpF [constructor, in SysF_PTS.sysf_pts]
istyF [inductive, in SysF_PTS.sysf_pts]
istyF_strengthen [lemma, in SysF_PTS.sysf_pts]
istyF_weaken [lemma, in SysF_PTS.sysf_pts]
istyF_ren [lemma, in SysF_PTS.sysf_pts]
istyF_all [constructor, in SysF_PTS.sysf_pts]
istyF_imp [constructor, in SysF_PTS.sysf_pts]
istyF_var [constructor, in SysF_PTS.sysf_pts]
istyP [inductive, in SysF_PTS.sysf_pts]
istyP_trTypePF [lemma, in SysF_PTS.sysf_pts]
istyP_typingL [lemma, in SysF_PTS.sysf_pts]
istyP_neqPrp [lemma, in SysF_PTS.sysf_pts]
istyP_subst [lemma, in SysF_PTS.sysf_pts]
istyP_strengthen [lemma, in SysF_PTS.sysf_pts]
istyP_weaken [lemma, in SysF_PTS.sysf_pts]
istyP_ren [lemma, in SysF_PTS.sysf_pts]
istyP_notSort [lemma, in SysF_PTS.sysf_pts]
istyP_prod2 [constructor, in SysF_PTS.sysf_pts]
istyP_prod1 [constructor, in SysF_PTS.sysf_pts]
istyP_var [constructor, in SysF_PTS.sysf_pts]
L
LamF [constructor, in SysF_PTS.sysf_pts]LamL [constructor, in SysF_PTS.sysf_pts]
level [inductive, in SysF_PTS.sysf_pts]
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.sysf_pts]Prp [constructor, in SysF_PTS.sysf_pts]
R
Rename_termL [instance, in SysF_PTS.sysf_pts]Rename_termF [instance, in SysF_PTS.sysf_pts]
Rename_typeF [instance, in SysF_PTS.sysf_pts]
repr [projection, in SysF_PTS.Decidable]
ret [projection, in SysF_PTS.lib]
S
SortL [constructor, in SysF_PTS.sysf_pts]sortL_add_ren [lemma, in SysF_PTS.sysf_pts]
sortL_p1 [lemma, in SysF_PTS.sysf_pts]
sortL_ren [lemma, in SysF_PTS.sysf_pts]
sortP_eqPrp_f [lemma, in SysF_PTS.sysf_pts]
sortP_neq_ren [lemma, in SysF_PTS.sysf_pts]
SubstHSubstComp_typeF_termF [instance, in SysF_PTS.sysf_pts]
SubstInstance [section, in SysF_PTS.lib]
SubstLemmas_termL [instance, in SysF_PTS.sysf_pts]
SubstLemmas_termF [instance, in SysF_PTS.sysf_pts]
SubstLemmas_typeF [instance, in SysF_PTS.sysf_pts]
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_termL [instance, in SysF_PTS.sysf_pts]
Subst_termF [instance, in SysF_PTS.sysf_pts]
Subst_typeF [instance, in SysF_PTS.sysf_pts]
sum2bool [definition, in SysF_PTS.lib]
sysf_pts [library]
T
termF [inductive, in SysF_PTS.sysf_pts]termL [inductive, in SysF_PTS.sysf_pts]
TmVarF [constructor, in SysF_PTS.sysf_pts]
trIstyFP_morph [lemma, in SysF_PTS.sysf_pts]
trIstyPF_morph' [lemma, in SysF_PTS.sysf_pts]
trIstyPF_morph [lemma, in SysF_PTS.sysf_pts]
trTermFP [definition, in SysF_PTS.sysf_pts]
trTermFP_not_istyP [lemma, in SysF_PTS.sysf_pts]
trTermFP_ren [lemma, in SysF_PTS.sysf_pts]
trTermFP_ren_ren [lemma, in SysF_PTS.sysf_pts]
trTermPF [definition, in SysF_PTS.sysf_pts]
trTermPF_free_ty [lemma, in SysF_PTS.sysf_pts]
trTermPF_free_tm [lemma, in SysF_PTS.sysf_pts]
trTermPF_free [lemma, in SysF_PTS.sysf_pts]
trTypeFP [definition, in SysF_PTS.sysf_pts]
trTypeFP_not_typingP [lemma, in SysF_PTS.sysf_pts]
trTypeFP_subst [lemma, in SysF_PTS.sysf_pts]
trTypeFP_ren [lemma, in SysF_PTS.sysf_pts]
trTypePF [definition, in SysF_PTS.sysf_pts]
trTypePF_subst [lemma, in SysF_PTS.sysf_pts]
trTypePF_ren [lemma, in SysF_PTS.sysf_pts]
trTypePF_free_arg [lemma, in SysF_PTS.sysf_pts]
trTypePF_free_res [lemma, in SysF_PTS.sysf_pts]
trTypePF_eqPrp_f [lemma, in SysF_PTS.sysf_pts]
trTypingFL_red [lemma, in SysF_PTS.sysf_pts]
trTypingFP_red [lemma, in SysF_PTS.sysf_pts]
trTypingFP_morph [lemma, in SysF_PTS.sysf_pts]
trTypingLF_red [lemma, in SysF_PTS.sysf_pts]
trTypingPF_red [lemma, in SysF_PTS.sysf_pts]
trTypingPF_morph [lemma, in SysF_PTS.sysf_pts]
TyAbsF [constructor, in SysF_PTS.sysf_pts]
Typ [constructor, in SysF_PTS.sysf_pts]
typeF [inductive, in SysF_PTS.sysf_pts]
typingF [inductive, in SysF_PTS.sysf_pts]
typingF_weaken_ty [lemma, in SysF_PTS.sysf_pts]
typingF_ren_ty [lemma, in SysF_PTS.sysf_pts]
typingF_weaken [lemma, in SysF_PTS.sysf_pts]
typingF_ren [lemma, in SysF_PTS.sysf_pts]
typingF_tyabs [constructor, in SysF_PTS.sysf_pts]
typingF_tyspec [constructor, in SysF_PTS.sysf_pts]
typingF_lam [constructor, in SysF_PTS.sysf_pts]
typingF_app [constructor, in SysF_PTS.sysf_pts]
typingF_var [constructor, in SysF_PTS.sysf_pts]
typingL [inductive, in SysF_PTS.sysf_pts]
typingL_typingP [lemma, in SysF_PTS.sysf_pts]
typingL_lam [constructor, in SysF_PTS.sysf_pts]
typingL_app [constructor, in SysF_PTS.sysf_pts]
typingL_prod [constructor, in SysF_PTS.sysf_pts]
typingL_var [constructor, in SysF_PTS.sysf_pts]
typingL_ax [constructor, in SysF_PTS.sysf_pts]
typingP [inductive, in SysF_PTS.sysf_pts]
typingPL_equiv [lemma, in SysF_PTS.sysf_pts]
typingP_trTypePF [lemma, in SysF_PTS.sysf_pts]
typingP_typingL [lemma, in SysF_PTS.sysf_pts]
typingP_istyP [lemma, in SysF_PTS.sysf_pts]
typingP_beta_type [lemma, in SysF_PTS.sysf_pts]
typingP_beta_term [lemma, in SysF_PTS.sysf_pts]
typingP_subst [lemma, in SysF_PTS.sysf_pts]
typingP_weaken [lemma, in SysF_PTS.sysf_pts]
typingP_ren [lemma, in SysF_PTS.sysf_pts]
typingP_lam2 [constructor, in SysF_PTS.sysf_pts]
typingP_app2 [constructor, in SysF_PTS.sysf_pts]
typingP_lam1 [constructor, in SysF_PTS.sysf_pts]
typingP_app1 [constructor, in SysF_PTS.sysf_pts]
typingP_var [constructor, in SysF_PTS.sysf_pts]
TySpecF [constructor, in SysF_PTS.sysf_pts]
TyVarF [constructor, in SysF_PTS.sysf_pts]
U
upren_comb [lemma, in SysF_PTS.lib]V
VarL [constructor, in SysF_PTS.sysf_pts]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
libS
sysf_ptsLemma Index
A
atnd_getD [in SysF_PTS.lib]atnd_type_eqPrp_f [in SysF_PTS.sysf_pts]
atnd_notPrp_eqPrp_f [in SysF_PTS.sysf_pts]
atnd_eqPrp_t [in SysF_PTS.sysf_pts]
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
cancellation_trTermFPF [in SysF_PTS.sysf_pts]cancellation_trTypeFPF [in SysF_PTS.sysf_pts]
cancellation_trTermPFP [in SysF_PTS.sysf_pts]
cancellation_trTypePFP [in SysF_PTS.sysf_pts]
cm_vdP_shift_up [in SysF_PTS.sysf_pts]
cm_vdP_up_shift [in SysF_PTS.sysf_pts]
cm_vdP_vac [in SysF_PTS.sysf_pts]
cm_trTypePF_beta [in SysF_PTS.sysf_pts]
cm_trTypePF_up [in SysF_PTS.sysf_pts]
cm_typingP_beta_type [in SysF_PTS.sysf_pts]
cm_typingP_beta_term [in SysF_PTS.sysf_pts]
cm_typingP_up [in SysF_PTS.sysf_pts]
cm_istyP_beta_term [in SysF_PTS.sysf_pts]
cm_istyP_beta_type [in SysF_PTS.sysf_pts]
cm_istyP_up [in SysF_PTS.sysf_pts]
comb_comp [in SysF_PTS.lib]
comb_cons [in SysF_PTS.lib]
cr_shift [in SysF_PTS.lib]
cr_up [in SysF_PTS.lib]
cr_typingPF_ushift_up [in SysF_PTS.sysf_pts]
cr_typingPF_up_ushift [in SysF_PTS.sysf_pts]
cr_typingPF_vac [in SysF_PTS.sysf_pts]
cr_istyPF_ushift [in SysF_PTS.sysf_pts]
cr_istyPF_up [in SysF_PTS.sysf_pts]
cr_istyPF_vac [in SysF_PTS.sysf_pts]
cr_typingFP_shift_up [in SysF_PTS.sysf_pts]
cr_typingFP_up_shift [in SysF_PTS.sysf_pts]
cr_typingFP_vac [in SysF_PTS.sysf_pts]
cr_istyFP_shift [in SysF_PTS.sysf_pts]
cr_istyFP_up [in SysF_PTS.sysf_pts]
cr_istyFP_vac [in SysF_PTS.sysf_pts]
cr_typingP_shift [in SysF_PTS.sysf_pts]
cr_typingP_up [in SysF_PTS.sysf_pts]
cr_cm_istyP [in SysF_PTS.sysf_pts]
cr_istyP_ushift [in SysF_PTS.sysf_pts]
cr_istyP_shift [in SysF_PTS.sysf_pts]
cr_istyP_up_id [in SysF_PTS.sysf_pts]
cr_istyP_up [in SysF_PTS.sysf_pts]
cr_istyP_id [in SysF_PTS.sysf_pts]
cr_cr_istyP [in SysF_PTS.sysf_pts]
cr_typingF_shift [in SysF_PTS.sysf_pts]
cr_typingF_ren_ushift [in SysF_PTS.sysf_pts]
cr_typingF_ren [in SysF_PTS.sysf_pts]
cr_typingF_up [in SysF_PTS.sysf_pts]
cr_typingF_id [in SysF_PTS.sysf_pts]
cr_istyF_ushift [in SysF_PTS.sysf_pts]
cr_istyF_shift [in SysF_PTS.sysf_pts]
cr_istyF_up [in SysF_PTS.sysf_pts]
cr_istyF_id [in SysF_PTS.sysf_pts]
D
decide_eq_fin_domain [in SysF_PTS.Decidable]decide_refl [in SysF_PTS.lib]
E
eqPrp_t_subst_t [in SysF_PTS.sysf_pts]eqPrp_ren [in SysF_PTS.sysf_pts]
G
gentypingP_typingP [in SysF_PTS.sysf_pts]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
istyF_strengthen [in SysF_PTS.sysf_pts]istyF_weaken [in SysF_PTS.sysf_pts]
istyF_ren [in SysF_PTS.sysf_pts]
istyP_trTypePF [in SysF_PTS.sysf_pts]
istyP_typingL [in SysF_PTS.sysf_pts]
istyP_neqPrp [in SysF_PTS.sysf_pts]
istyP_subst [in SysF_PTS.sysf_pts]
istyP_strengthen [in SysF_PTS.sysf_pts]
istyP_weaken [in SysF_PTS.sysf_pts]
istyP_ren [in SysF_PTS.sysf_pts]
istyP_notSort [in SysF_PTS.sysf_pts]
M
mmap_get_None [in SysF_PTS.lib]mmap_get [in SysF_PTS.lib]
mmap_atn [in SysF_PTS.lib]
S
sortL_add_ren [in SysF_PTS.sysf_pts]sortL_p1 [in SysF_PTS.sysf_pts]
sortL_ren [in SysF_PTS.sysf_pts]
sortP_eqPrp_f [in SysF_PTS.sysf_pts]
sortP_neq_ren [in SysF_PTS.sysf_pts]
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
trIstyFP_morph [in SysF_PTS.sysf_pts]trIstyPF_morph' [in SysF_PTS.sysf_pts]
trIstyPF_morph [in SysF_PTS.sysf_pts]
trTermFP_not_istyP [in SysF_PTS.sysf_pts]
trTermFP_ren [in SysF_PTS.sysf_pts]
trTermFP_ren_ren [in SysF_PTS.sysf_pts]
trTermPF_free_ty [in SysF_PTS.sysf_pts]
trTermPF_free_tm [in SysF_PTS.sysf_pts]
trTermPF_free [in SysF_PTS.sysf_pts]
trTypeFP_not_typingP [in SysF_PTS.sysf_pts]
trTypeFP_subst [in SysF_PTS.sysf_pts]
trTypeFP_ren [in SysF_PTS.sysf_pts]
trTypePF_subst [in SysF_PTS.sysf_pts]
trTypePF_ren [in SysF_PTS.sysf_pts]
trTypePF_free_arg [in SysF_PTS.sysf_pts]
trTypePF_free_res [in SysF_PTS.sysf_pts]
trTypePF_eqPrp_f [in SysF_PTS.sysf_pts]
trTypingFL_red [in SysF_PTS.sysf_pts]
trTypingFP_red [in SysF_PTS.sysf_pts]
trTypingFP_morph [in SysF_PTS.sysf_pts]
trTypingLF_red [in SysF_PTS.sysf_pts]
trTypingPF_red [in SysF_PTS.sysf_pts]
trTypingPF_morph [in SysF_PTS.sysf_pts]
typingF_weaken_ty [in SysF_PTS.sysf_pts]
typingF_ren_ty [in SysF_PTS.sysf_pts]
typingF_weaken [in SysF_PTS.sysf_pts]
typingF_ren [in SysF_PTS.sysf_pts]
typingL_typingP [in SysF_PTS.sysf_pts]
typingPL_equiv [in SysF_PTS.sysf_pts]
typingP_trTypePF [in SysF_PTS.sysf_pts]
typingP_typingL [in SysF_PTS.sysf_pts]
typingP_istyP [in SysF_PTS.sysf_pts]
typingP_beta_type [in SysF_PTS.sysf_pts]
typingP_beta_term [in SysF_PTS.sysf_pts]
typingP_subst [in SysF_PTS.sysf_pts]
typingP_weaken [in SysF_PTS.sysf_pts]
typingP_ren [in SysF_PTS.sysf_pts]
U
upren_comb [in SysF_PTS.lib]Constructor Index
A
AllF [in SysF_PTS.sysf_pts]AppF [in SysF_PTS.sysf_pts]
AppL [in SysF_PTS.sysf_pts]
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_pts]istyF_all [in SysF_PTS.sysf_pts]
istyF_imp [in SysF_PTS.sysf_pts]
istyF_var [in SysF_PTS.sysf_pts]
istyP_prod2 [in SysF_PTS.sysf_pts]
istyP_prod1 [in SysF_PTS.sysf_pts]
istyP_var [in SysF_PTS.sysf_pts]
L
LamF [in SysF_PTS.sysf_pts]LamL [in SysF_PTS.sysf_pts]
P
ProdL [in SysF_PTS.sysf_pts]Prp [in SysF_PTS.sysf_pts]
S
SortL [in SysF_PTS.sysf_pts]T
TmVarF [in SysF_PTS.sysf_pts]TyAbsF [in SysF_PTS.sysf_pts]
Typ [in SysF_PTS.sysf_pts]
typingF_tyabs [in SysF_PTS.sysf_pts]
typingF_tyspec [in SysF_PTS.sysf_pts]
typingF_lam [in SysF_PTS.sysf_pts]
typingF_app [in SysF_PTS.sysf_pts]
typingF_var [in SysF_PTS.sysf_pts]
typingL_lam [in SysF_PTS.sysf_pts]
typingL_app [in SysF_PTS.sysf_pts]
typingL_prod [in SysF_PTS.sysf_pts]
typingL_var [in SysF_PTS.sysf_pts]
typingL_ax [in SysF_PTS.sysf_pts]
typingP_lam2 [in SysF_PTS.sysf_pts]
typingP_app2 [in SysF_PTS.sysf_pts]
typingP_lam1 [in SysF_PTS.sysf_pts]
typingP_app1 [in SysF_PTS.sysf_pts]
typingP_var [in SysF_PTS.sysf_pts]
TySpecF [in SysF_PTS.sysf_pts]
TyVarF [in SysF_PTS.sysf_pts]
V
VarL [in SysF_PTS.sysf_pts]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]
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_pts]istyP [in SysF_PTS.sysf_pts]
L
level [in SysF_PTS.sysf_pts]T
termF [in SysF_PTS.sysf_pts]termL [in SysF_PTS.sysf_pts]
typeF [in SysF_PTS.sysf_pts]
typingF [in SysF_PTS.sysf_pts]
typingL [in SysF_PTS.sysf_pts]
typingP [in SysF_PTS.sysf_pts]
Instance Index
D
decidable_neg [in SysF_PTS.Decidable]decide_eq_termL [in SysF_PTS.sysf_pts]
decide_eq_level [in SysF_PTS.sysf_pts]
decide_eq_termF [in SysF_PTS.sysf_pts]
decide_eq_typeF [in SysF_PTS.sysf_pts]
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_pts]HSubst_termF [in SysF_PTS.sysf_pts]
I
Ids_termL [in SysF_PTS.sysf_pts]Ids_termF [in SysF_PTS.sysf_pts]
Ids_typeF [in SysF_PTS.sysf_pts]
R
Rename_termL [in SysF_PTS.sysf_pts]Rename_termF [in SysF_PTS.sysf_pts]
Rename_typeF [in SysF_PTS.sysf_pts]
S
SubstHSubstComp_typeF_termF [in SysF_PTS.sysf_pts]SubstLemmas_termL [in SysF_PTS.sysf_pts]
SubstLemmas_termF [in SysF_PTS.sysf_pts]
SubstLemmas_typeF [in SysF_PTS.sysf_pts]
Subst_termL [in SysF_PTS.sysf_pts]
Subst_termF [in SysF_PTS.sysf_pts]
Subst_typeF [in SysF_PTS.sysf_pts]
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]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]Definition Index
B
bfr [in SysF_PTS.lib]C
cm_vdP [in SysF_PTS.sysf_pts]cm_trTypePF [in SysF_PTS.sysf_pts]
cm_typingP [in SysF_PTS.sysf_pts]
cm_istyP [in SysF_PTS.sysf_pts]
comb [in SysF_PTS.lib]
cr [in SysF_PTS.lib]
cr_typingPF [in SysF_PTS.sysf_pts]
cr_istyPF [in SysF_PTS.sysf_pts]
cr_typingFP [in SysF_PTS.sysf_pts]
cr_istyFP [in SysF_PTS.sysf_pts]
cr_typingP [in SysF_PTS.sysf_pts]
cr_istyP [in SysF_PTS.sysf_pts]
cr_typingF [in SysF_PTS.sysf_pts]
cr_istyF [in SysF_PTS.sysf_pts]
E
eqPrp [in SysF_PTS.sysf_pts]G
gentypingP [in SysF_PTS.sysf_pts]get [in SysF_PTS.lib]
getD [in SysF_PTS.lib]
S
subst_coinc [in SysF_PTS.lib]sum2bool [in SysF_PTS.lib]
T
trTermFP [in SysF_PTS.sysf_pts]trTermPF [in SysF_PTS.sysf_pts]
trTypeFP [in SysF_PTS.sysf_pts]
trTypePF [in SysF_PTS.sysf_pts]
| 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 | (269 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 | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (130 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 | (41 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) |
| 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 | (12 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) |
| 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) |
| 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 | (25 entries) |