| 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 | (1116 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 | (50 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 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 | (13 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 | (271 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 | (83 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) |
| 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 | (16 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 | (71 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 | (40 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 | (232 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 | (216 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 | (30 entries) |
Global Index
A
accn [inductive, in Rec.Base.ARS]accnH [constructor, in Rec.Base.ARS]
accnL [constructor, in Rec.Base.ARS]
accn_inv [lemma, in Rec.Base.ARS]
accn_ind' [definition, in Rec.Base.ARS]
admissible [definition, in Rec.Examples.sysf_const_sn]
ad_cons [lemma, in Rec.Examples.sysf_const_sn]
ARS [library]
axioms [library]
B
beta_expansion [lemma, in Rec.Examples.sysf_const_sn]bound [definition, in Rec.Base.fintype]
box [definition, in Rec.Framework.graded]
BoxGraded1 [section, in Rec.Framework.graded]
BoxGraded1.V [variable, in Rec.Framework.graded]
BoxGraded2 [section, in Rec.Framework.graded]
BoxGraded2.V [variable, in Rec.Framework.graded]
box_igraded2 [definition, in Rec.Framework.graded]
box_igraded2_mixin [lemma, in Rec.Framework.graded]
box_cgraded2 [definition, in Rec.Framework.graded]
box_cgraded2_mixin [lemma, in Rec.Framework.graded]
box_graded2 [definition, in Rec.Framework.graded]
box_igraded1 [definition, in Rec.Framework.graded]
box_igraded1_mixin [lemma, in Rec.Framework.graded]
box_cgraded1 [definition, in Rec.Framework.graded]
box_cgraded1_mixin [lemma, in Rec.Framework.graded]
box_graded1 [definition, in Rec.Framework.graded]
box2 [definition, in Rec.Framework.graded]
C
cand [definition, in Rec.Examples.sysf_const_sn]CGraded1 [module, in Rec.Framework.graded]
CGraded1.base [projection, in Rec.Framework.graded]
CGraded1.class [definition, in Rec.Framework.graded]
CGraded1.Class [constructor, in Rec.Framework.graded]
CGraded1.ClassDef [section, in Rec.Framework.graded]
CGraded1.ClassDef.cT [variable, in Rec.Framework.graded]
CGraded1.ClassDef.T [variable, in Rec.Framework.graded]
CGraded1.ClassDef.xT [variable, in Rec.Framework.graded]
CGraded1.class_of [record, in Rec.Framework.graded]
CGraded1.clone [definition, in Rec.Framework.graded]
CGraded1.Exports [module, in Rec.Framework.graded]
CGraded1.Exports.CGraded1 [abbreviation, in Rec.Framework.graded]
CGraded1.Exports.cgraded1 [abbreviation, in Rec.Framework.graded]
[ cgraded1 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ cgraded1 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
CGraded1.graded1 [definition, in Rec.Framework.graded]
CGraded1.mixin [projection, in Rec.Framework.graded]
CGraded1.mixin_of [definition, in Rec.Framework.graded]
CGraded1.pack [definition, in Rec.Framework.graded]
CGraded1.Pack [constructor, in Rec.Framework.graded]
CGraded1.sort [projection, in Rec.Framework.graded]
CGraded1.type [record, in Rec.Framework.graded]
CGraded1.xclass [abbreviation, in Rec.Framework.graded]
CGraded2 [module, in Rec.Framework.graded]
CGraded2.base [projection, in Rec.Framework.graded]
CGraded2.class [definition, in Rec.Framework.graded]
CGraded2.Class [constructor, in Rec.Framework.graded]
CGraded2.ClassDef [section, in Rec.Framework.graded]
CGraded2.ClassDef.cT [variable, in Rec.Framework.graded]
CGraded2.ClassDef.T [variable, in Rec.Framework.graded]
CGraded2.ClassDef.xT [variable, in Rec.Framework.graded]
CGraded2.class_of [record, in Rec.Framework.graded]
CGraded2.clone [definition, in Rec.Framework.graded]
CGraded2.Exports [module, in Rec.Framework.graded]
CGraded2.Exports.CGraded2 [abbreviation, in Rec.Framework.graded]
CGraded2.Exports.cgraded2 [abbreviation, in Rec.Framework.graded]
[ cgraded2 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ cgraded2 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
CGraded2.graded2 [definition, in Rec.Framework.graded]
CGraded2.mixin [projection, in Rec.Framework.graded]
CGraded2.mixin_of [definition, in Rec.Framework.graded]
CGraded2.pack [definition, in Rec.Framework.graded]
CGraded2.Pack [constructor, in Rec.Framework.graded]
CGraded2.sort [projection, in Rec.Framework.graded]
CGraded2.type [record, in Rec.Framework.graded]
CGraded2.xclass [abbreviation, in Rec.Framework.graded]
cofinal [definition, in Rec.Base.ARS]
CoFinal [section, in Rec.Base.ARS]
cofinal_normalizing [lemma, in Rec.Base.ARS]
CoFinal.e [variable, in Rec.Base.ARS]
CoFinal.rho [variable, in Rec.Base.ARS]
CoFinal.T [variable, in Rec.Base.ARS]
CoFinal.tri [variable, in Rec.Base.ARS]
com [definition, in Rec.Base.ARS]
Commutation [section, in Rec.Base.ARS]
Commutation.T [variable, in Rec.Base.ARS]
ComputationN [section, in Rec.Base.ARS]
ComputationN.classical [variable, in Rec.Base.ARS]
ComputationN.e [variable, in Rec.Base.ARS]
ComputationN.norm [variable, in Rec.Base.ARS]
ComputationN.rho [variable, in Rec.Base.ARS]
ComputationN.sound [variable, in Rec.Base.ARS]
ComputationN.T [variable, in Rec.Base.ARS]
com_lift [lemma, in Rec.Base.ARS]
com_strip [lemma, in Rec.Base.ARS]
confluent [definition, in Rec.Base.ARS]
confluent_stable [lemma, in Rec.Base.ARS]
confluent_cr [lemma, in Rec.Base.ARS]
ConstGraded1 [section, in Rec.Framework.graded]
ConstGraded1.T [variable, in Rec.Framework.graded]
ConstGraded2 [section, in Rec.Framework.graded]
ConstGraded2.T [variable, in Rec.Framework.graded]
constl [definition, in Rec.Framework.graded]
constl_pgraded2 [definition, in Rec.Framework.graded]
constl_pgraded2_mixin [lemma, in Rec.Framework.graded]
constl_igraded2 [definition, in Rec.Framework.graded]
constl_igraded2_mixin [lemma, in Rec.Framework.graded]
constl_cgraded2_mixin [lemma, in Rec.Framework.graded]
constl_graded2 [definition, in Rec.Framework.graded]
constl_th2 [definition, in Rec.Framework.graded]
constr [definition, in Rec.Framework.graded]
constr_pgraded2 [definition, in Rec.Framework.graded]
constr_pgraded2_mixin [lemma, in Rec.Framework.graded]
constr_igraded2 [definition, in Rec.Framework.graded]
constr_igraded2_mixin [lemma, in Rec.Framework.graded]
constr_cgraded2_mixin [lemma, in Rec.Framework.graded]
constr_graded2 [definition, in Rec.Framework.graded]
constr_th2 [definition, in Rec.Framework.graded]
const_pgraded2 [definition, in Rec.Framework.graded]
const_pgraded2_mixin [lemma, in Rec.Framework.graded]
const_igraded2 [definition, in Rec.Framework.graded]
const_igraded2_mixin [lemma, in Rec.Framework.graded]
const_cgraded2 [definition, in Rec.Framework.graded]
const_cgraded2_mixin [lemma, in Rec.Framework.graded]
const_graded2 [definition, in Rec.Framework.graded]
const_pgraded1 [definition, in Rec.Framework.graded]
const_pgraded1_mixin [lemma, in Rec.Framework.graded]
const_igraded1 [definition, in Rec.Framework.graded]
const_igraded1_mixin [lemma, in Rec.Framework.graded]
const_cgraded1 [definition, in Rec.Framework.graded]
const_cgraded1_mixin [lemma, in Rec.Framework.graded]
const_graded1 [definition, in Rec.Framework.graded]
const1 [definition, in Rec.Framework.graded]
const2 [definition, in Rec.Framework.graded]
context_morphism [lemma, in Rec.Examples.sysf_typing]
contl_cgraded2 [definition, in Rec.Framework.graded]
contr_cgraded2 [definition, in Rec.Framework.graded]
conv [inductive, in Rec.Base.ARS]
convES [lemma, in Rec.Base.ARS]
convESi [lemma, in Rec.Base.ARS]
convR [constructor, in Rec.Base.ARS]
convSE [constructor, in Rec.Base.ARS]
convSEi [constructor, in Rec.Base.ARS]
conv_closure [lemma, in Rec.Base.ARS]
conv_hom [lemma, in Rec.Base.ARS]
conv_img [lemma, in Rec.Base.ARS]
conv_sym [lemma, in Rec.Base.ARS]
conv_trans [lemma, in Rec.Base.ARS]
conv1 [lemma, in Rec.Base.ARS]
conv1i [lemma, in Rec.Base.ARS]
CR [definition, in Rec.Base.ARS]
cr_method [lemma, in Rec.Base.ARS]
cr_conv_normal [lemma, in Rec.Base.ARS]
cr_star_normal [lemma, in Rec.Base.ARS]
ctx [definition, in Rec.Examples.sysf_const_sn]
cvl [abbreviation, in Rec.Examples.sysf_wn]
cvls [definition, in Rec.Examples.sysf_wn]
D
Definitions [section, in Rec.Base.ARS]Definitions.e [variable, in Rec.Base.ARS]
Definitions.T [variable, in Rec.Base.ARS]
diamond [definition, in Rec.Base.ARS]
diamond_confluent [lemma, in Rec.Base.ARS]
E
E [abbreviation, in Rec.Examples.sysf_wn]E [abbreviation, in Rec.Examples.sysf_const_sn]
eq_star [lemma, in Rec.Base.ARS]
eval [inductive, in Rec.Examples.sysf_wn]
evaln [definition, in Rec.Base.ARS]
evalnP [lemma, in Rec.Base.ARS]
evaln_sound [lemma, in Rec.Base.ARS]
eval_App [constructor, in Rec.Examples.sysf_wn]
eval_app [constructor, in Rec.Examples.sysf_wn]
eval_val [constructor, in Rec.Examples.sysf_wn]
ev_inst [lemma, in Rec.Extras.lambda_model]
ev_lam [lemma, in Rec.Extras.lambda_model]
ev_app [lemma, in Rec.Extras.lambda_model]
ev_var [lemma, in Rec.Extras.lambda_model]
F
fin [definition, in Rec.Base.fintype]fintype [library]
fin_pgraded1 [definition, in Rec.Framework.graded]
fin_pgraded1_mixin [lemma, in Rec.Framework.graded]
fin_igraded1 [definition, in Rec.Framework.graded]
fin_igraded1_mixin [lemma, in Rec.Framework.graded]
fin_cgraded1 [definition, in Rec.Framework.graded]
fin_cgraded1_mixin [lemma, in Rec.Framework.graded]
fin_graded1 [definition, in Rec.Framework.graded]
fin_th1 [definition, in Rec.Framework.graded]
fin2 [definition, in Rec.Framework.graded]
fundamental_theorem [lemma, in Rec.Examples.sysf_wn]
G
graded [library]Graded1 [module, in Rec.Framework.graded]
Graded1.class [definition, in Rec.Framework.graded]
Graded1.class_of [abbreviation, in Rec.Framework.graded]
Graded1.clone [definition, in Rec.Framework.graded]
Graded1.Defs [section, in Rec.Framework.graded]
Graded1.Defs.cT [variable, in Rec.Framework.graded]
Graded1.Defs.p [variable, in Rec.Framework.graded]
Graded1.Exports [module, in Rec.Framework.graded]
Graded1.Exports.Graded1 [abbreviation, in Rec.Framework.graded]
Graded1.Exports.graded1 [abbreviation, in Rec.Framework.graded]
[ graded1 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ graded1 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
Graded1.mixin_of [definition, in Rec.Framework.graded]
Graded1.pack [definition, in Rec.Framework.graded]
Graded1.Pack [constructor, in Rec.Framework.graded]
Graded1.sort [projection, in Rec.Framework.graded]
Graded1.type [record, in Rec.Framework.graded]
Graded2 [module, in Rec.Framework.graded]
Graded2.class [definition, in Rec.Framework.graded]
Graded2.class_of [abbreviation, in Rec.Framework.graded]
Graded2.clone [definition, in Rec.Framework.graded]
Graded2.Defs [section, in Rec.Framework.graded]
Graded2.Defs.cT [variable, in Rec.Framework.graded]
Graded2.Defs.p [variable, in Rec.Framework.graded]
Graded2.Exports [module, in Rec.Framework.graded]
Graded2.Exports.Graded2 [abbreviation, in Rec.Framework.graded]
Graded2.Exports.graded2 [abbreviation, in Rec.Framework.graded]
[ graded2 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ graded2 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
Graded2.mixin_of [definition, in Rec.Framework.graded]
Graded2.pack [definition, in Rec.Framework.graded]
Graded2.Pack [constructor, in Rec.Framework.graded]
Graded2.sort [projection, in Rec.Framework.graded]
Graded2.type [record, in Rec.Framework.graded]
H
has_type [inductive, in Rec.Examples.sysf_const_sn]I
id [definition, in Rec.Extras.sysf_print]idren [definition, in Rec.Base.fintype]
IGraded1 [module, in Rec.Framework.graded]
IGraded1.base [projection, in Rec.Framework.graded]
IGraded1.class [definition, in Rec.Framework.graded]
IGraded1.Class [constructor, in Rec.Framework.graded]
IGraded1.ClassDef [section, in Rec.Framework.graded]
IGraded1.ClassDef.cT [variable, in Rec.Framework.graded]
IGraded1.ClassDef.T [variable, in Rec.Framework.graded]
IGraded1.ClassDef.xT [variable, in Rec.Framework.graded]
IGraded1.class_of [record, in Rec.Framework.graded]
IGraded1.clone [definition, in Rec.Framework.graded]
IGraded1.Exports [module, in Rec.Framework.graded]
IGraded1.Exports.IGraded1 [abbreviation, in Rec.Framework.graded]
IGraded1.Exports.igraded1 [abbreviation, in Rec.Framework.graded]
[ igraded1 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ igraded1 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
IGraded1.graded1 [definition, in Rec.Framework.graded]
IGraded1.mixin [projection, in Rec.Framework.graded]
IGraded1.mixin_of [definition, in Rec.Framework.graded]
IGraded1.pack [definition, in Rec.Framework.graded]
IGraded1.Pack [constructor, in Rec.Framework.graded]
IGraded1.sort [projection, in Rec.Framework.graded]
IGraded1.type [record, in Rec.Framework.graded]
IGraded1.xclass [abbreviation, in Rec.Framework.graded]
IGraded2 [module, in Rec.Framework.graded]
IGraded2.base [projection, in Rec.Framework.graded]
IGraded2.class [definition, in Rec.Framework.graded]
IGraded2.Class [constructor, in Rec.Framework.graded]
IGraded2.ClassDef [section, in Rec.Framework.graded]
IGraded2.ClassDef.cT [variable, in Rec.Framework.graded]
IGraded2.ClassDef.T [variable, in Rec.Framework.graded]
IGraded2.ClassDef.xT [variable, in Rec.Framework.graded]
IGraded2.class_of [record, in Rec.Framework.graded]
IGraded2.clone [definition, in Rec.Framework.graded]
IGraded2.Exports [module, in Rec.Framework.graded]
IGraded2.Exports.IGraded2 [abbreviation, in Rec.Framework.graded]
IGraded2.Exports.igraded2 [abbreviation, in Rec.Framework.graded]
[ igraded2 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ igraded2 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
IGraded2.graded2 [definition, in Rec.Framework.graded]
IGraded2.mixin [projection, in Rec.Framework.graded]
IGraded2.mixin_of [definition, in Rec.Framework.graded]
IGraded2.pack [definition, in Rec.Framework.graded]
IGraded2.Pack [constructor, in Rec.Framework.graded]
IGraded2.sort [projection, in Rec.Framework.graded]
IGraded2.type [record, in Rec.Framework.graded]
IGraded2.xclass [abbreviation, in Rec.Framework.graded]
im [definition, in Rec.Framework.graded]
im_comp [lemma, in Rec.Framework.graded]
im_id [lemma, in Rec.Framework.graded]
im_injective [lemma, in Rec.Framework.graded]
im_inj [lemma, in Rec.Framework.graded]
im_exists2 [lemma, in Rec.Examples.sysf_typing]
im_eq [lemma, in Rec.Examples.sysf_typing]
inst_expansion [lemma, in Rec.Examples.sysf_const_sn]
iren [record, in Rec.Base.fintype]
IRen [constructor, in Rec.Base.fintype]
iren_eq [lemma, in Rec.Base.fintype]
iren_inj [projection, in Rec.Base.fintype]
iren_fun [projection, in Rec.Base.fintype]
J
joinable [definition, in Rec.Base.ARS]join_conv [lemma, in Rec.Base.ARS]
L
L [abbreviation, in Rec.Examples.sysf_wn]LambdaModel [section, in Rec.Extras.lambda_model]
LambdaModel.app [variable, in Rec.Extras.lambda_model]
LambdaModel.beta [variable, in Rec.Extras.lambda_model]
LambdaModel.D [variable, in Rec.Extras.lambda_model]
LambdaModel.lam [variable, in Rec.Extras.lambda_model]
⟦ _ ⟧ _ [notation, in Rec.Extras.lambda_model]
LambdaTerms [module, in Rec.Extras.lambda_terms]
LambdaTerms.app [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.base [projection, in Rec.Extras.lambda_terms]
LambdaTerms.Defs [section, in Rec.Extras.lambda_terms]
LambdaTerms.Defs.EvalRen [section, in Rec.Extras.lambda_terms]
_ .[ _ ] (tm_inst_scope) [notation, in Rec.Extras.lambda_terms]
{ model _ , _ } (type_scope) [notation, in Rec.Extras.lambda_terms]
_ ◁ _ [notation, in Rec.Extras.lambda_terms]
LambdaTerms.eval [definition, in Rec.Extras.lambda_terms]
LambdaTerms.eval_inst [definition, in Rec.Extras.lambda_terms]
LambdaTerms.eval_ren [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.Exports [module, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm [module, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.tm [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.app [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.embed [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval_inst [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval_ren [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_comp [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_id [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_ren [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_traversal [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.IsNatural [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.is_natural [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.lam [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.lift [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.Model [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.model [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.napp [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.naturality [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.nlam [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.nvar [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_inst [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_inj [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_comp [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_id [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_traversal [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.sapp [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_inst [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_ren [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_irrelevance [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.slam [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.SModel [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.smodel [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.svar [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tapp [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tlam [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.Traversal [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.traversal [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tvar [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.var [abbreviation, in Rec.Extras.lambda_terms]
_ .[ _ ] (tm_inst_scope) [notation, in Rec.Extras.lambda_terms]
_ ◁ _ (tm_inst_scope) [notation, in Rec.Extras.lambda_terms]
LambdaTerms.inst [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.inst_comp [definition, in Rec.Extras.lambda_terms]
LambdaTerms.inst_id [definition, in Rec.Extras.lambda_terms]
LambdaTerms.inst_traversal [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.IsNatural [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.is_natural [record, in Rec.Extras.lambda_terms]
LambdaTerms.lam [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.lift [definition, in Rec.Extras.lambda_terms]
LambdaTerms.lift_smodel [definition, in Rec.Extras.lambda_terms]
LambdaTerms.lift_embed [definition, in Rec.Extras.lambda_terms]
LambdaTerms.lift_model [definition, in Rec.Extras.lambda_terms]
LambdaTerms.lift_is_natural [definition, in Rec.Extras.lambda_terms]
LambdaTerms.model [record, in Rec.Extras.lambda_terms]
LambdaTerms.Model [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.model_is_natural [definition, in Rec.Extras.lambda_terms]
LambdaTerms.model_of [definition, in Rec.Extras.lambda_terms]
LambdaTerms.napp [projection, in Rec.Extras.lambda_terms]
LambdaTerms.naturality [definition, in Rec.Extras.lambda_terms]
LambdaTerms.nlam [projection, in Rec.Extras.lambda_terms]
LambdaTerms.nvar [projection, in Rec.Extras.lambda_terms]
LambdaTerms.ren_id [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.ren_inj [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.ren_comp [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.ren_model [definition, in Rec.Extras.lambda_terms]
LambdaTerms.ren_is_natural [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.ren_traversal [definition, in Rec.Extras.lambda_terms]
LambdaTerms.sapp [projection, in Rec.Extras.lambda_terms]
LambdaTerms.seval [definition, in Rec.Extras.lambda_terms]
LambdaTerms.seval_inst [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.seval_ren [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.seval_irrelevance [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.slam [projection, in Rec.Extras.lambda_terms]
LambdaTerms.smodel [record, in Rec.Extras.lambda_terms]
LambdaTerms.SModel [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.smodel_to_model [definition, in Rec.Extras.lambda_terms]
LambdaTerms.smodel_is_natural [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.smodel_to_traversal [definition, in Rec.Extras.lambda_terms]
LambdaTerms.svar [projection, in Rec.Extras.lambda_terms]
LambdaTerms.tapp [projection, in Rec.Extras.lambda_terms]
LambdaTerms.th1_tmE [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.tlam [projection, in Rec.Extras.lambda_terms]
LambdaTerms.tm [inductive, in Rec.Extras.lambda_terms]
LambdaTerms.tm_inst_ren [lemma, in Rec.Extras.lambda_terms]
LambdaTerms.tm_ren_inst [definition, in Rec.Extras.lambda_terms]
LambdaTerms.tm_pgraded1 [definition, in Rec.Extras.lambda_terms]
LambdaTerms.tm_igraded1 [definition, in Rec.Extras.lambda_terms]
LambdaTerms.tm_cgraded1 [definition, in Rec.Extras.lambda_terms]
LambdaTerms.tm_graded1 [definition, in Rec.Extras.lambda_terms]
LambdaTerms.tm_ren [abbreviation, in Rec.Extras.lambda_terms]
LambdaTerms.traversal [record, in Rec.Extras.lambda_terms]
LambdaTerms.Traversal [constructor, in Rec.Extras.lambda_terms]
LambdaTerms.tvar [projection, in Rec.Extras.lambda_terms]
LambdaTerms.var [constructor, in Rec.Extras.lambda_terms]
lambda_smodel [definition, in Rec.Extras.lambda_model]
lambda_terms [library]
lambda_model [library]
LeftCGraded1 [section, in Rec.Framework.graded]
LeftCGraded1.F [variable, in Rec.Framework.graded]
LeftCGraded1.n [variable, in Rec.Framework.graded]
LeftGraded1 [section, in Rec.Framework.graded]
LeftGraded1.F [variable, in Rec.Framework.graded]
LeftGraded1.n [variable, in Rec.Framework.graded]
LeftIGraded1 [section, in Rec.Framework.graded]
LeftIGraded1.F [variable, in Rec.Framework.graded]
LeftIGraded1.n [variable, in Rec.Framework.graded]
LeftPGraded1 [section, in Rec.Framework.graded]
LeftPGraded1.F [variable, in Rec.Framework.graded]
LeftPGraded1.n [variable, in Rec.Framework.graded]
left_pgraded1 [definition, in Rec.Framework.graded]
left_pgraded1_mixin [lemma, in Rec.Framework.graded]
left_igraded1 [definition, in Rec.Framework.graded]
left_igraded1_mixin [lemma, in Rec.Framework.graded]
left_cgraded1 [definition, in Rec.Framework.graded]
left_cgraded1_mixin [lemma, in Rec.Framework.graded]
left_graded1 [definition, in Rec.Framework.graded]
left_th1 [definition, in Rec.Framework.graded]
left1 [definition, in Rec.Framework.graded]
LiftCGrading [section, in Rec.Framework.graded]
LiftCGrading.F [variable, in Rec.Framework.graded]
LiftGrading [section, in Rec.Framework.graded]
LiftGrading.F [variable, in Rec.Framework.graded]
LiftIGrading [section, in Rec.Framework.graded]
LiftIGrading.F [variable, in Rec.Framework.graded]
LiftPGrading [section, in Rec.Framework.graded]
LiftPGrading.F [variable, in Rec.Framework.graded]
L_cl_star [lemma, in Rec.Examples.sysf_const_sn]
L_const [lemma, in Rec.Examples.sysf_const_sn]
L_var [lemma, in Rec.Examples.sysf_const_sn]
L_nc [lemma, in Rec.Examples.sysf_const_sn]
L_cl [lemma, in Rec.Examples.sysf_const_sn]
L_sn [lemma, in Rec.Examples.sysf_const_sn]
L_reducible [lemma, in Rec.Examples.sysf_const_sn]
N
nall [constructor, in Rec.Extras.sysf_print]narr [constructor, in Rec.Extras.sysf_print]
neutral [definition, in Rec.Examples.sysf_const_sn]
nf [definition, in Rec.Base.ARS]
nf_accn [lemma, in Rec.Base.ARS]
normal [definition, in Rec.Base.ARS]
normalizing [definition, in Rec.Base.ARS]
normal_star [lemma, in Rec.Base.ARS]
nty [inductive, in Rec.Extras.sysf_print]
null [definition, in Rec.Base.fintype]
nvar [constructor, in Rec.Extras.sysf_print]
P
pext [axiom, in Rec.Base.axioms]PGraded1 [module, in Rec.Framework.graded]
PGraded1.base [projection, in Rec.Framework.graded]
PGraded1.class [definition, in Rec.Framework.graded]
PGraded1.Class [constructor, in Rec.Framework.graded]
PGraded1.ClassDef [section, in Rec.Framework.graded]
PGraded1.ClassDef.cT [variable, in Rec.Framework.graded]
PGraded1.ClassDef.T [variable, in Rec.Framework.graded]
PGraded1.ClassDef.xT [variable, in Rec.Framework.graded]
PGraded1.class_of [record, in Rec.Framework.graded]
PGraded1.clone [definition, in Rec.Framework.graded]
PGraded1.Exports [module, in Rec.Framework.graded]
PGraded1.Exports.PGraded1 [abbreviation, in Rec.Framework.graded]
PGraded1.Exports.pgraded1 [abbreviation, in Rec.Framework.graded]
[ pgraded1 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ pgraded1 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
PGraded1.graded1 [definition, in Rec.Framework.graded]
PGraded1.mixin [projection, in Rec.Framework.graded]
PGraded1.mixin_of [definition, in Rec.Framework.graded]
PGraded1.pack [definition, in Rec.Framework.graded]
PGraded1.Pack [constructor, in Rec.Framework.graded]
PGraded1.sort [projection, in Rec.Framework.graded]
PGraded1.type [record, in Rec.Framework.graded]
PGraded1.xclass [abbreviation, in Rec.Framework.graded]
PGraded2 [module, in Rec.Framework.graded]
PGraded2.base [projection, in Rec.Framework.graded]
PGraded2.class [definition, in Rec.Framework.graded]
PGraded2.Class [constructor, in Rec.Framework.graded]
PGraded2.ClassDef [section, in Rec.Framework.graded]
PGraded2.ClassDef.cT [variable, in Rec.Framework.graded]
PGraded2.ClassDef.T [variable, in Rec.Framework.graded]
PGraded2.ClassDef.xT [variable, in Rec.Framework.graded]
PGraded2.class_of [record, in Rec.Framework.graded]
PGraded2.clone [definition, in Rec.Framework.graded]
PGraded2.Exports [module, in Rec.Framework.graded]
PGraded2.Exports.PGraded2 [abbreviation, in Rec.Framework.graded]
PGraded2.Exports.pgraded2 [abbreviation, in Rec.Framework.graded]
[ pgraded2 of _ ] (form_scope) [notation, in Rec.Framework.graded]
[ pgraded2 of _ for _ ] (form_scope) [notation, in Rec.Framework.graded]
PGraded2.graded2 [definition, in Rec.Framework.graded]
PGraded2.mixin [projection, in Rec.Framework.graded]
PGraded2.mixin_of [definition, in Rec.Framework.graded]
PGraded2.pack [definition, in Rec.Framework.graded]
PGraded2.Pack [constructor, in Rec.Framework.graded]
PGraded2.sort [projection, in Rec.Framework.graded]
PGraded2.type [record, in Rec.Framework.graded]
PGraded2.xclass [abbreviation, in Rec.Framework.graded]
pi [lemma, in Rec.Base.axioms]
Pred [definition, in Rec.Base.ARS]
PredCGrading [section, in Rec.Framework.graded]
PredCGrading.A [variable, in Rec.Framework.graded]
PredGrading [section, in Rec.Framework.graded]
PredGrading.A [variable, in Rec.Framework.graded]
PredIGrading [section, in Rec.Framework.graded]
PredIGrading.A [variable, in Rec.Framework.graded]
PredPGrading [section, in Rec.Framework.graded]
PredPGrading.A [variable, in Rec.Framework.graded]
pred_pgraded1 [definition, in Rec.Framework.graded]
pred_pgraded1_mixin [lemma, in Rec.Framework.graded]
pred_igraded1 [definition, in Rec.Framework.graded]
pred_igraded1_mixin [lemma, in Rec.Framework.graded]
pred_cgraded1 [definition, in Rec.Framework.graded]
pred_cgraded1_mixin [lemma, in Rec.Framework.graded]
pred_graded1 [definition, in Rec.Framework.graded]
pred_th1 [definition, in Rec.Framework.graded]
pred1 [definition, in Rec.Framework.graded]
preservation [lemma, in Rec.Examples.sysf_typing]
print [definition, in Rec.Extras.sysf_print]
printer [definition, in Rec.Extras.sysf_print]
print_smodel [definition, in Rec.Extras.sysf_print]
p_nc [projection, in Rec.Examples.sysf_const_sn]
p_cl [projection, in Rec.Examples.sysf_const_sn]
p_sn [projection, in Rec.Examples.sysf_const_sn]
R
rcomp [definition, in Rec.Base.fintype]red [definition, in Rec.Examples.sysf_const_sn]
reducible [record, in Rec.Examples.sysf_const_sn]
reducible [definition, in Rec.Base.ARS]
reducible_const [lemma, in Rec.Examples.sysf_const_sn]
reducible_sn [lemma, in Rec.Examples.sysf_const_sn]
red_beta [lemma, in Rec.Examples.sysf_const_sn]
red_compat [lemma, in Rec.Examples.sysf_const_sn]
red_inst [lemma, in Rec.Examples.sysf_const_sn]
red_tabs [lemma, in Rec.Examples.sysf_const_sn]
red_tapp [lemma, in Rec.Examples.sysf_const_sn]
red_abs [lemma, in Rec.Examples.sysf_const_sn]
red_app [lemma, in Rec.Examples.sysf_const_sn]
Rel [definition, in Rec.Base.ARS]
rel_preservation [lemma, in Rec.Examples.sysf_typing]
ren [definition, in Rec.Base.fintype]
rho_id [lemma, in Rec.Examples.sysf_const_sn]
S
S [definition, in Rec.Examples.sysf_const_sn]scons [definition, in Rec.Base.fintype]
scons_comp [lemma, in Rec.Base.fintype]
scons_eta_id [lemma, in Rec.Base.fintype]
scons_eta [lemma, in Rec.Base.fintype]
shift [definition, in Rec.Base.fintype]
shift_up [lemma, in Rec.Base.fintype]
shift_typing [lemma, in Rec.Examples.sysf_typing]
sn [abbreviation, in Rec.Examples.sysf_const_sn]
sn [inductive, in Rec.Base.ARS]
SNI [constructor, in Rec.Base.ARS]
sn_inst [lemma, in Rec.Examples.sysf_const_sn]
sn_tclosed [lemma, in Rec.Examples.sysf_const_sn]
sn_closed [lemma, in Rec.Examples.sysf_const_sn]
sn_wn [lemma, in Rec.Base.ARS]
sn_preimage [lemma, in Rec.Base.ARS]
soundness [lemma, in Rec.Examples.sysf_const_sn]
sred [definition, in Rec.Examples.sysf_const_sn]
star [inductive, in Rec.Base.ARS]
starES [lemma, in Rec.Base.ARS]
starR [constructor, in Rec.Base.ARS]
starSE [constructor, in Rec.Base.ARS]
star_interpolation [lemma, in Rec.Base.ARS]
star_monotone [lemma, in Rec.Base.ARS]
star_closure [lemma, in Rec.Base.ARS]
star_hom [lemma, in Rec.Base.ARS]
star_img [lemma, in Rec.Base.ARS]
star_conv [lemma, in Rec.Base.ARS]
star_trans [lemma, in Rec.Base.ARS]
star1 [lemma, in Rec.Base.ARS]
step [inductive, in Rec.Extras.lambda_model]
step [inductive, in Rec.Examples.sysf_const_sn]
step_invariant [lemma, in Rec.Extras.lambda_model]
step_lam [constructor, in Rec.Extras.lambda_model]
step_appR [constructor, in Rec.Extras.lambda_model]
step_appL [constructor, in Rec.Extras.lambda_model]
step_beta [constructor, in Rec.Extras.lambda_model]
step_inst [lemma, in Rec.Examples.sysf_const_sn]
step_eBeta [lemma, in Rec.Examples.sysf_const_sn]
step_ebeta [lemma, in Rec.Examples.sysf_const_sn]
step_tabs [constructor, in Rec.Examples.sysf_const_sn]
step_tapp [constructor, in Rec.Examples.sysf_const_sn]
step_abs [constructor, in Rec.Examples.sysf_const_sn]
step_appR [constructor, in Rec.Examples.sysf_const_sn]
step_appL [constructor, in Rec.Examples.sysf_const_sn]
step_Beta [constructor, in Rec.Examples.sysf_const_sn]
step_beta [constructor, in Rec.Examples.sysf_const_sn]
strong_normalisation [lemma, in Rec.Examples.sysf_const_sn]
sysf_types [library]
sysf_wn [library]
sysf_print [library]
sysf_const_sn [library]
sysf_const_terms [library]
sysf_terms [library]
sysf_typing [library]
T
Termination [section, in Rec.Base.ARS]Termination.cr [variable, in Rec.Base.ARS]
Termination.e [variable, in Rec.Base.ARS]
Termination.T [variable, in Rec.Base.ARS]
test [definition, in Rec.Extras.sysf_print]
th_inj2 [lemma, in Rec.Framework.graded]
th_id2 [lemma, in Rec.Framework.graded]
th_comp2 [lemma, in Rec.Framework.graded]
th_inj1 [lemma, in Rec.Framework.graded]
th_id1 [lemma, in Rec.Framework.graded]
th_comp1 [lemma, in Rec.Framework.graded]
th1 [definition, in Rec.Framework.graded]
th1_compR [lemma, in Rec.Framework.graded]
th1_compX [lemma, in Rec.Framework.graded]
th1_idX [lemma, in Rec.Framework.graded]
th1_leftE [lemma, in Rec.Framework.graded]
th1_predE [lemma, in Rec.Framework.graded]
th1_boxE [lemma, in Rec.Framework.graded]
th1_constE [lemma, in Rec.Framework.graded]
th1_finE [lemma, in Rec.Framework.graded]
th2 [definition, in Rec.Framework.graded]
th2_compR [lemma, in Rec.Framework.graded]
th2_compX [lemma, in Rec.Framework.graded]
th2_idX [lemma, in Rec.Framework.graded]
th2_boxE [lemma, in Rec.Framework.graded]
th2_constE [lemma, in Rec.Framework.graded]
th2_constrE [lemma, in Rec.Framework.graded]
th2_constlE [lemma, in Rec.Framework.graded]
TmVl [module, in Rec.Framework.sysf_const_terms]
TmVl [module, in Rec.Framework.sysf_terms]
TmVl.App [constructor, in Rec.Framework.sysf_const_terms]
TmVl.app [constructor, in Rec.Framework.sysf_const_terms]
TmVl.App [constructor, in Rec.Framework.sysf_terms]
TmVl.app [constructor, in Rec.Framework.sysf_terms]
TmVl.base [projection, in Rec.Framework.sysf_const_terms]
TmVl.base [projection, in Rec.Framework.sysf_terms]
TmVl.const [constructor, in Rec.Framework.sysf_const_terms]
TmVl.Defs [section, in Rec.Framework.sysf_const_terms]
TmVl.Defs [section, in Rec.Framework.sysf_terms]
TmVl.Defs.EvalRen [section, in Rec.Framework.sysf_const_terms]
TmVl.Defs.EvalRen [section, in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (tm_inst_scope) [notation, in Rec.Framework.sysf_const_terms]
_ .[ _ , _ ] (tm_inst_scope) [notation, in Rec.Framework.sysf_terms]
{ model _ , _ , _ , _ , _ } (type_scope) [notation, in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (vl_inst_scope) [notation, in Rec.Framework.sysf_terms]
TmVl.eval [definition, in Rec.Framework.sysf_const_terms]
TmVl.eval_inst [lemma, in Rec.Framework.sysf_const_terms]
TmVl.eval_ren [lemma, in Rec.Framework.sysf_const_terms]
TmVl.eval_tm_inst [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_vl_inst [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_vl_tm_inst [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_tm_ren [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_vl_ren [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_vl_tm_ren [lemma, in Rec.Framework.sysf_terms]
TmVl.eval_tm [definition, in Rec.Framework.sysf_terms]
TmVl.eval_vl [definition, in Rec.Framework.sysf_terms]
TmVl.Exports [module, in Rec.Framework.sysf_const_terms]
TmVl.Exports [module, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV [module, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.inst_traversal [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.IsNatural [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.is_natural [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.lift [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.model [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nApp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.napp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nLam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nlam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ntvl [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nvar [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ren_traversal [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tApp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tapp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tLam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tlam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.Traversal [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.traversal [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ttvl [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tvar [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm [module, in Rec.Framework.sysf_const_terms]
TmVl.Exports.tm [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm [module, in Rec.Framework.sysf_terms]
TmVl.Exports.tm [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.App [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.app [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.App [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.app [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.const [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.embed [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.embed [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval_inst [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval_ren [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval_inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_comp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_id [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_ren [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_traversal [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_comp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_id [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.IsNatural [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.is_natural [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Lam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.lam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.lift [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Model [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.model [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nApp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.napp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.naturality [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.naturality [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.nconst [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nLam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nlam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nvar [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_inst [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_inj [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_comp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_id [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_traversal [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_inj [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_comp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_id [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.tApp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tapp [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tconst [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tLam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tlam [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Traversal [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.traversal [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tvar [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tvl [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.var [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.Exports.Vl [module, in Rec.Framework.sysf_terms]
TmVl.Exports.vl [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.embed [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval_inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_comp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_id [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.Lam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.lam [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.naturality [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_inst [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_inj [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_comp [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_id [abbreviation, in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.var [abbreviation, in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (tm_inst_scope) [notation, in Rec.Framework.sysf_const_terms]
_ ◁ ( _ , _ ) (tm_inst_scope) [notation, in Rec.Framework.sysf_const_terms]
_ .[ _ , _ ] (tm_inst_scope) [notation, in Rec.Framework.sysf_terms]
_ ◁ ( _ , _ ) (tm_inst_scope) [notation, in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (vl_inst_scope) [notation, in Rec.Framework.sysf_terms]
_ ◁ ( _ , _ ) (vl_inst_scope) [notation, in Rec.Framework.sysf_terms]
TmVl.inst_comp [lemma, in Rec.Framework.sysf_const_terms]
TmVl.inst_tm_id [definition, in Rec.Framework.sysf_const_terms]
TmVl.inst_tm [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.inst_traversal [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.inst_tm_comp [lemma, in Rec.Framework.sysf_terms]
TmVl.inst_vl_comp [lemma, in Rec.Framework.sysf_terms]
TmVl.inst_tm_id [definition, in Rec.Framework.sysf_terms]
TmVl.inst_vl_id [definition, in Rec.Framework.sysf_terms]
TmVl.inst_tm [abbreviation, in Rec.Framework.sysf_terms]
TmVl.inst_vl [abbreviation, in Rec.Framework.sysf_terms]
TmVl.inst_traversal [abbreviation, in Rec.Framework.sysf_terms]
TmVl.IsNatural [constructor, in Rec.Framework.sysf_const_terms]
TmVl.IsNatural [constructor, in Rec.Framework.sysf_terms]
TmVl.is_natural [record, in Rec.Framework.sysf_const_terms]
TmVl.is_natural [record, in Rec.Framework.sysf_terms]
TmVl.Lam [constructor, in Rec.Framework.sysf_const_terms]
TmVl.lam [constructor, in Rec.Framework.sysf_const_terms]
TmVl.Lam [constructor, in Rec.Framework.sysf_terms]
TmVl.lam [constructor, in Rec.Framework.sysf_terms]
TmVl.lift [definition, in Rec.Framework.sysf_const_terms]
TmVl.lift [definition, in Rec.Framework.sysf_terms]
TmVl.lift_embed [lemma, in Rec.Framework.sysf_const_terms]
TmVl.lift_model [definition, in Rec.Framework.sysf_const_terms]
TmVl.lift_is_natural [definition, in Rec.Framework.sysf_const_terms]
TmVl.lift_tm_embed [lemma, in Rec.Framework.sysf_terms]
TmVl.lift_vl_embed [lemma, in Rec.Framework.sysf_terms]
TmVl.lift_vl_tm_embed [definition, in Rec.Framework.sysf_terms]
TmVl.lift_model [definition, in Rec.Framework.sysf_terms]
TmVl.lift_is_natural [definition, in Rec.Framework.sysf_terms]
TmVl.model [record, in Rec.Framework.sysf_const_terms]
TmVl.Model [constructor, in Rec.Framework.sysf_const_terms]
TmVl.model [record, in Rec.Framework.sysf_terms]
TmVl.Model [constructor, in Rec.Framework.sysf_terms]
TmVl.model_is_natural [definition, in Rec.Framework.sysf_const_terms]
TmVl.model_is_natural [definition, in Rec.Framework.sysf_terms]
TmVl.model_of [definition, in Rec.Framework.sysf_terms]
TmVl.nApp [projection, in Rec.Framework.sysf_const_terms]
TmVl.napp [projection, in Rec.Framework.sysf_const_terms]
TmVl.nApp [projection, in Rec.Framework.sysf_terms]
TmVl.napp [projection, in Rec.Framework.sysf_terms]
TmVl.naturality [lemma, in Rec.Framework.sysf_const_terms]
TmVl.naturality_tm [lemma, in Rec.Framework.sysf_terms]
TmVl.naturality_vl [lemma, in Rec.Framework.sysf_terms]
TmVl.naturality_vl_tm [definition, in Rec.Framework.sysf_terms]
TmVl.nconst [projection, in Rec.Framework.sysf_const_terms]
TmVl.nLam [projection, in Rec.Framework.sysf_const_terms]
TmVl.nlam [projection, in Rec.Framework.sysf_const_terms]
TmVl.nLam [projection, in Rec.Framework.sysf_terms]
TmVl.nlam [projection, in Rec.Framework.sysf_terms]
TmVl.ntvl [projection, in Rec.Framework.sysf_terms]
TmVl.nvar [projection, in Rec.Framework.sysf_const_terms]
TmVl.nvar [projection, in Rec.Framework.sysf_terms]
TmVl.ren_tm_inj [lemma, in Rec.Framework.sysf_const_terms]
TmVl.ren_comp [lemma, in Rec.Framework.sysf_const_terms]
TmVl.ren_tm_id [lemma, in Rec.Framework.sysf_const_terms]
TmVl.ren_model [definition, in Rec.Framework.sysf_const_terms]
TmVl.ren_is_natural [lemma, in Rec.Framework.sysf_const_terms]
TmVl.ren_traversal [definition, in Rec.Framework.sysf_const_terms]
TmVl.ren_tm_inj [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_vl_inj [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_vl_tm_inj [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_tm_comp [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_vl_comp [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_tm_id [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_vl_id [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_vl_tm_id [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_model [definition, in Rec.Framework.sysf_terms]
TmVl.ren_is_natural [lemma, in Rec.Framework.sysf_terms]
TmVl.ren_traversal [definition, in Rec.Framework.sysf_terms]
TmVl.tApp [projection, in Rec.Framework.sysf_const_terms]
TmVl.tapp [projection, in Rec.Framework.sysf_const_terms]
TmVl.tApp [projection, in Rec.Framework.sysf_terms]
TmVl.tapp [projection, in Rec.Framework.sysf_terms]
TmVl.tconst [projection, in Rec.Framework.sysf_const_terms]
TmVl.th2_tmE [lemma, in Rec.Framework.sysf_const_terms]
TmVl.th2_tmE [lemma, in Rec.Framework.sysf_terms]
TmVl.th2_vlE [lemma, in Rec.Framework.sysf_terms]
TmVl.tLam [projection, in Rec.Framework.sysf_const_terms]
TmVl.tlam [projection, in Rec.Framework.sysf_const_terms]
TmVl.tLam [projection, in Rec.Framework.sysf_terms]
TmVl.tlam [projection, in Rec.Framework.sysf_terms]
TmVl.tm [inductive, in Rec.Framework.sysf_const_terms]
TmVl.tm [inductive, in Rec.Framework.sysf_terms]
TmVl.tm_inst_ren [lemma, in Rec.Framework.sysf_const_terms]
TmVl.tm_ren_inst [definition, in Rec.Framework.sysf_const_terms]
TmVl.tm_pgraded2 [definition, in Rec.Framework.sysf_const_terms]
TmVl.tm_cgraded2 [definition, in Rec.Framework.sysf_const_terms]
TmVl.tm_igraded2 [definition, in Rec.Framework.sysf_const_terms]
TmVl.tm_graded2 [definition, in Rec.Framework.sysf_const_terms]
TmVl.tm_ren [abbreviation, in Rec.Framework.sysf_const_terms]
TmVl.tm_inst_ren [lemma, in Rec.Framework.sysf_terms]
TmVl.tm_ren_inst [definition, in Rec.Framework.sysf_terms]
TmVl.tm_pgraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.tm_cgraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.tm_igraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.tm_graded2 [definition, in Rec.Framework.sysf_terms]
TmVl.tm_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.tm_ind [definition, in Rec.Framework.sysf_terms]
TmVl.traversal [record, in Rec.Framework.sysf_const_terms]
TmVl.Traversal [constructor, in Rec.Framework.sysf_const_terms]
TmVl.traversal [record, in Rec.Framework.sysf_terms]
TmVl.Traversal [constructor, in Rec.Framework.sysf_terms]
TmVl.ttvl [projection, in Rec.Framework.sysf_terms]
TmVl.tvar [projection, in Rec.Framework.sysf_const_terms]
TmVl.tvar [projection, in Rec.Framework.sysf_terms]
TmVl.tvl [constructor, in Rec.Framework.sysf_terms]
TmVl.tv_ind [definition, in Rec.Framework.sysf_terms]
TmVl.var [constructor, in Rec.Framework.sysf_const_terms]
TmVl.var [constructor, in Rec.Framework.sysf_terms]
TmVl.vl [inductive, in Rec.Framework.sysf_terms]
TmVl.vl_inst_ren [lemma, in Rec.Framework.sysf_terms]
TmVl.vl_ren_inst [definition, in Rec.Framework.sysf_terms]
TmVl.vl_pgraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.vl_cgraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.vl_igraded2 [definition, in Rec.Framework.sysf_terms]
TmVl.vl_graded2 [definition, in Rec.Framework.sysf_terms]
TmVl.vl_ren [abbreviation, in Rec.Framework.sysf_terms]
TmVl.vl_ind [definition, in Rec.Framework.sysf_terms]
tm_inst_compR [lemma, in Rec.Extras.lambda_terms]
tm_inst_compX [lemma, in Rec.Extras.lambda_terms]
tm_inst_idR [lemma, in Rec.Extras.lambda_terms]
tm_inst_idX [lemma, in Rec.Extras.lambda_terms]
tm_id_instX [lemma, in Rec.Extras.lambda_terms]
tm_inst_renR [lemma, in Rec.Extras.lambda_terms]
tm_inst_renX [lemma, in Rec.Extras.lambda_terms]
tm_ren_instR [lemma, in Rec.Extras.lambda_terms]
tm_ren_instX [lemma, in Rec.Extras.lambda_terms]
tm_ren_compR [lemma, in Rec.Extras.lambda_terms]
tm_ren_compX [lemma, in Rec.Extras.lambda_terms]
tm_ren_idX [lemma, in Rec.Extras.lambda_terms]
tm_inst_compR [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_compX [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_idR [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_idX [lemma, in Rec.Framework.sysf_const_terms]
tm_id_instX [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_renR [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_renX [lemma, in Rec.Framework.sysf_const_terms]
tm_ren_instR [lemma, in Rec.Framework.sysf_const_terms]
tm_ren_instX [lemma, in Rec.Framework.sysf_const_terms]
tm_ren_compR [lemma, in Rec.Framework.sysf_const_terms]
tm_ren_compX [lemma, in Rec.Framework.sysf_const_terms]
tm_ren_idX [lemma, in Rec.Framework.sysf_const_terms]
tm_inst_compR [lemma, in Rec.Framework.sysf_terms]
tm_inst_compX [lemma, in Rec.Framework.sysf_terms]
tm_inst_idX [lemma, in Rec.Framework.sysf_terms]
tm_inst_renR [lemma, in Rec.Framework.sysf_terms]
tm_inst_renX [lemma, in Rec.Framework.sysf_terms]
tm_ren_instR [lemma, in Rec.Framework.sysf_terms]
tm_ren_instX [lemma, in Rec.Framework.sysf_terms]
tm_ren_compR [lemma, in Rec.Framework.sysf_terms]
tm_ren_compX [lemma, in Rec.Framework.sysf_terms]
tm_ren_idX [lemma, in Rec.Framework.sysf_terms]
tm_sty [definition, in Rec.Examples.sysf_wn]
tm_ty_ind [definition, in Rec.Examples.sysf_wn]
tm_ty_App [constructor, in Rec.Examples.sysf_wn]
tm_ty_app [constructor, in Rec.Examples.sysf_wn]
tm_ty_vl [constructor, in Rec.Examples.sysf_wn]
tm_ty [inductive, in Rec.Examples.sysf_wn]
tm_rel_mono [lemma, in Rec.Examples.sysf_typing]
tm_frel_mono [lemma, in Rec.Examples.sysf_typing]
tm_rel [abbreviation, in Rec.Examples.sysf_typing]
tm_frel [abbreviation, in Rec.Examples.sysf_typing]
tm_type [abbreviation, in Rec.Examples.sysf_typing]
tm_sty [definition, in Rec.Examples.sysf_const_sn]
triangle [definition, in Rec.Base.ARS]
triangle_cofinal [lemma, in Rec.Base.ARS]
triangle_monotone [lemma, in Rec.Base.ARS]
triangle_diamond [lemma, in Rec.Base.ARS]
TrivialGraded1 [section, in Rec.Framework.graded]
tv_monotone [lemma, in Rec.Examples.sysf_typing]
type_of_model [definition, in Rec.Examples.sysf_typing]
type_of_is_natural [lemma, in Rec.Examples.sysf_typing]
type_of_App [lemma, in Rec.Examples.sysf_typing]
type_of_app [lemma, in Rec.Examples.sysf_typing]
type_of_tvl [lemma, in Rec.Examples.sysf_typing]
type_of_Lam [lemma, in Rec.Examples.sysf_typing]
type_of_lam [lemma, in Rec.Examples.sysf_typing]
type_of_var [lemma, in Rec.Examples.sysf_typing]
type_of_traversal [definition, in Rec.Examples.sysf_typing]
type_E [lemma, in Rec.Examples.sysf_const_sn]
TyTerms [module, in Rec.Framework.sysf_types]
TyTerms.all [constructor, in Rec.Framework.sysf_types]
TyTerms.arr [constructor, in Rec.Framework.sysf_types]
TyTerms.base [projection, in Rec.Framework.sysf_types]
TyTerms.Defs [section, in Rec.Framework.sysf_types]
TyTerms.Defs.Embedding [section, in Rec.Framework.sysf_types]
TyTerms.Defs.Embedding.var_is_natural [variable, in Rec.Framework.sysf_types]
TyTerms.Defs.EvalRen [section, in Rec.Framework.sysf_types]
_ .[ _ ] (ty_inst_scope) [notation, in Rec.Framework.sysf_types]
_ ◁ _ [notation, in Rec.Framework.sysf_types]
TyTerms.eval [definition, in Rec.Framework.sysf_types]
TyTerms.eval_inst [lemma, in Rec.Framework.sysf_types]
TyTerms.eval_ren [lemma, in Rec.Framework.sysf_types]
TyTerms.Exports [module, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty [module, in Rec.Framework.sysf_types]
TyTerms.Exports.ty [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.all [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.arr [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.embed [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval_inst [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval_ren [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_comp [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_id [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_ren [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_traversal [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.IsNatural [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.is_natural [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.lift [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.Model [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.model [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.nall [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.narr [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.naturality [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.nvar [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_inst [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_inj [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_comp [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_id [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_traversal [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.sall [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.sarr [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_inst [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_ren [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_irrelevance [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.SModel [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.smodel [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.svar [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tall [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tarr [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.Traversal [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.traversal [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tvar [abbreviation, in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.var [abbreviation, in Rec.Framework.sysf_types]
_ .[ _ ] (ty_inst_scope) [notation, in Rec.Framework.sysf_types]
_ ◁ _ (ty_inst_scope) [notation, in Rec.Framework.sysf_types]
TyTerms.inst [abbreviation, in Rec.Framework.sysf_types]
TyTerms.inst_comp [definition, in Rec.Framework.sysf_types]
TyTerms.inst_id [lemma, in Rec.Framework.sysf_types]
TyTerms.inst_traversal [abbreviation, in Rec.Framework.sysf_types]
TyTerms.IsNatural [constructor, in Rec.Framework.sysf_types]
TyTerms.is_natural [record, in Rec.Framework.sysf_types]
TyTerms.lift [definition, in Rec.Framework.sysf_types]
TyTerms.lift_smodel [definition, in Rec.Framework.sysf_types]
TyTerms.lift_embed [lemma, in Rec.Framework.sysf_types]
TyTerms.lift_model [definition, in Rec.Framework.sysf_types]
TyTerms.lift_is_natural [definition, in Rec.Framework.sysf_types]
TyTerms.lift_embed' [lemma, in Rec.Framework.sysf_types]
TyTerms.model [record, in Rec.Framework.sysf_types]
TyTerms.Model [constructor, in Rec.Framework.sysf_types]
TyTerms.model_is_natural [definition, in Rec.Framework.sysf_types]
TyTerms.nall [projection, in Rec.Framework.sysf_types]
TyTerms.narr [projection, in Rec.Framework.sysf_types]
TyTerms.naturality [lemma, in Rec.Framework.sysf_types]
TyTerms.nvar [projection, in Rec.Framework.sysf_types]
TyTerms.ren_is_inst [lemma, in Rec.Framework.sysf_types]
TyTerms.ren_model [definition, in Rec.Framework.sysf_types]
TyTerms.ren_is_natural [lemma, in Rec.Framework.sysf_types]
TyTerms.ren_id [lemma, in Rec.Framework.sysf_types]
TyTerms.ren_inj [lemma, in Rec.Framework.sysf_types]
TyTerms.ren_comp [lemma, in Rec.Framework.sysf_types]
TyTerms.ren_traversal [definition, in Rec.Framework.sysf_types]
TyTerms.sall [projection, in Rec.Framework.sysf_types]
TyTerms.sarr [projection, in Rec.Framework.sysf_types]
TyTerms.seval [definition, in Rec.Framework.sysf_types]
TyTerms.seval_inst [lemma, in Rec.Framework.sysf_types]
TyTerms.seval_ren [lemma, in Rec.Framework.sysf_types]
TyTerms.seval_irrelevance [lemma, in Rec.Framework.sysf_types]
TyTerms.smodel [record, in Rec.Framework.sysf_types]
TyTerms.SModel [constructor, in Rec.Framework.sysf_types]
TyTerms.smodel_to_model [definition, in Rec.Framework.sysf_types]
TyTerms.smodel_is_natural [lemma, in Rec.Framework.sysf_types]
TyTerms.smodel_to_traversal [definition, in Rec.Framework.sysf_types]
TyTerms.svar [projection, in Rec.Framework.sysf_types]
TyTerms.tall [projection, in Rec.Framework.sysf_types]
TyTerms.tarr [projection, in Rec.Framework.sysf_types]
TyTerms.th1_tyE [lemma, in Rec.Framework.sysf_types]
TyTerms.traversal [record, in Rec.Framework.sysf_types]
TyTerms.Traversal [constructor, in Rec.Framework.sysf_types]
TyTerms.tvar [projection, in Rec.Framework.sysf_types]
TyTerms.ty [inductive, in Rec.Framework.sysf_types]
TyTerms.ty_inst_ren [lemma, in Rec.Framework.sysf_types]
TyTerms.ty_ren_inst [definition, in Rec.Framework.sysf_types]
TyTerms.ty_pgraded1 [definition, in Rec.Framework.sysf_types]
TyTerms.ty_igraded1 [definition, in Rec.Framework.sysf_types]
TyTerms.ty_cgraded1 [definition, in Rec.Framework.sysf_types]
TyTerms.ty_graded1 [definition, in Rec.Framework.sysf_types]
TyTerms.ty_ren [abbreviation, in Rec.Framework.sysf_types]
TyTerms.var [constructor, in Rec.Framework.sysf_types]
ty_inst_compR [lemma, in Rec.Framework.sysf_types]
ty_inst_compX [lemma, in Rec.Framework.sysf_types]
ty_inst_idR [lemma, in Rec.Framework.sysf_types]
ty_inst_idX [lemma, in Rec.Framework.sysf_types]
ty_id_instX [lemma, in Rec.Framework.sysf_types]
ty_inst_renR [lemma, in Rec.Framework.sysf_types]
ty_inst_renX [lemma, in Rec.Framework.sysf_types]
ty_ren_instR [lemma, in Rec.Framework.sysf_types]
ty_ren_instX [lemma, in Rec.Framework.sysf_types]
ty_ren_compR [lemma, in Rec.Framework.sysf_types]
ty_ren_compX [lemma, in Rec.Framework.sysf_types]
ty_ren_idX [lemma, in Rec.Framework.sysf_types]
ty_tapp [constructor, in Rec.Examples.sysf_const_sn]
ty_tabs [constructor, in Rec.Examples.sysf_const_sn]
ty_app [constructor, in Rec.Examples.sysf_const_sn]
ty_abs [constructor, in Rec.Examples.sysf_const_sn]
ty_var [constructor, in Rec.Examples.sysf_const_sn]
U
up [definition, in Rec.Base.fintype]V
V [abbreviation, in Rec.Examples.sysf_wn]vl_inst_compR [lemma, in Rec.Framework.sysf_terms]
vl_inst_compX [lemma, in Rec.Framework.sysf_terms]
vl_inst_idR [lemma, in Rec.Framework.sysf_terms]
vl_inst_idX [lemma, in Rec.Framework.sysf_terms]
vl_id_instX [lemma, in Rec.Framework.sysf_terms]
vl_inst_renR [lemma, in Rec.Framework.sysf_terms]
vl_inst_renX [lemma, in Rec.Framework.sysf_terms]
vl_ren_instR [lemma, in Rec.Framework.sysf_terms]
vl_ren_instX [lemma, in Rec.Framework.sysf_terms]
vl_ren_compR [lemma, in Rec.Framework.sysf_terms]
vl_ren_compX [lemma, in Rec.Framework.sysf_terms]
vl_ren_idX [lemma, in Rec.Framework.sysf_terms]
vl_sty [definition, in Rec.Examples.sysf_wn]
vl_ty_ind [definition, in Rec.Examples.sysf_wn]
vl_ty_Lam [constructor, in Rec.Examples.sysf_wn]
vl_ty_lam [constructor, in Rec.Examples.sysf_wn]
vl_ty_var [constructor, in Rec.Examples.sysf_wn]
vl_ty [inductive, in Rec.Examples.sysf_wn]
vl_tvar_shift [lemma, in Rec.Examples.sysf_typing]
vl_rel [abbreviation, in Rec.Examples.sysf_typing]
vl_frel [abbreviation, in Rec.Examples.sysf_typing]
vl_type [abbreviation, in Rec.Examples.sysf_typing]
Vs [definition, in Rec.Examples.sysf_wn]
vt_ty_ind [definition, in Rec.Examples.sysf_wn]
W
W [definition, in Rec.Examples.sysf_wn]weak_normalisation [lemma, in Rec.Examples.sysf_wn]
wn [definition, in Rec.Base.ARS]
wn_accn [lemma, in Rec.Base.ARS]
other
_ ⋅ ( _ , _ ) (graded_scope) [notation, in Rec.Framework.graded]_ ⋅ ( _ ) (graded_scope) [notation, in Rec.Framework.graded]
_ ⋅ _ (graded_scope) [notation, in Rec.Framework.graded]
_ <=>2 _ (prop_scope) [notation, in Rec.Base.ARS]
_ <=2 _ (prop_scope) [notation, in Rec.Base.ARS]
_ >>> _ (subst_scope) [notation, in Rec.Base.fintype]
_ .: _ (subst_scope) [notation, in Rec.Base.fintype]
_ >> _ (subst_scope) [notation, in Rec.Base.fintype]
_ → _ [notation, in Rec.Extras.sysf_print]
[ tm _ ⊢ _ : _ ] [notation, in Rec.Examples.sysf_typing]
[ vl _ ⊢ _ : _ ] [notation, in Rec.Examples.sysf_typing]
∀ _ .. _ , _ [notation, in Rec.Extras.sysf_print]
☐ _ [notation, in Rec.Framework.graded]
☐₂ _ [notation, in Rec.Framework.graded]
Notation Index
C
[ cgraded1 of _ ] (form_scope) [in Rec.Framework.graded][ cgraded1 of _ for _ ] (form_scope) [in Rec.Framework.graded]
[ cgraded2 of _ ] (form_scope) [in Rec.Framework.graded]
[ cgraded2 of _ for _ ] (form_scope) [in Rec.Framework.graded]
G
[ graded1 of _ ] (form_scope) [in Rec.Framework.graded][ graded1 of _ for _ ] (form_scope) [in Rec.Framework.graded]
[ graded2 of _ ] (form_scope) [in Rec.Framework.graded]
[ graded2 of _ for _ ] (form_scope) [in Rec.Framework.graded]
I
[ igraded1 of _ ] (form_scope) [in Rec.Framework.graded][ igraded1 of _ for _ ] (form_scope) [in Rec.Framework.graded]
[ igraded2 of _ ] (form_scope) [in Rec.Framework.graded]
[ igraded2 of _ for _ ] (form_scope) [in Rec.Framework.graded]
L
⟦ _ ⟧ _ [in Rec.Extras.lambda_model]_ .[ _ ] (tm_inst_scope) [in Rec.Extras.lambda_terms]
{ model _ , _ } (type_scope) [in Rec.Extras.lambda_terms]
_ ◁ _ [in Rec.Extras.lambda_terms]
_ .[ _ ] (tm_inst_scope) [in Rec.Extras.lambda_terms]
_ ◁ _ (tm_inst_scope) [in Rec.Extras.lambda_terms]
P
[ pgraded1 of _ ] (form_scope) [in Rec.Framework.graded][ pgraded1 of _ for _ ] (form_scope) [in Rec.Framework.graded]
[ pgraded2 of _ ] (form_scope) [in Rec.Framework.graded]
[ pgraded2 of _ for _ ] (form_scope) [in Rec.Framework.graded]
T
_ .[ _ , _ ] (tm_inst_scope) [in Rec.Framework.sysf_const_terms]_ .[ _ , _ ] (tm_inst_scope) [in Rec.Framework.sysf_terms]
{ model _ , _ , _ , _ , _ } (type_scope) [in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (vl_inst_scope) [in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (tm_inst_scope) [in Rec.Framework.sysf_const_terms]
_ ◁ ( _ , _ ) (tm_inst_scope) [in Rec.Framework.sysf_const_terms]
_ .[ _ , _ ] (tm_inst_scope) [in Rec.Framework.sysf_terms]
_ ◁ ( _ , _ ) (tm_inst_scope) [in Rec.Framework.sysf_terms]
_ .[ _ , _ ] (vl_inst_scope) [in Rec.Framework.sysf_terms]
_ ◁ ( _ , _ ) (vl_inst_scope) [in Rec.Framework.sysf_terms]
_ .[ _ ] (ty_inst_scope) [in Rec.Framework.sysf_types]
_ ◁ _ [in Rec.Framework.sysf_types]
_ .[ _ ] (ty_inst_scope) [in Rec.Framework.sysf_types]
_ ◁ _ (ty_inst_scope) [in Rec.Framework.sysf_types]
other
_ ⋅ ( _ , _ ) (graded_scope) [in Rec.Framework.graded]_ ⋅ ( _ ) (graded_scope) [in Rec.Framework.graded]
_ ⋅ _ (graded_scope) [in Rec.Framework.graded]
_ <=>2 _ (prop_scope) [in Rec.Base.ARS]
_ <=2 _ (prop_scope) [in Rec.Base.ARS]
_ >>> _ (subst_scope) [in Rec.Base.fintype]
_ .: _ (subst_scope) [in Rec.Base.fintype]
_ >> _ (subst_scope) [in Rec.Base.fintype]
_ → _ [in Rec.Extras.sysf_print]
[ tm _ ⊢ _ : _ ] [in Rec.Examples.sysf_typing]
[ vl _ ⊢ _ : _ ] [in Rec.Examples.sysf_typing]
∀ _ .. _ , _ [in Rec.Extras.sysf_print]
☐ _ [in Rec.Framework.graded]
☐₂ _ [in Rec.Framework.graded]
Module Index
C
CGraded1 [in Rec.Framework.graded]CGraded1.Exports [in Rec.Framework.graded]
CGraded2 [in Rec.Framework.graded]
CGraded2.Exports [in Rec.Framework.graded]
G
Graded1 [in Rec.Framework.graded]Graded1.Exports [in Rec.Framework.graded]
Graded2 [in Rec.Framework.graded]
Graded2.Exports [in Rec.Framework.graded]
I
IGraded1 [in Rec.Framework.graded]IGraded1.Exports [in Rec.Framework.graded]
IGraded2 [in Rec.Framework.graded]
IGraded2.Exports [in Rec.Framework.graded]
L
LambdaTerms [in Rec.Extras.lambda_terms]LambdaTerms.Exports [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm [in Rec.Extras.lambda_terms]
P
PGraded1 [in Rec.Framework.graded]PGraded1.Exports [in Rec.Framework.graded]
PGraded2 [in Rec.Framework.graded]
PGraded2.Exports [in Rec.Framework.graded]
T
TmVl [in Rec.Framework.sysf_const_terms]TmVl [in Rec.Framework.sysf_terms]
TmVl.Exports [in Rec.Framework.sysf_const_terms]
TmVl.Exports [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl [in Rec.Framework.sysf_terms]
TyTerms [in Rec.Framework.sysf_types]
TyTerms.Exports [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty [in Rec.Framework.sysf_types]
Variable Index
B
BoxGraded1.V [in Rec.Framework.graded]BoxGraded2.V [in Rec.Framework.graded]
C
CGraded1.ClassDef.cT [in Rec.Framework.graded]CGraded1.ClassDef.T [in Rec.Framework.graded]
CGraded1.ClassDef.xT [in Rec.Framework.graded]
CGraded2.ClassDef.cT [in Rec.Framework.graded]
CGraded2.ClassDef.T [in Rec.Framework.graded]
CGraded2.ClassDef.xT [in Rec.Framework.graded]
CoFinal.e [in Rec.Base.ARS]
CoFinal.rho [in Rec.Base.ARS]
CoFinal.T [in Rec.Base.ARS]
CoFinal.tri [in Rec.Base.ARS]
Commutation.T [in Rec.Base.ARS]
ComputationN.classical [in Rec.Base.ARS]
ComputationN.e [in Rec.Base.ARS]
ComputationN.norm [in Rec.Base.ARS]
ComputationN.rho [in Rec.Base.ARS]
ComputationN.sound [in Rec.Base.ARS]
ComputationN.T [in Rec.Base.ARS]
ConstGraded1.T [in Rec.Framework.graded]
ConstGraded2.T [in Rec.Framework.graded]
D
Definitions.e [in Rec.Base.ARS]Definitions.T [in Rec.Base.ARS]
G
Graded1.Defs.cT [in Rec.Framework.graded]Graded1.Defs.p [in Rec.Framework.graded]
Graded2.Defs.cT [in Rec.Framework.graded]
Graded2.Defs.p [in Rec.Framework.graded]
I
IGraded1.ClassDef.cT [in Rec.Framework.graded]IGraded1.ClassDef.T [in Rec.Framework.graded]
IGraded1.ClassDef.xT [in Rec.Framework.graded]
IGraded2.ClassDef.cT [in Rec.Framework.graded]
IGraded2.ClassDef.T [in Rec.Framework.graded]
IGraded2.ClassDef.xT [in Rec.Framework.graded]
L
LambdaModel.app [in Rec.Extras.lambda_model]LambdaModel.beta [in Rec.Extras.lambda_model]
LambdaModel.D [in Rec.Extras.lambda_model]
LambdaModel.lam [in Rec.Extras.lambda_model]
LeftCGraded1.F [in Rec.Framework.graded]
LeftCGraded1.n [in Rec.Framework.graded]
LeftGraded1.F [in Rec.Framework.graded]
LeftGraded1.n [in Rec.Framework.graded]
LeftIGraded1.F [in Rec.Framework.graded]
LeftIGraded1.n [in Rec.Framework.graded]
LeftPGraded1.F [in Rec.Framework.graded]
LeftPGraded1.n [in Rec.Framework.graded]
LiftCGrading.F [in Rec.Framework.graded]
LiftGrading.F [in Rec.Framework.graded]
LiftIGrading.F [in Rec.Framework.graded]
LiftPGrading.F [in Rec.Framework.graded]
P
PGraded1.ClassDef.cT [in Rec.Framework.graded]PGraded1.ClassDef.T [in Rec.Framework.graded]
PGraded1.ClassDef.xT [in Rec.Framework.graded]
PGraded2.ClassDef.cT [in Rec.Framework.graded]
PGraded2.ClassDef.T [in Rec.Framework.graded]
PGraded2.ClassDef.xT [in Rec.Framework.graded]
PredCGrading.A [in Rec.Framework.graded]
PredGrading.A [in Rec.Framework.graded]
PredIGrading.A [in Rec.Framework.graded]
PredPGrading.A [in Rec.Framework.graded]
T
Termination.cr [in Rec.Base.ARS]Termination.e [in Rec.Base.ARS]
Termination.T [in Rec.Base.ARS]
TyTerms.Defs.Embedding.var_is_natural [in Rec.Framework.sysf_types]
Library Index
A
ARSaxioms
F
fintypeG
gradedL
lambda_termslambda_model
S
sysf_typessysf_wn
sysf_print
sysf_const_sn
sysf_const_terms
sysf_terms
sysf_typing
Lemma Index
A
accn_inv [in Rec.Base.ARS]ad_cons [in Rec.Examples.sysf_const_sn]
B
beta_expansion [in Rec.Examples.sysf_const_sn]box_igraded2_mixin [in Rec.Framework.graded]
box_cgraded2_mixin [in Rec.Framework.graded]
box_igraded1_mixin [in Rec.Framework.graded]
box_cgraded1_mixin [in Rec.Framework.graded]
C
cofinal_normalizing [in Rec.Base.ARS]com_lift [in Rec.Base.ARS]
com_strip [in Rec.Base.ARS]
confluent_stable [in Rec.Base.ARS]
confluent_cr [in Rec.Base.ARS]
constl_pgraded2_mixin [in Rec.Framework.graded]
constl_igraded2_mixin [in Rec.Framework.graded]
constl_cgraded2_mixin [in Rec.Framework.graded]
constr_pgraded2_mixin [in Rec.Framework.graded]
constr_igraded2_mixin [in Rec.Framework.graded]
constr_cgraded2_mixin [in Rec.Framework.graded]
const_pgraded2_mixin [in Rec.Framework.graded]
const_igraded2_mixin [in Rec.Framework.graded]
const_cgraded2_mixin [in Rec.Framework.graded]
const_pgraded1_mixin [in Rec.Framework.graded]
const_igraded1_mixin [in Rec.Framework.graded]
const_cgraded1_mixin [in Rec.Framework.graded]
context_morphism [in Rec.Examples.sysf_typing]
convES [in Rec.Base.ARS]
convESi [in Rec.Base.ARS]
conv_closure [in Rec.Base.ARS]
conv_hom [in Rec.Base.ARS]
conv_img [in Rec.Base.ARS]
conv_sym [in Rec.Base.ARS]
conv_trans [in Rec.Base.ARS]
conv1 [in Rec.Base.ARS]
conv1i [in Rec.Base.ARS]
cr_method [in Rec.Base.ARS]
cr_conv_normal [in Rec.Base.ARS]
cr_star_normal [in Rec.Base.ARS]
D
diamond_confluent [in Rec.Base.ARS]E
eq_star [in Rec.Base.ARS]evalnP [in Rec.Base.ARS]
evaln_sound [in Rec.Base.ARS]
ev_inst [in Rec.Extras.lambda_model]
ev_lam [in Rec.Extras.lambda_model]
ev_app [in Rec.Extras.lambda_model]
ev_var [in Rec.Extras.lambda_model]
F
fin_pgraded1_mixin [in Rec.Framework.graded]fin_igraded1_mixin [in Rec.Framework.graded]
fin_cgraded1_mixin [in Rec.Framework.graded]
fundamental_theorem [in Rec.Examples.sysf_wn]
I
im_comp [in Rec.Framework.graded]im_id [in Rec.Framework.graded]
im_injective [in Rec.Framework.graded]
im_inj [in Rec.Framework.graded]
im_exists2 [in Rec.Examples.sysf_typing]
im_eq [in Rec.Examples.sysf_typing]
inst_expansion [in Rec.Examples.sysf_const_sn]
iren_eq [in Rec.Base.fintype]
J
join_conv [in Rec.Base.ARS]L
LambdaTerms.eval_ren [in Rec.Extras.lambda_terms]LambdaTerms.ren_id [in Rec.Extras.lambda_terms]
LambdaTerms.ren_inj [in Rec.Extras.lambda_terms]
LambdaTerms.ren_comp [in Rec.Extras.lambda_terms]
LambdaTerms.ren_is_natural [in Rec.Extras.lambda_terms]
LambdaTerms.seval_inst [in Rec.Extras.lambda_terms]
LambdaTerms.seval_ren [in Rec.Extras.lambda_terms]
LambdaTerms.seval_irrelevance [in Rec.Extras.lambda_terms]
LambdaTerms.smodel_is_natural [in Rec.Extras.lambda_terms]
LambdaTerms.th1_tmE [in Rec.Extras.lambda_terms]
LambdaTerms.tm_inst_ren [in Rec.Extras.lambda_terms]
left_pgraded1_mixin [in Rec.Framework.graded]
left_igraded1_mixin [in Rec.Framework.graded]
left_cgraded1_mixin [in Rec.Framework.graded]
L_cl_star [in Rec.Examples.sysf_const_sn]
L_const [in Rec.Examples.sysf_const_sn]
L_var [in Rec.Examples.sysf_const_sn]
L_nc [in Rec.Examples.sysf_const_sn]
L_cl [in Rec.Examples.sysf_const_sn]
L_sn [in Rec.Examples.sysf_const_sn]
L_reducible [in Rec.Examples.sysf_const_sn]
N
nf_accn [in Rec.Base.ARS]normal_star [in Rec.Base.ARS]
P
pi [in Rec.Base.axioms]pred_pgraded1_mixin [in Rec.Framework.graded]
pred_igraded1_mixin [in Rec.Framework.graded]
pred_cgraded1_mixin [in Rec.Framework.graded]
preservation [in Rec.Examples.sysf_typing]
R
reducible_const [in Rec.Examples.sysf_const_sn]reducible_sn [in Rec.Examples.sysf_const_sn]
red_beta [in Rec.Examples.sysf_const_sn]
red_compat [in Rec.Examples.sysf_const_sn]
red_inst [in Rec.Examples.sysf_const_sn]
red_tabs [in Rec.Examples.sysf_const_sn]
red_tapp [in Rec.Examples.sysf_const_sn]
red_abs [in Rec.Examples.sysf_const_sn]
red_app [in Rec.Examples.sysf_const_sn]
rel_preservation [in Rec.Examples.sysf_typing]
rho_id [in Rec.Examples.sysf_const_sn]
S
scons_comp [in Rec.Base.fintype]scons_eta_id [in Rec.Base.fintype]
scons_eta [in Rec.Base.fintype]
shift_up [in Rec.Base.fintype]
shift_typing [in Rec.Examples.sysf_typing]
sn_inst [in Rec.Examples.sysf_const_sn]
sn_tclosed [in Rec.Examples.sysf_const_sn]
sn_closed [in Rec.Examples.sysf_const_sn]
sn_wn [in Rec.Base.ARS]
sn_preimage [in Rec.Base.ARS]
soundness [in Rec.Examples.sysf_const_sn]
starES [in Rec.Base.ARS]
star_interpolation [in Rec.Base.ARS]
star_monotone [in Rec.Base.ARS]
star_closure [in Rec.Base.ARS]
star_hom [in Rec.Base.ARS]
star_img [in Rec.Base.ARS]
star_conv [in Rec.Base.ARS]
star_trans [in Rec.Base.ARS]
star1 [in Rec.Base.ARS]
step_invariant [in Rec.Extras.lambda_model]
step_inst [in Rec.Examples.sysf_const_sn]
step_eBeta [in Rec.Examples.sysf_const_sn]
step_ebeta [in Rec.Examples.sysf_const_sn]
strong_normalisation [in Rec.Examples.sysf_const_sn]
T
th_inj2 [in Rec.Framework.graded]th_id2 [in Rec.Framework.graded]
th_comp2 [in Rec.Framework.graded]
th_inj1 [in Rec.Framework.graded]
th_id1 [in Rec.Framework.graded]
th_comp1 [in Rec.Framework.graded]
th1_compR [in Rec.Framework.graded]
th1_compX [in Rec.Framework.graded]
th1_idX [in Rec.Framework.graded]
th1_leftE [in Rec.Framework.graded]
th1_predE [in Rec.Framework.graded]
th1_boxE [in Rec.Framework.graded]
th1_constE [in Rec.Framework.graded]
th1_finE [in Rec.Framework.graded]
th2_compR [in Rec.Framework.graded]
th2_compX [in Rec.Framework.graded]
th2_idX [in Rec.Framework.graded]
th2_boxE [in Rec.Framework.graded]
th2_constE [in Rec.Framework.graded]
th2_constrE [in Rec.Framework.graded]
th2_constlE [in Rec.Framework.graded]
TmVl.eval_inst [in Rec.Framework.sysf_const_terms]
TmVl.eval_ren [in Rec.Framework.sysf_const_terms]
TmVl.eval_tm_inst [in Rec.Framework.sysf_terms]
TmVl.eval_vl_inst [in Rec.Framework.sysf_terms]
TmVl.eval_vl_tm_inst [in Rec.Framework.sysf_terms]
TmVl.eval_tm_ren [in Rec.Framework.sysf_terms]
TmVl.eval_vl_ren [in Rec.Framework.sysf_terms]
TmVl.eval_vl_tm_ren [in Rec.Framework.sysf_terms]
TmVl.inst_comp [in Rec.Framework.sysf_const_terms]
TmVl.inst_tm_comp [in Rec.Framework.sysf_terms]
TmVl.inst_vl_comp [in Rec.Framework.sysf_terms]
TmVl.lift_embed [in Rec.Framework.sysf_const_terms]
TmVl.lift_tm_embed [in Rec.Framework.sysf_terms]
TmVl.lift_vl_embed [in Rec.Framework.sysf_terms]
TmVl.naturality [in Rec.Framework.sysf_const_terms]
TmVl.naturality_tm [in Rec.Framework.sysf_terms]
TmVl.naturality_vl [in Rec.Framework.sysf_terms]
TmVl.ren_tm_inj [in Rec.Framework.sysf_const_terms]
TmVl.ren_comp [in Rec.Framework.sysf_const_terms]
TmVl.ren_tm_id [in Rec.Framework.sysf_const_terms]
TmVl.ren_is_natural [in Rec.Framework.sysf_const_terms]
TmVl.ren_tm_inj [in Rec.Framework.sysf_terms]
TmVl.ren_vl_inj [in Rec.Framework.sysf_terms]
TmVl.ren_vl_tm_inj [in Rec.Framework.sysf_terms]
TmVl.ren_tm_comp [in Rec.Framework.sysf_terms]
TmVl.ren_vl_comp [in Rec.Framework.sysf_terms]
TmVl.ren_tm_id [in Rec.Framework.sysf_terms]
TmVl.ren_vl_id [in Rec.Framework.sysf_terms]
TmVl.ren_vl_tm_id [in Rec.Framework.sysf_terms]
TmVl.ren_is_natural [in Rec.Framework.sysf_terms]
TmVl.th2_tmE [in Rec.Framework.sysf_const_terms]
TmVl.th2_tmE [in Rec.Framework.sysf_terms]
TmVl.th2_vlE [in Rec.Framework.sysf_terms]
TmVl.tm_inst_ren [in Rec.Framework.sysf_const_terms]
TmVl.tm_inst_ren [in Rec.Framework.sysf_terms]
TmVl.vl_inst_ren [in Rec.Framework.sysf_terms]
tm_inst_compR [in Rec.Extras.lambda_terms]
tm_inst_compX [in Rec.Extras.lambda_terms]
tm_inst_idR [in Rec.Extras.lambda_terms]
tm_inst_idX [in Rec.Extras.lambda_terms]
tm_id_instX [in Rec.Extras.lambda_terms]
tm_inst_renR [in Rec.Extras.lambda_terms]
tm_inst_renX [in Rec.Extras.lambda_terms]
tm_ren_instR [in Rec.Extras.lambda_terms]
tm_ren_instX [in Rec.Extras.lambda_terms]
tm_ren_compR [in Rec.Extras.lambda_terms]
tm_ren_compX [in Rec.Extras.lambda_terms]
tm_ren_idX [in Rec.Extras.lambda_terms]
tm_inst_compR [in Rec.Framework.sysf_const_terms]
tm_inst_compX [in Rec.Framework.sysf_const_terms]
tm_inst_idR [in Rec.Framework.sysf_const_terms]
tm_inst_idX [in Rec.Framework.sysf_const_terms]
tm_id_instX [in Rec.Framework.sysf_const_terms]
tm_inst_renR [in Rec.Framework.sysf_const_terms]
tm_inst_renX [in Rec.Framework.sysf_const_terms]
tm_ren_instR [in Rec.Framework.sysf_const_terms]
tm_ren_instX [in Rec.Framework.sysf_const_terms]
tm_ren_compR [in Rec.Framework.sysf_const_terms]
tm_ren_compX [in Rec.Framework.sysf_const_terms]
tm_ren_idX [in Rec.Framework.sysf_const_terms]
tm_inst_compR [in Rec.Framework.sysf_terms]
tm_inst_compX [in Rec.Framework.sysf_terms]
tm_inst_idX [in Rec.Framework.sysf_terms]
tm_inst_renR [in Rec.Framework.sysf_terms]
tm_inst_renX [in Rec.Framework.sysf_terms]
tm_ren_instR [in Rec.Framework.sysf_terms]
tm_ren_instX [in Rec.Framework.sysf_terms]
tm_ren_compR [in Rec.Framework.sysf_terms]
tm_ren_compX [in Rec.Framework.sysf_terms]
tm_ren_idX [in Rec.Framework.sysf_terms]
tm_rel_mono [in Rec.Examples.sysf_typing]
tm_frel_mono [in Rec.Examples.sysf_typing]
triangle_cofinal [in Rec.Base.ARS]
triangle_monotone [in Rec.Base.ARS]
triangle_diamond [in Rec.Base.ARS]
tv_monotone [in Rec.Examples.sysf_typing]
type_of_is_natural [in Rec.Examples.sysf_typing]
type_of_App [in Rec.Examples.sysf_typing]
type_of_app [in Rec.Examples.sysf_typing]
type_of_tvl [in Rec.Examples.sysf_typing]
type_of_Lam [in Rec.Examples.sysf_typing]
type_of_lam [in Rec.Examples.sysf_typing]
type_of_var [in Rec.Examples.sysf_typing]
type_E [in Rec.Examples.sysf_const_sn]
TyTerms.eval_inst [in Rec.Framework.sysf_types]
TyTerms.eval_ren [in Rec.Framework.sysf_types]
TyTerms.inst_id [in Rec.Framework.sysf_types]
TyTerms.lift_embed [in Rec.Framework.sysf_types]
TyTerms.lift_embed' [in Rec.Framework.sysf_types]
TyTerms.naturality [in Rec.Framework.sysf_types]
TyTerms.ren_is_inst [in Rec.Framework.sysf_types]
TyTerms.ren_is_natural [in Rec.Framework.sysf_types]
TyTerms.ren_id [in Rec.Framework.sysf_types]
TyTerms.ren_inj [in Rec.Framework.sysf_types]
TyTerms.ren_comp [in Rec.Framework.sysf_types]
TyTerms.seval_inst [in Rec.Framework.sysf_types]
TyTerms.seval_ren [in Rec.Framework.sysf_types]
TyTerms.seval_irrelevance [in Rec.Framework.sysf_types]
TyTerms.smodel_is_natural [in Rec.Framework.sysf_types]
TyTerms.th1_tyE [in Rec.Framework.sysf_types]
TyTerms.ty_inst_ren [in Rec.Framework.sysf_types]
ty_inst_compR [in Rec.Framework.sysf_types]
ty_inst_compX [in Rec.Framework.sysf_types]
ty_inst_idR [in Rec.Framework.sysf_types]
ty_inst_idX [in Rec.Framework.sysf_types]
ty_id_instX [in Rec.Framework.sysf_types]
ty_inst_renR [in Rec.Framework.sysf_types]
ty_inst_renX [in Rec.Framework.sysf_types]
ty_ren_instR [in Rec.Framework.sysf_types]
ty_ren_instX [in Rec.Framework.sysf_types]
ty_ren_compR [in Rec.Framework.sysf_types]
ty_ren_compX [in Rec.Framework.sysf_types]
ty_ren_idX [in Rec.Framework.sysf_types]
V
vl_inst_compR [in Rec.Framework.sysf_terms]vl_inst_compX [in Rec.Framework.sysf_terms]
vl_inst_idR [in Rec.Framework.sysf_terms]
vl_inst_idX [in Rec.Framework.sysf_terms]
vl_id_instX [in Rec.Framework.sysf_terms]
vl_inst_renR [in Rec.Framework.sysf_terms]
vl_inst_renX [in Rec.Framework.sysf_terms]
vl_ren_instR [in Rec.Framework.sysf_terms]
vl_ren_instX [in Rec.Framework.sysf_terms]
vl_ren_compR [in Rec.Framework.sysf_terms]
vl_ren_compX [in Rec.Framework.sysf_terms]
vl_ren_idX [in Rec.Framework.sysf_terms]
vl_tvar_shift [in Rec.Examples.sysf_typing]
W
weak_normalisation [in Rec.Examples.sysf_wn]wn_accn [in Rec.Base.ARS]
Constructor Index
A
accnH [in Rec.Base.ARS]accnL [in Rec.Base.ARS]
C
CGraded1.Class [in Rec.Framework.graded]CGraded1.Pack [in Rec.Framework.graded]
CGraded2.Class [in Rec.Framework.graded]
CGraded2.Pack [in Rec.Framework.graded]
convR [in Rec.Base.ARS]
convSE [in Rec.Base.ARS]
convSEi [in Rec.Base.ARS]
E
eval_App [in Rec.Examples.sysf_wn]eval_app [in Rec.Examples.sysf_wn]
eval_val [in Rec.Examples.sysf_wn]
G
Graded1.Pack [in Rec.Framework.graded]Graded2.Pack [in Rec.Framework.graded]
I
IGraded1.Class [in Rec.Framework.graded]IGraded1.Pack [in Rec.Framework.graded]
IGraded2.Class [in Rec.Framework.graded]
IGraded2.Pack [in Rec.Framework.graded]
IRen [in Rec.Base.fintype]
L
LambdaTerms.app [in Rec.Extras.lambda_terms]LambdaTerms.IsNatural [in Rec.Extras.lambda_terms]
LambdaTerms.lam [in Rec.Extras.lambda_terms]
LambdaTerms.Model [in Rec.Extras.lambda_terms]
LambdaTerms.SModel [in Rec.Extras.lambda_terms]
LambdaTerms.Traversal [in Rec.Extras.lambda_terms]
LambdaTerms.var [in Rec.Extras.lambda_terms]
N
nall [in Rec.Extras.sysf_print]narr [in Rec.Extras.sysf_print]
nvar [in Rec.Extras.sysf_print]
P
PGraded1.Class [in Rec.Framework.graded]PGraded1.Pack [in Rec.Framework.graded]
PGraded2.Class [in Rec.Framework.graded]
PGraded2.Pack [in Rec.Framework.graded]
S
SNI [in Rec.Base.ARS]starR [in Rec.Base.ARS]
starSE [in Rec.Base.ARS]
step_lam [in Rec.Extras.lambda_model]
step_appR [in Rec.Extras.lambda_model]
step_appL [in Rec.Extras.lambda_model]
step_beta [in Rec.Extras.lambda_model]
step_tabs [in Rec.Examples.sysf_const_sn]
step_tapp [in Rec.Examples.sysf_const_sn]
step_abs [in Rec.Examples.sysf_const_sn]
step_appR [in Rec.Examples.sysf_const_sn]
step_appL [in Rec.Examples.sysf_const_sn]
step_Beta [in Rec.Examples.sysf_const_sn]
step_beta [in Rec.Examples.sysf_const_sn]
T
TmVl.App [in Rec.Framework.sysf_const_terms]TmVl.app [in Rec.Framework.sysf_const_terms]
TmVl.App [in Rec.Framework.sysf_terms]
TmVl.app [in Rec.Framework.sysf_terms]
TmVl.const [in Rec.Framework.sysf_const_terms]
TmVl.IsNatural [in Rec.Framework.sysf_const_terms]
TmVl.IsNatural [in Rec.Framework.sysf_terms]
TmVl.Lam [in Rec.Framework.sysf_const_terms]
TmVl.lam [in Rec.Framework.sysf_const_terms]
TmVl.Lam [in Rec.Framework.sysf_terms]
TmVl.lam [in Rec.Framework.sysf_terms]
TmVl.Model [in Rec.Framework.sysf_const_terms]
TmVl.Model [in Rec.Framework.sysf_terms]
TmVl.Traversal [in Rec.Framework.sysf_const_terms]
TmVl.Traversal [in Rec.Framework.sysf_terms]
TmVl.tvl [in Rec.Framework.sysf_terms]
TmVl.var [in Rec.Framework.sysf_const_terms]
TmVl.var [in Rec.Framework.sysf_terms]
tm_ty_App [in Rec.Examples.sysf_wn]
tm_ty_app [in Rec.Examples.sysf_wn]
tm_ty_vl [in Rec.Examples.sysf_wn]
TyTerms.all [in Rec.Framework.sysf_types]
TyTerms.arr [in Rec.Framework.sysf_types]
TyTerms.IsNatural [in Rec.Framework.sysf_types]
TyTerms.Model [in Rec.Framework.sysf_types]
TyTerms.SModel [in Rec.Framework.sysf_types]
TyTerms.Traversal [in Rec.Framework.sysf_types]
TyTerms.var [in Rec.Framework.sysf_types]
ty_tapp [in Rec.Examples.sysf_const_sn]
ty_tabs [in Rec.Examples.sysf_const_sn]
ty_app [in Rec.Examples.sysf_const_sn]
ty_abs [in Rec.Examples.sysf_const_sn]
ty_var [in Rec.Examples.sysf_const_sn]
V
vl_ty_Lam [in Rec.Examples.sysf_wn]vl_ty_lam [in Rec.Examples.sysf_wn]
vl_ty_var [in Rec.Examples.sysf_wn]
Axiom Index
P
pext [in Rec.Base.axioms]Inductive Index
A
accn [in Rec.Base.ARS]C
conv [in Rec.Base.ARS]E
eval [in Rec.Examples.sysf_wn]H
has_type [in Rec.Examples.sysf_const_sn]L
LambdaTerms.tm [in Rec.Extras.lambda_terms]N
nty [in Rec.Extras.sysf_print]S
sn [in Rec.Base.ARS]star [in Rec.Base.ARS]
step [in Rec.Extras.lambda_model]
step [in Rec.Examples.sysf_const_sn]
T
TmVl.tm [in Rec.Framework.sysf_const_terms]TmVl.tm [in Rec.Framework.sysf_terms]
TmVl.vl [in Rec.Framework.sysf_terms]
tm_ty [in Rec.Examples.sysf_wn]
TyTerms.ty [in Rec.Framework.sysf_types]
V
vl_ty [in Rec.Examples.sysf_wn]Projection Index
C
CGraded1.base [in Rec.Framework.graded]CGraded1.mixin [in Rec.Framework.graded]
CGraded1.sort [in Rec.Framework.graded]
CGraded2.base [in Rec.Framework.graded]
CGraded2.mixin [in Rec.Framework.graded]
CGraded2.sort [in Rec.Framework.graded]
G
Graded1.sort [in Rec.Framework.graded]Graded2.sort [in Rec.Framework.graded]
I
IGraded1.base [in Rec.Framework.graded]IGraded1.mixin [in Rec.Framework.graded]
IGraded1.sort [in Rec.Framework.graded]
IGraded2.base [in Rec.Framework.graded]
IGraded2.mixin [in Rec.Framework.graded]
IGraded2.sort [in Rec.Framework.graded]
iren_inj [in Rec.Base.fintype]
iren_fun [in Rec.Base.fintype]
L
LambdaTerms.base [in Rec.Extras.lambda_terms]LambdaTerms.napp [in Rec.Extras.lambda_terms]
LambdaTerms.nlam [in Rec.Extras.lambda_terms]
LambdaTerms.nvar [in Rec.Extras.lambda_terms]
LambdaTerms.sapp [in Rec.Extras.lambda_terms]
LambdaTerms.slam [in Rec.Extras.lambda_terms]
LambdaTerms.svar [in Rec.Extras.lambda_terms]
LambdaTerms.tapp [in Rec.Extras.lambda_terms]
LambdaTerms.tlam [in Rec.Extras.lambda_terms]
LambdaTerms.tvar [in Rec.Extras.lambda_terms]
P
PGraded1.base [in Rec.Framework.graded]PGraded1.mixin [in Rec.Framework.graded]
PGraded1.sort [in Rec.Framework.graded]
PGraded2.base [in Rec.Framework.graded]
PGraded2.mixin [in Rec.Framework.graded]
PGraded2.sort [in Rec.Framework.graded]
p_nc [in Rec.Examples.sysf_const_sn]
p_cl [in Rec.Examples.sysf_const_sn]
p_sn [in Rec.Examples.sysf_const_sn]
T
TmVl.base [in Rec.Framework.sysf_const_terms]TmVl.base [in Rec.Framework.sysf_terms]
TmVl.nApp [in Rec.Framework.sysf_const_terms]
TmVl.napp [in Rec.Framework.sysf_const_terms]
TmVl.nApp [in Rec.Framework.sysf_terms]
TmVl.napp [in Rec.Framework.sysf_terms]
TmVl.nconst [in Rec.Framework.sysf_const_terms]
TmVl.nLam [in Rec.Framework.sysf_const_terms]
TmVl.nlam [in Rec.Framework.sysf_const_terms]
TmVl.nLam [in Rec.Framework.sysf_terms]
TmVl.nlam [in Rec.Framework.sysf_terms]
TmVl.ntvl [in Rec.Framework.sysf_terms]
TmVl.nvar [in Rec.Framework.sysf_const_terms]
TmVl.nvar [in Rec.Framework.sysf_terms]
TmVl.tApp [in Rec.Framework.sysf_const_terms]
TmVl.tapp [in Rec.Framework.sysf_const_terms]
TmVl.tApp [in Rec.Framework.sysf_terms]
TmVl.tapp [in Rec.Framework.sysf_terms]
TmVl.tconst [in Rec.Framework.sysf_const_terms]
TmVl.tLam [in Rec.Framework.sysf_const_terms]
TmVl.tlam [in Rec.Framework.sysf_const_terms]
TmVl.tLam [in Rec.Framework.sysf_terms]
TmVl.tlam [in Rec.Framework.sysf_terms]
TmVl.ttvl [in Rec.Framework.sysf_terms]
TmVl.tvar [in Rec.Framework.sysf_const_terms]
TmVl.tvar [in Rec.Framework.sysf_terms]
TyTerms.base [in Rec.Framework.sysf_types]
TyTerms.nall [in Rec.Framework.sysf_types]
TyTerms.narr [in Rec.Framework.sysf_types]
TyTerms.nvar [in Rec.Framework.sysf_types]
TyTerms.sall [in Rec.Framework.sysf_types]
TyTerms.sarr [in Rec.Framework.sysf_types]
TyTerms.svar [in Rec.Framework.sysf_types]
TyTerms.tall [in Rec.Framework.sysf_types]
TyTerms.tarr [in Rec.Framework.sysf_types]
TyTerms.tvar [in Rec.Framework.sysf_types]
Section Index
B
BoxGraded1 [in Rec.Framework.graded]BoxGraded2 [in Rec.Framework.graded]
C
CGraded1.ClassDef [in Rec.Framework.graded]CGraded2.ClassDef [in Rec.Framework.graded]
CoFinal [in Rec.Base.ARS]
Commutation [in Rec.Base.ARS]
ComputationN [in Rec.Base.ARS]
ConstGraded1 [in Rec.Framework.graded]
ConstGraded2 [in Rec.Framework.graded]
D
Definitions [in Rec.Base.ARS]G
Graded1.Defs [in Rec.Framework.graded]Graded2.Defs [in Rec.Framework.graded]
I
IGraded1.ClassDef [in Rec.Framework.graded]IGraded2.ClassDef [in Rec.Framework.graded]
L
LambdaModel [in Rec.Extras.lambda_model]LambdaTerms.Defs [in Rec.Extras.lambda_terms]
LambdaTerms.Defs.EvalRen [in Rec.Extras.lambda_terms]
LeftCGraded1 [in Rec.Framework.graded]
LeftGraded1 [in Rec.Framework.graded]
LeftIGraded1 [in Rec.Framework.graded]
LeftPGraded1 [in Rec.Framework.graded]
LiftCGrading [in Rec.Framework.graded]
LiftGrading [in Rec.Framework.graded]
LiftIGrading [in Rec.Framework.graded]
LiftPGrading [in Rec.Framework.graded]
P
PGraded1.ClassDef [in Rec.Framework.graded]PGraded2.ClassDef [in Rec.Framework.graded]
PredCGrading [in Rec.Framework.graded]
PredGrading [in Rec.Framework.graded]
PredIGrading [in Rec.Framework.graded]
PredPGrading [in Rec.Framework.graded]
T
Termination [in Rec.Base.ARS]TmVl.Defs [in Rec.Framework.sysf_const_terms]
TmVl.Defs [in Rec.Framework.sysf_terms]
TmVl.Defs.EvalRen [in Rec.Framework.sysf_const_terms]
TmVl.Defs.EvalRen [in Rec.Framework.sysf_terms]
TrivialGraded1 [in Rec.Framework.graded]
TyTerms.Defs [in Rec.Framework.sysf_types]
TyTerms.Defs.Embedding [in Rec.Framework.sysf_types]
TyTerms.Defs.EvalRen [in Rec.Framework.sysf_types]
Abbreviation Index
C
CGraded1.Exports.CGraded1 [in Rec.Framework.graded]CGraded1.Exports.cgraded1 [in Rec.Framework.graded]
CGraded1.xclass [in Rec.Framework.graded]
CGraded2.Exports.CGraded2 [in Rec.Framework.graded]
CGraded2.Exports.cgraded2 [in Rec.Framework.graded]
CGraded2.xclass [in Rec.Framework.graded]
cvl [in Rec.Examples.sysf_wn]
E
E [in Rec.Examples.sysf_wn]E [in Rec.Examples.sysf_const_sn]
G
Graded1.class_of [in Rec.Framework.graded]Graded1.Exports.Graded1 [in Rec.Framework.graded]
Graded1.Exports.graded1 [in Rec.Framework.graded]
Graded2.class_of [in Rec.Framework.graded]
Graded2.Exports.Graded2 [in Rec.Framework.graded]
Graded2.Exports.graded2 [in Rec.Framework.graded]
I
IGraded1.Exports.IGraded1 [in Rec.Framework.graded]IGraded1.Exports.igraded1 [in Rec.Framework.graded]
IGraded1.xclass [in Rec.Framework.graded]
IGraded2.Exports.IGraded2 [in Rec.Framework.graded]
IGraded2.Exports.igraded2 [in Rec.Framework.graded]
IGraded2.xclass [in Rec.Framework.graded]
L
L [in Rec.Examples.sysf_wn]LambdaTerms.Exports.tm [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.app [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.embed [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval_inst [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.eval_ren [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_comp [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_id [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_ren [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.inst_traversal [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.IsNatural [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.is_natural [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.lam [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.lift [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.Model [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.model [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.napp [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.naturality [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.nlam [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.nvar [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_inst [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_inj [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_comp [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_id [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.ren_traversal [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.sapp [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_inst [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_ren [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.seval_irrelevance [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.slam [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.SModel [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.smodel [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.svar [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tapp [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tlam [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.Traversal [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.traversal [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.tvar [in Rec.Extras.lambda_terms]
LambdaTerms.Exports.Tm.var [in Rec.Extras.lambda_terms]
LambdaTerms.inst [in Rec.Extras.lambda_terms]
LambdaTerms.inst_traversal [in Rec.Extras.lambda_terms]
LambdaTerms.tm_ren [in Rec.Extras.lambda_terms]
P
PGraded1.Exports.PGraded1 [in Rec.Framework.graded]PGraded1.Exports.pgraded1 [in Rec.Framework.graded]
PGraded1.xclass [in Rec.Framework.graded]
PGraded2.Exports.PGraded2 [in Rec.Framework.graded]
PGraded2.Exports.pgraded2 [in Rec.Framework.graded]
PGraded2.xclass [in Rec.Framework.graded]
S
sn [in Rec.Examples.sysf_const_sn]T
TmVl.Exports.FCBV.inst_traversal [in Rec.Framework.sysf_terms]TmVl.Exports.FCBV.IsNatural [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.is_natural [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.lift [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.model [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nApp [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.napp [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nLam [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nlam [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ntvl [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.nvar [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ren_traversal [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tApp [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tapp [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tLam [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tlam [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.Traversal [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.traversal [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.ttvl [in Rec.Framework.sysf_terms]
TmVl.Exports.FCBV.tvar [in Rec.Framework.sysf_terms]
TmVl.Exports.tm [in Rec.Framework.sysf_const_terms]
TmVl.Exports.tm [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.App [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.app [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.App [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.app [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.const [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.embed [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.embed [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval_inst [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval_ren [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.eval_inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.eval_ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_comp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_id [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_ren [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_traversal [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.inst_comp [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_id [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.inst_ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.IsNatural [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.is_natural [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Lam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.lam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.lift [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Model [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.model [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nApp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.napp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.naturality [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.naturality [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.nconst [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nLam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nlam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.nvar [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_inst [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_inj [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_comp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_id [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_traversal [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.ren_inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_inj [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_comp [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.ren_id [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.tApp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tapp [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tconst [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tLam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tlam [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.Traversal [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.traversal [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tvar [in Rec.Framework.sysf_const_terms]
TmVl.Exports.Tm.tvl [in Rec.Framework.sysf_terms]
TmVl.Exports.Tm.var [in Rec.Framework.sysf_const_terms]
TmVl.Exports.vl [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.embed [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval_inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.eval_ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_comp [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_id [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.inst_ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.Lam [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.lam [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.naturality [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_inst [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_inj [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_comp [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.ren_id [in Rec.Framework.sysf_terms]
TmVl.Exports.Vl.var [in Rec.Framework.sysf_terms]
TmVl.inst_tm [in Rec.Framework.sysf_const_terms]
TmVl.inst_traversal [in Rec.Framework.sysf_const_terms]
TmVl.inst_tm [in Rec.Framework.sysf_terms]
TmVl.inst_vl [in Rec.Framework.sysf_terms]
TmVl.inst_traversal [in Rec.Framework.sysf_terms]
TmVl.tm_ren [in Rec.Framework.sysf_const_terms]
TmVl.tm_ren [in Rec.Framework.sysf_terms]
TmVl.vl_ren [in Rec.Framework.sysf_terms]
tm_rel [in Rec.Examples.sysf_typing]
tm_frel [in Rec.Examples.sysf_typing]
tm_type [in Rec.Examples.sysf_typing]
TyTerms.Exports.ty [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.all [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.arr [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.embed [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval_inst [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.eval_ren [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_comp [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_id [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_ren [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.inst_traversal [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.IsNatural [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.is_natural [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.lift [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.Model [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.model [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.nall [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.narr [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.naturality [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.nvar [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_inst [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_inj [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_comp [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_id [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.ren_traversal [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.sall [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.sarr [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_inst [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_ren [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.seval_irrelevance [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.SModel [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.smodel [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.svar [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tall [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tarr [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.Traversal [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.traversal [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.tvar [in Rec.Framework.sysf_types]
TyTerms.Exports.Ty.var [in Rec.Framework.sysf_types]
TyTerms.inst [in Rec.Framework.sysf_types]
TyTerms.inst_traversal [in Rec.Framework.sysf_types]
TyTerms.ty_ren [in Rec.Framework.sysf_types]
V
V [in Rec.Examples.sysf_wn]vl_rel [in Rec.Examples.sysf_typing]
vl_frel [in Rec.Examples.sysf_typing]
vl_type [in Rec.Examples.sysf_typing]
Definition Index
A
accn_ind' [in Rec.Base.ARS]admissible [in Rec.Examples.sysf_const_sn]
B
bound [in Rec.Base.fintype]box [in Rec.Framework.graded]
box_igraded2 [in Rec.Framework.graded]
box_cgraded2 [in Rec.Framework.graded]
box_graded2 [in Rec.Framework.graded]
box_igraded1 [in Rec.Framework.graded]
box_cgraded1 [in Rec.Framework.graded]
box_graded1 [in Rec.Framework.graded]
box2 [in Rec.Framework.graded]
C
cand [in Rec.Examples.sysf_const_sn]CGraded1.class [in Rec.Framework.graded]
CGraded1.clone [in Rec.Framework.graded]
CGraded1.graded1 [in Rec.Framework.graded]
CGraded1.mixin_of [in Rec.Framework.graded]
CGraded1.pack [in Rec.Framework.graded]
CGraded2.class [in Rec.Framework.graded]
CGraded2.clone [in Rec.Framework.graded]
CGraded2.graded2 [in Rec.Framework.graded]
CGraded2.mixin_of [in Rec.Framework.graded]
CGraded2.pack [in Rec.Framework.graded]
cofinal [in Rec.Base.ARS]
com [in Rec.Base.ARS]
confluent [in Rec.Base.ARS]
constl [in Rec.Framework.graded]
constl_pgraded2 [in Rec.Framework.graded]
constl_igraded2 [in Rec.Framework.graded]
constl_graded2 [in Rec.Framework.graded]
constl_th2 [in Rec.Framework.graded]
constr [in Rec.Framework.graded]
constr_pgraded2 [in Rec.Framework.graded]
constr_igraded2 [in Rec.Framework.graded]
constr_graded2 [in Rec.Framework.graded]
constr_th2 [in Rec.Framework.graded]
const_pgraded2 [in Rec.Framework.graded]
const_igraded2 [in Rec.Framework.graded]
const_cgraded2 [in Rec.Framework.graded]
const_graded2 [in Rec.Framework.graded]
const_pgraded1 [in Rec.Framework.graded]
const_igraded1 [in Rec.Framework.graded]
const_cgraded1 [in Rec.Framework.graded]
const_graded1 [in Rec.Framework.graded]
const1 [in Rec.Framework.graded]
const2 [in Rec.Framework.graded]
contl_cgraded2 [in Rec.Framework.graded]
contr_cgraded2 [in Rec.Framework.graded]
CR [in Rec.Base.ARS]
ctx [in Rec.Examples.sysf_const_sn]
cvls [in Rec.Examples.sysf_wn]
D
diamond [in Rec.Base.ARS]E
evaln [in Rec.Base.ARS]F
fin [in Rec.Base.fintype]fin_pgraded1 [in Rec.Framework.graded]
fin_igraded1 [in Rec.Framework.graded]
fin_cgraded1 [in Rec.Framework.graded]
fin_graded1 [in Rec.Framework.graded]
fin_th1 [in Rec.Framework.graded]
fin2 [in Rec.Framework.graded]
G
Graded1.class [in Rec.Framework.graded]Graded1.clone [in Rec.Framework.graded]
Graded1.mixin_of [in Rec.Framework.graded]
Graded1.pack [in Rec.Framework.graded]
Graded2.class [in Rec.Framework.graded]
Graded2.clone [in Rec.Framework.graded]
Graded2.mixin_of [in Rec.Framework.graded]
Graded2.pack [in Rec.Framework.graded]
I
id [in Rec.Extras.sysf_print]idren [in Rec.Base.fintype]
IGraded1.class [in Rec.Framework.graded]
IGraded1.clone [in Rec.Framework.graded]
IGraded1.graded1 [in Rec.Framework.graded]
IGraded1.mixin_of [in Rec.Framework.graded]
IGraded1.pack [in Rec.Framework.graded]
IGraded2.class [in Rec.Framework.graded]
IGraded2.clone [in Rec.Framework.graded]
IGraded2.graded2 [in Rec.Framework.graded]
IGraded2.mixin_of [in Rec.Framework.graded]
IGraded2.pack [in Rec.Framework.graded]
im [in Rec.Framework.graded]
J
joinable [in Rec.Base.ARS]L
LambdaTerms.eval [in Rec.Extras.lambda_terms]LambdaTerms.eval_inst [in Rec.Extras.lambda_terms]
LambdaTerms.inst_comp [in Rec.Extras.lambda_terms]
LambdaTerms.inst_id [in Rec.Extras.lambda_terms]
LambdaTerms.lift [in Rec.Extras.lambda_terms]
LambdaTerms.lift_smodel [in Rec.Extras.lambda_terms]
LambdaTerms.lift_embed [in Rec.Extras.lambda_terms]
LambdaTerms.lift_model [in Rec.Extras.lambda_terms]
LambdaTerms.lift_is_natural [in Rec.Extras.lambda_terms]
LambdaTerms.model_is_natural [in Rec.Extras.lambda_terms]
LambdaTerms.model_of [in Rec.Extras.lambda_terms]
LambdaTerms.naturality [in Rec.Extras.lambda_terms]
LambdaTerms.ren_model [in Rec.Extras.lambda_terms]
LambdaTerms.ren_traversal [in Rec.Extras.lambda_terms]
LambdaTerms.seval [in Rec.Extras.lambda_terms]
LambdaTerms.smodel_to_model [in Rec.Extras.lambda_terms]
LambdaTerms.smodel_to_traversal [in Rec.Extras.lambda_terms]
LambdaTerms.tm_ren_inst [in Rec.Extras.lambda_terms]
LambdaTerms.tm_pgraded1 [in Rec.Extras.lambda_terms]
LambdaTerms.tm_igraded1 [in Rec.Extras.lambda_terms]
LambdaTerms.tm_cgraded1 [in Rec.Extras.lambda_terms]
LambdaTerms.tm_graded1 [in Rec.Extras.lambda_terms]
lambda_smodel [in Rec.Extras.lambda_model]
left_pgraded1 [in Rec.Framework.graded]
left_igraded1 [in Rec.Framework.graded]
left_cgraded1 [in Rec.Framework.graded]
left_graded1 [in Rec.Framework.graded]
left_th1 [in Rec.Framework.graded]
left1 [in Rec.Framework.graded]
N
neutral [in Rec.Examples.sysf_const_sn]nf [in Rec.Base.ARS]
normal [in Rec.Base.ARS]
normalizing [in Rec.Base.ARS]
null [in Rec.Base.fintype]
P
PGraded1.class [in Rec.Framework.graded]PGraded1.clone [in Rec.Framework.graded]
PGraded1.graded1 [in Rec.Framework.graded]
PGraded1.mixin_of [in Rec.Framework.graded]
PGraded1.pack [in Rec.Framework.graded]
PGraded2.class [in Rec.Framework.graded]
PGraded2.clone [in Rec.Framework.graded]
PGraded2.graded2 [in Rec.Framework.graded]
PGraded2.mixin_of [in Rec.Framework.graded]
PGraded2.pack [in Rec.Framework.graded]
Pred [in Rec.Base.ARS]
pred_pgraded1 [in Rec.Framework.graded]
pred_igraded1 [in Rec.Framework.graded]
pred_cgraded1 [in Rec.Framework.graded]
pred_graded1 [in Rec.Framework.graded]
pred_th1 [in Rec.Framework.graded]
pred1 [in Rec.Framework.graded]
print [in Rec.Extras.sysf_print]
printer [in Rec.Extras.sysf_print]
print_smodel [in Rec.Extras.sysf_print]
R
rcomp [in Rec.Base.fintype]red [in Rec.Examples.sysf_const_sn]
reducible [in Rec.Base.ARS]
Rel [in Rec.Base.ARS]
ren [in Rec.Base.fintype]
S
S [in Rec.Examples.sysf_const_sn]scons [in Rec.Base.fintype]
shift [in Rec.Base.fintype]
sred [in Rec.Examples.sysf_const_sn]
T
test [in Rec.Extras.sysf_print]th1 [in Rec.Framework.graded]
th2 [in Rec.Framework.graded]
TmVl.eval [in Rec.Framework.sysf_const_terms]
TmVl.eval_tm [in Rec.Framework.sysf_terms]
TmVl.eval_vl [in Rec.Framework.sysf_terms]
TmVl.inst_tm_id [in Rec.Framework.sysf_const_terms]
TmVl.inst_tm_id [in Rec.Framework.sysf_terms]
TmVl.inst_vl_id [in Rec.Framework.sysf_terms]
TmVl.lift [in Rec.Framework.sysf_const_terms]
TmVl.lift [in Rec.Framework.sysf_terms]
TmVl.lift_model [in Rec.Framework.sysf_const_terms]
TmVl.lift_is_natural [in Rec.Framework.sysf_const_terms]
TmVl.lift_vl_tm_embed [in Rec.Framework.sysf_terms]
TmVl.lift_model [in Rec.Framework.sysf_terms]
TmVl.lift_is_natural [in Rec.Framework.sysf_terms]
TmVl.model_is_natural [in Rec.Framework.sysf_const_terms]
TmVl.model_is_natural [in Rec.Framework.sysf_terms]
TmVl.model_of [in Rec.Framework.sysf_terms]
TmVl.naturality_vl_tm [in Rec.Framework.sysf_terms]
TmVl.ren_model [in Rec.Framework.sysf_const_terms]
TmVl.ren_traversal [in Rec.Framework.sysf_const_terms]
TmVl.ren_model [in Rec.Framework.sysf_terms]
TmVl.ren_traversal [in Rec.Framework.sysf_terms]
TmVl.tm_ren_inst [in Rec.Framework.sysf_const_terms]
TmVl.tm_pgraded2 [in Rec.Framework.sysf_const_terms]
TmVl.tm_cgraded2 [in Rec.Framework.sysf_const_terms]
TmVl.tm_igraded2 [in Rec.Framework.sysf_const_terms]
TmVl.tm_graded2 [in Rec.Framework.sysf_const_terms]
TmVl.tm_ren_inst [in Rec.Framework.sysf_terms]
TmVl.tm_pgraded2 [in Rec.Framework.sysf_terms]
TmVl.tm_cgraded2 [in Rec.Framework.sysf_terms]
TmVl.tm_igraded2 [in Rec.Framework.sysf_terms]
TmVl.tm_graded2 [in Rec.Framework.sysf_terms]
TmVl.tm_ind [in Rec.Framework.sysf_terms]
TmVl.tv_ind [in Rec.Framework.sysf_terms]
TmVl.vl_ren_inst [in Rec.Framework.sysf_terms]
TmVl.vl_pgraded2 [in Rec.Framework.sysf_terms]
TmVl.vl_cgraded2 [in Rec.Framework.sysf_terms]
TmVl.vl_igraded2 [in Rec.Framework.sysf_terms]
TmVl.vl_graded2 [in Rec.Framework.sysf_terms]
TmVl.vl_ind [in Rec.Framework.sysf_terms]
tm_sty [in Rec.Examples.sysf_wn]
tm_ty_ind [in Rec.Examples.sysf_wn]
tm_sty [in Rec.Examples.sysf_const_sn]
triangle [in Rec.Base.ARS]
type_of_model [in Rec.Examples.sysf_typing]
type_of_traversal [in Rec.Examples.sysf_typing]
TyTerms.eval [in Rec.Framework.sysf_types]
TyTerms.inst_comp [in Rec.Framework.sysf_types]
TyTerms.lift [in Rec.Framework.sysf_types]
TyTerms.lift_smodel [in Rec.Framework.sysf_types]
TyTerms.lift_model [in Rec.Framework.sysf_types]
TyTerms.lift_is_natural [in Rec.Framework.sysf_types]
TyTerms.model_is_natural [in Rec.Framework.sysf_types]
TyTerms.ren_model [in Rec.Framework.sysf_types]
TyTerms.ren_traversal [in Rec.Framework.sysf_types]
TyTerms.seval [in Rec.Framework.sysf_types]
TyTerms.smodel_to_model [in Rec.Framework.sysf_types]
TyTerms.smodel_to_traversal [in Rec.Framework.sysf_types]
TyTerms.ty_ren_inst [in Rec.Framework.sysf_types]
TyTerms.ty_pgraded1 [in Rec.Framework.sysf_types]
TyTerms.ty_igraded1 [in Rec.Framework.sysf_types]
TyTerms.ty_cgraded1 [in Rec.Framework.sysf_types]
TyTerms.ty_graded1 [in Rec.Framework.sysf_types]
U
up [in Rec.Base.fintype]V
vl_sty [in Rec.Examples.sysf_wn]vl_ty_ind [in Rec.Examples.sysf_wn]
Vs [in Rec.Examples.sysf_wn]
vt_ty_ind [in Rec.Examples.sysf_wn]
W
W [in Rec.Examples.sysf_wn]wn [in Rec.Base.ARS]
Record Index
C
CGraded1.class_of [in Rec.Framework.graded]CGraded1.type [in Rec.Framework.graded]
CGraded2.class_of [in Rec.Framework.graded]
CGraded2.type [in Rec.Framework.graded]
G
Graded1.type [in Rec.Framework.graded]Graded2.type [in Rec.Framework.graded]
I
IGraded1.class_of [in Rec.Framework.graded]IGraded1.type [in Rec.Framework.graded]
IGraded2.class_of [in Rec.Framework.graded]
IGraded2.type [in Rec.Framework.graded]
iren [in Rec.Base.fintype]
L
LambdaTerms.is_natural [in Rec.Extras.lambda_terms]LambdaTerms.model [in Rec.Extras.lambda_terms]
LambdaTerms.smodel [in Rec.Extras.lambda_terms]
LambdaTerms.traversal [in Rec.Extras.lambda_terms]
P
PGraded1.class_of [in Rec.Framework.graded]PGraded1.type [in Rec.Framework.graded]
PGraded2.class_of [in Rec.Framework.graded]
PGraded2.type [in Rec.Framework.graded]
R
reducible [in Rec.Examples.sysf_const_sn]T
TmVl.is_natural [in Rec.Framework.sysf_const_terms]TmVl.is_natural [in Rec.Framework.sysf_terms]
TmVl.model [in Rec.Framework.sysf_const_terms]
TmVl.model [in Rec.Framework.sysf_terms]
TmVl.traversal [in Rec.Framework.sysf_const_terms]
TmVl.traversal [in Rec.Framework.sysf_terms]
TyTerms.is_natural [in Rec.Framework.sysf_types]
TyTerms.model [in Rec.Framework.sysf_types]
TyTerms.smodel [in Rec.Framework.sysf_types]
TyTerms.traversal [in Rec.Framework.sysf_types]
| 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 | (1116 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 | (50 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 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 | (13 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 | (271 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 | (83 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) |
| 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 | (16 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 | (71 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 | (40 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 | (232 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 | (216 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 | (30 entries) |