| 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 | (882 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 | (45 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 | (33 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 | (23 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 | (403 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 | (171 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 | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 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 | (7 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 | (29 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 | (127 entries) |
Global Index
A
all_seq_inf [definition, in Sequences]app_sel_fields [lemma, in Binding]
app_inv_right [lemma, in Binding]
avar [inductive, in Definitions]
avar_f [constructor, in Definitions]
avar_b [constructor, in Definitions]
B
Binding [library]binds_destruct [lemma, in Binding]
binds_inert [lemma, in PreciseFlow]
C
CanonicalForms [library]canonical_forms_fun [lemma, in CanonicalForms]
CompilerExample [section, in CompilerExample]
CompilerExample [library]
CompilerExample.denotation [variable, in CompilerExample]
CompilerExample.dottyCore [variable, in CompilerExample]
CompilerExample.DottyCore [variable, in CompilerExample]
CompilerExample.srcPos [variable, in CompilerExample]
CompilerExample.ST [variable, in CompilerExample]
CompilerExample.symb [variable, in CompilerExample]
CompilerExample.symbol [variable, in CompilerExample]
CompilerExample.Symbol [variable, in CompilerExample]
CompilerExample.symbols [variable, in CompilerExample]
CompilerExample.tpe [variable, in CompilerExample]
CompilerExample.Tpe [variable, in CompilerExample]
CompilerExample.TS [variable, in CompilerExample]
CompilerExample.TS' [variable, in CompilerExample]
CompilerExample.typeRef [variable, in CompilerExample]
CompilerExample.types [variable, in CompilerExample]
compiler_typecheck [lemma, in CompilerExample]
corresponding_types_fun [lemma, in CanonicalForms]
ctx [definition, in Definitions]
cycle_infseq [lemma, in Sequences]
cyclic_path [definition, in Safety]
D
dec [inductive, in Definitions]dec_mut [definition, in Definitions]
dec_trm [constructor, in Definitions]
dec_typ [constructor, in Definitions]
def [inductive, in Definitions]
Definitions [library]
defp [constructor, in Definitions]
defrhs_mut [definition, in Definitions]
defs [inductive, in Definitions]
defs_has_hasnt_neq [lemma, in Binding]
defs_has_inv [lemma, in Binding]
defs_invert_trm [lemma, in RecordAndInertTypes]
defs_has_open' [lemma, in RecordAndInertTypes]
defs_has_open [lemma, in RecordAndInertTypes]
defs_mut [definition, in Definitions]
defs_hasnt [definition, in Definitions]
defs_has [definition, in Definitions]
defs_cons [constructor, in Definitions]
defs_nil [constructor, in Definitions]
defs_typing_rhs [lemma, in Safety]
defs_typing_sngl_rhs [lemma, in Safety]
deftrm [definition, in CanonicalForms]
defv [constructor, in Definitions]
def_mut [definition, in Definitions]
def_rhs [inductive, in Definitions]
def_trm [constructor, in Definitions]
def_typ [constructor, in Definitions]
def_typing_rhs [lemma, in Safety]
diverges [definition, in Safety]
diverges' [definition, in Safety]
DottyCoreAbstract [abbreviation, in CompilerExample]
DottyCorePackage [abbreviation, in CompilerExample]
DottyCoreTight [abbreviation, in CompilerExample]
E
env_ok_inv' [lemma, in Binding]env_ok_inv [lemma, in Binding]
er_lookup [constructor, in Safety]
er_red [constructor, in Safety]
ExampleTactics [library]
ExtendedSafety [section, in Safety]
_ ↠* _ [notation, in Safety]
_ ↠ _ [notation, in Safety]
extended_safety [lemma, in Safety]
extended_red [inductive, in Safety]
extend_infseq [lemma, in Safety]
F
fields [definition, in Definitions]field_sel_nil [lemma, in Binding]
field_sel_open [lemma, in Binding]
field_typing_comp2 [lemma, in PreciseTyping]
field_typing_comp1 [lemma, in PreciseTyping]
field_elim_q3 [lemma, in PreciseTyping]
field_elim_q2 [lemma, in PreciseTyping]
field_elim_q [lemma, in PreciseTyping]
field_elim_q0' [lemma, in PreciseTyping]
field_elim_q0 [lemma, in PreciseTyping]
finseq_unique [lemma, in Sequences]
fresh_subst_typ_dec [lemma, in Binding]
fv_ctx_types_push_eq [lemma, in Binding]
fv_sta_vals [definition, in Definitions]
fv_ctx_types [definition, in Definitions]
fv_defrhs [definition, in Definitions]
fv_defs [definition, in Definitions]
fv_def [definition, in Definitions]
fv_val [definition, in Definitions]
fv_trm [definition, in Definitions]
fv_dec [definition, in Definitions]
fv_typ [definition, in Definitions]
fv_path [definition, in Definitions]
fv_avar [definition, in Definitions]
G
GeneralToTight [library]general_to_tight_typing [lemma, in GeneralToTight]
general_to_tight [lemma, in GeneralToTight]
get_def [definition, in Definitions]
H
hasnt_notin [lemma, in RecordAndInertTypes]I
Id [abbreviation, in ExampleTactics]id [abbreviation, in ExampleTactics]
inert [inductive, in Definitions]
inert_prefix [lemma, in RecordAndInertTypes]
inert_prefix_one [lemma, in RecordAndInertTypes]
inert_concat [lemma, in RecordAndInertTypes]
inert_record_has [lemma, in RecordAndInertTypes]
inert_sngl [definition, in RecordAndInertTypes]
inert_mut [definition, in Definitions]
inert_push [constructor, in Definitions]
inert_empty [constructor, in Definitions]
inert_typ_bnd [constructor, in Definitions]
inert_typ_all [constructor, in Definitions]
inert_typ [inductive, in Definitions]
inert_ok [lemma, in PreciseFlow]
infseq [inductive, in Sequences]
infseq_all_seq_inf [lemma, in Sequences]
infseq_finseq_excl [lemma, in Sequences]
infseq_star_inv [lemma, in Sequences]
infseq_or_finseq [lemma, in Sequences]
infseq_from_function [lemma, in Sequences]
infseq_if_all_seq_inf [lemma, in Sequences]
infseq_coinduction_principle_2 [lemma, in Sequences]
infseq_coinduction_principle [lemma, in Sequences]
infseq_step [constructor, in Sequences]
infseq_with_function [definition, in Sequences]
InvertibleTyping [library]
invertible_typing_closure_tight_v [lemma, in ReplacementTyping]
invertible_andv [lemma, in ReplacementTyping]
invertible_to_precise_obj [lemma, in InvertibleTyping]
invertible_val_to_precise_lambda [lemma, in InvertibleTyping]
invertible_repl_closure_v [lemma, in InvertibleTyping]
invertible_repl_closure_v_helper [lemma, in InvertibleTyping]
invertible_repl_closure_comp_typed [lemma, in InvertibleTyping]
invertible_bnd [lemma, in InvertibleTyping]
invertible_and [lemma, in InvertibleTyping]
invertible_bot [lemma, in InvertibleTyping]
invertible_repl_closure [lemma, in InvertibleTyping]
invertible_repl_closure_helper [lemma, in InvertibleTyping]
invertible_to_precise_rcd [lemma, in InvertibleTyping]
invertible_to_precise_typ_all [lemma, in InvertibleTyping]
invert_fv_ctx_types_push [lemma, in Binding]
inv_sngl_trans [lemma, in ReplacementTyping]
inv_backtrack [lemma, in InvertibleTyping]
inv_to_prec [lemma, in InvertibleTyping]
inv_to_precise_sngl [lemma, in InvertibleTyping]
inv_to_precise_sngl_repl_comp [lemma, in InvertibleTyping]
irred [definition, in Sequences]
is_sngl [definition, in RecordAndInertTypes]
L
label [inductive, in Definitions]label_of_dec [definition, in Definitions]
label_of_def [definition, in Definitions]
label_trm [constructor, in Definitions]
label_typ [constructor, in Definitions]
last_field [lemma, in Binding]
last_path [lemma, in PreciseTyping]
Lazy [abbreviation, in ExampleTactics]
lazy [abbreviation, in ExampleTactics]
let_trm [abbreviation, in ExampleTactics]
lfs_defs_typing [lemma, in Safety]
lft_typ_sngl_inv [lemma, in Safety]
lft_typ_all_inv [lemma, in Safety]
lft_unique [lemma, in Safety]
lft_inert [lemma, in Safety]
lft_cons [constructor, in Safety]
lft_empty [constructor, in Safety]
ListExample [section, in ListExample]
ListExample [library]
ListExample.A [variable, in ListExample]
ListExample.Cons [variable, in ListExample]
ListExample.head [variable, in ListExample]
ListExample.HT [variable, in ListExample]
ListExample.List [variable, in ListExample]
ListExample.NC [variable, in ListExample]
ListExample.Nil [variable, in ListExample]
ListExample.tail [variable, in ListExample]
ListObjType [abbreviation, in ListExample]
ListType [abbreviation, in ListExample]
ListTypeA [abbreviation, in ListExample]
list_typing [lemma, in ListExample]
Lookup [library]
lookup_same_var_same_type [lemma, in CanonicalForms]
lookup_step_preservation_sngl_prec3 [lemma, in CanonicalForms]
lookup_preservation_forall [lemma, in CanonicalForms]
lookup_pres [lemma, in CanonicalForms]
lookup_step_pres [lemma, in CanonicalForms]
lookup_step_preservation_prec3_fun [lemma, in CanonicalForms]
lookup_step_preservation_inert_prec3 [lemma, in CanonicalForms]
lookup_step_preservation_prec2 [lemma, in CanonicalForms]
lookup_step_preservation_prec1 [lemma, in CanonicalForms]
lookup_weaken [lemma, in Lookup]
lookup_weaken_one [lemma, in Lookup]
lookup_step_weaken [lemma, in Lookup]
lookup_step_weaken_one [lemma, in Lookup]
lookup_func [lemma, in Lookup]
lookup_irred [lemma, in Lookup]
lookup_step_func [lemma, in Lookup]
lookup_val_inv [lemma, in Lookup]
lookup_strengthen [lemma, in Lookup]
lookup_strengthen_one [lemma, in Lookup]
lookup_empty [lemma, in Lookup]
lookup_sel_v [constructor, in Lookup]
lookup_sel_p [constructor, in Lookup]
lookup_var [constructor, in Lookup]
lookup_step [inductive, in Lookup]
lookup_fields_typ [inductive, in Safety]
M
map_lookup_extend [lemma, in Safety]map_red_extend [lemma, in Safety]
N
named_path [definition, in Binding]named_lookup_step [lemma, in Lookup]
Narrowing [library]
narrow_defs [lemma, in Narrowing]
narrow_subtyping [lemma, in Narrowing]
narrow_typing [lemma, in Narrowing]
narrow_rules [lemma, in Narrowing]
nf_val [constructor, in Reduction]
nf_path [constructor, in Reduction]
norm_form [inductive, in Reduction]
O
object_typing [lemma, in CanonicalForms]open_env_last_defs [lemma, in Binding]
open_env_rules [lemma, in Binding]
open_fresh_typ_dec_injective [lemma, in Binding]
open_fresh_path_injective [lemma, in Binding]
open_fresh_avar_injective [lemma, in Binding]
open_var_trm_eq [lemma, in Binding]
open_var_defs_eq [lemma, in Binding]
open_var_trm_val_def_eq [lemma, in Binding]
open_var_typ_eq [lemma, in Binding]
open_var_typ_dec_eq [lemma, in Binding]
open_var_path_eq [lemma, in Binding]
open_named_path [lemma, in Binding]
open_record_type_p [lemma, in RecordAndInertTypes]
open_record_typ_p [lemma, in RecordAndInertTypes]
open_record_p [lemma, in RecordAndInertTypes]
open_dec_preserves_label_p [lemma, in RecordAndInertTypes]
open_dec_preserves_label [lemma, in RecordAndInertTypes]
open_defrhs_p [definition, in Definitions]
open_defs_p [definition, in Definitions]
open_def_p [definition, in Definitions]
open_val_p [definition, in Definitions]
open_trm_p [definition, in Definitions]
open_path_p [definition, in Definitions]
open_dec_p [definition, in Definitions]
open_typ_p [definition, in Definitions]
open_avar_p [definition, in Definitions]
open_rec_defrhs_p [definition, in Definitions]
open_rec_defs_p [definition, in Definitions]
open_rec_def_p [definition, in Definitions]
open_rec_val_p [definition, in Definitions]
open_rec_trm_p [definition, in Definitions]
open_rec_dec_p [definition, in Definitions]
open_rec_typ_p [definition, in Definitions]
open_rec_path_p [definition, in Definitions]
open_rec_avar_p [definition, in Definitions]
open_paths [definition, in Definitions]
open_path [definition, in Definitions]
open_defrhsdd [definition, in Definitions]
open_defs [definition, in Definitions]
open_def [definition, in Definitions]
open_val [definition, in Definitions]
open_trm [definition, in Definitions]
open_dec [definition, in Definitions]
open_typ [definition, in Definitions]
open_avar [definition, in Definitions]
open_rec_defrhs [definition, in Definitions]
open_rec_defs [definition, in Definitions]
open_rec_def [definition, in Definitions]
open_rec_val [definition, in Definitions]
open_rec_trm [definition, in Definitions]
open_rec_dec [definition, in Definitions]
open_rec_typ [definition, in Definitions]
open_rec_path [definition, in Definitions]
open_rec_avar [definition, in Definitions]
open_typ_subst [lemma, in Substitution]
P
path [inductive, in Definitions]PathSafety [section, in Safety]
path_sel_repl_inv_v [lemma, in ReplacementTyping]
path_sel_repl_v [lemma, in ReplacementTyping]
path_sel_repl2_v [lemma, in ReplacementTyping]
path_elim_repl [lemma, in ReplacementTyping]
path_sel_repl_inv [lemma, in ReplacementTyping]
path_sel_repl [lemma, in ReplacementTyping]
path_sel_repl2 [lemma, in ReplacementTyping]
path_ref [abbreviation, in ExampleTactics]
path_sel_inv_v [lemma, in InvertibleTyping]
path_sel_inv [lemma, in InvertibleTyping]
path_elim_prec [lemma, in PreciseTyping]
path_typ_all_to_precise [lemma, in GeneralToTight]
path_safety [lemma, in Safety]
pfv_inert [lemma, in PreciseFlow]
pf_sngl_sel_unique [lemma, in PreciseFlow]
pf_sngl_flds_elim [lemma, in PreciseFlow]
pf_sngl_fld_elim [lemma, in PreciseFlow]
pf_weaken [lemma, in PreciseFlow]
pf_weaken_one [lemma, in PreciseFlow]
pf_sngl [lemma, in PreciseFlow]
pf_path_sel [lemma, in PreciseFlow]
pf_strengthen [lemma, in PreciseFlow]
pf_dec_typ_tight [lemma, in PreciseFlow]
pf_T_unique [lemma, in PreciseFlow]
pf_dec_typ_unique [lemma, in PreciseFlow]
pf_record_has_U [lemma, in PreciseFlow]
pf_record_has_T [lemma, in PreciseFlow]
pf_psel [lemma, in PreciseFlow]
pf_bot [lemma, in PreciseFlow]
pf_binds [lemma, in PreciseFlow]
pf_forall_T [lemma, in PreciseFlow]
pf_bnd_T2 [lemma, in PreciseFlow]
pf_sngl_T [lemma, in PreciseFlow]
pf_bnd_T [lemma, in PreciseFlow]
pf_sngl_U [lemma, in PreciseFlow]
pf_rec_rcd_U [lemma, in PreciseFlow]
pf_rcd_T [lemma, in PreciseFlow]
pf_inert [lemma, in PreciseFlow]
pf_inertsngl [lemma, in PreciseFlow]
pf_forall_U [lemma, in PreciseFlow]
pf_and2 [constructor, in PreciseFlow]
pf_and1 [constructor, in PreciseFlow]
pf_open [constructor, in PreciseFlow]
pf_fld [constructor, in PreciseFlow]
pf_bind [constructor, in PreciseFlow]
pf_strengthen_from_pt3 [lemma, in PreciseTyping]
pf_strengthen_one_helper [lemma, in PreciseTyping]
pf_inert_pt3_sngl_false [lemma, in PreciseTyping]
pf_inert_pt2_sngl_false [lemma, in PreciseTyping]
pf_pt3_unique [lemma, in PreciseTyping]
pf_pt3_trans_inv_mult' [lemma, in PreciseTyping]
pf_pt3_trans_inv_mult [lemma, in PreciseTyping]
pf_pt2_trans_inv_mult [lemma, in PreciseTyping]
pf_strengthen_full [lemma, in PreciseTyping]
pf_pt2_sngl_invert [lemma, in PreciseTyping]
pf_pt2_sngl [lemma, in PreciseTyping]
pf_pt2 [lemma, in PreciseTyping]
pf_sngl_to_lft [lemma, in Safety]
plus [inductive, in Sequences]
plus_right [lemma, in Sequences]
plus_star_trans [lemma, in Sequences]
plus_star [lemma, in Sequences]
plus_one [lemma, in Sequences]
plus_left [constructor, in Sequences]
PreciseFlow [library]
PreciseTyping [library]
precise_to_general_v [lemma, in PreciseFlow]
precise_to_general [lemma, in PreciseFlow]
precise_to_general_h [lemma, in PreciseFlow]
precise_flow [inductive, in PreciseFlow]
precise_to_general3 [lemma, in PreciseTyping]
precise_to_general2 [lemma, in PreciseTyping]
precise_typing3 [inductive, in PreciseTyping]
precise_typing2 [inductive, in PreciseTyping]
preservation [lemma, in Safety]
prev_var_exists [lemma, in CanonicalForms]
progress [lemma, in Safety]
proj_rewrite' [lemma, in Binding]
proj_rewrite_mult [lemma, in Binding]
proj_rewrite [lemma, in Binding]
pt2 [constructor, in PreciseTyping]
pt2_strengthen_from_pf [lemma, in PreciseTyping]
pt2_strengthen_full [lemma, in PreciseTyping]
pt2_strengthen [lemma, in PreciseTyping]
pt2_fld_strengthen [lemma, in PreciseTyping]
pt2_strengthen_one [lemma, in PreciseTyping]
pt2_strengthen_one_helper [lemma, in PreciseTyping]
pt2_qbs_typed [lemma, in PreciseTyping]
pt2_dec_typ_tight [lemma, in PreciseTyping]
pt2_exists [lemma, in PreciseTyping]
pt2_bnd [lemma, in PreciseTyping]
pt2_to_pf [lemma, in PreciseTyping]
pt2_var_sngl [lemma, in PreciseTyping]
pt2_destruct_env [lemma, in PreciseTyping]
pt2_weaken [lemma, in PreciseTyping]
pt2_weaken_one [lemma, in PreciseTyping]
pt2_backtrack [lemma, in PreciseTyping]
pt2_sngl_unique' [lemma, in PreciseTyping]
pt2_sngl_unique [lemma, in PreciseTyping]
pt2_sngl_exists [lemma, in PreciseTyping]
pt2_psel [lemma, in PreciseTyping]
pt2_inertsngl [lemma, in PreciseTyping]
pt2_and_destruct2 [lemma, in PreciseTyping]
pt2_and_destruct1 [lemma, in PreciseTyping]
pt2_sngl_trans [constructor, in PreciseTyping]
pt23_invert [lemma, in PreciseTyping]
pt3 [constructor, in PreciseTyping]
pt3_fld_strengthen [lemma, in PreciseTyping]
pt3_strengthen_full [lemma, in PreciseTyping]
pt3_strengthen [lemma, in PreciseTyping]
pt3_strengthen_one [lemma, in PreciseTyping]
pt3_dec_typ_tight [lemma, in PreciseTyping]
pt3_inert_sngl_invert [lemma, in PreciseTyping]
pt3_inert_pt2_sngl_invert [lemma, in PreciseTyping]
pt3_var_sngl [lemma, in PreciseTyping]
pt3_invert [lemma, in PreciseTyping]
pt3_bnd [lemma, in PreciseTyping]
pt3_trans_trans [lemma, in PreciseTyping]
pt3_weaken [lemma, in PreciseTyping]
pt3_weaken_one [lemma, in PreciseTyping]
pt3_field_trans' [lemma, in PreciseTyping]
pt3_field_trans [lemma, in PreciseTyping]
pt3_sngl_trans3 [lemma, in PreciseTyping]
pt3_backtrack [lemma, in PreciseTyping]
pt3_field_elim_p [lemma, in PreciseTyping]
pt3_field_elim [lemma, in PreciseTyping]
pt3_trans2 [lemma, in PreciseTyping]
pt3_trans [lemma, in PreciseTyping]
pt3_psel [lemma, in PreciseTyping]
pt3_inertsngl [lemma, in PreciseTyping]
pt3_and_destruct2 [lemma, in PreciseTyping]
pt3_and_destruct1 [lemma, in PreciseTyping]
pt3_sngl_trans [constructor, in PreciseTyping]
pt3_exists [lemma, in GeneralToTight]
pvar [abbreviation, in Definitions]
p_sel [constructor, in Definitions]
R
rall1 [constructor, in Definitions]rall2 [constructor, in Definitions]
rand1 [constructor, in Definitions]
rand2 [constructor, in Definitions]
rbnd [constructor, in Definitions]
rcd_mutind [definition, in Definitions]
rcd_typ_mut [definition, in Definitions]
rcd_dec_mut [definition, in Definitions]
rdtrm [constructor, in Definitions]
rdtyp1 [constructor, in Definitions]
rdtyp2 [constructor, in Definitions]
rd_trm_sngl [constructor, in Definitions]
rd_trm [constructor, in Definitions]
rd_typ [constructor, in Definitions]
RecordAndInertTypes [library]
record_has_ty_defs [lemma, in Binding]
record_typ_has_label_in [lemma, in RecordAndInertTypes]
record_open_tight [lemma, in RecordAndInertTypes]
record_open [lemma, in RecordAndInertTypes]
record_type [definition, in Definitions]
record_has [inductive, in Definitions]
record_typ [inductive, in Definitions]
record_dec [inductive, in Definitions]
red [inductive, in Reduction]
Reduction [library]
red_let_tgt [constructor, in Reduction]
red_let_path [constructor, in Reduction]
red_let_val [constructor, in Reduction]
red_app [constructor, in Reduction]
rename_defs [lemma, in Substitution]
rename_def_defs [lemma, in Substitution]
rename_ty_trm [lemma, in Substitution]
Replacement [library]
ReplacementTyping [library]
replacement_closure_v [lemma, in ReplacementTyping]
replacement_repl_closure_pq3_v [lemma, in ReplacementTyping]
replacement_repl_closure_pq2_v [lemma, in ReplacementTyping]
replacement_repl_closure_pq_v [lemma, in ReplacementTyping]
replacement_repl_closure_qp3_v [lemma, in ReplacementTyping]
replacement_repl_closure_qp2_v [lemma, in ReplacementTyping]
replacement_repl_closure_qp_v [lemma, in ReplacementTyping]
replacement_closure [lemma, in ReplacementTyping]
replacement_repl_closure_comp_typed [lemma, in ReplacementTyping]
replacement_subtyping_closure [lemma, in ReplacementTyping]
replacement_repl_closure_pq_comp [lemma, in ReplacementTyping]
replacement_repl_closure_pq3 [lemma, in ReplacementTyping]
replacement_repl_closure_pq2 [lemma, in ReplacementTyping]
replacement_repl_closure_pq [lemma, in ReplacementTyping]
replacement_repl_closure_pq_helper [lemma, in ReplacementTyping]
replacement_repl_closure_pq_helper_mutind [lemma, in ReplacementTyping]
replacement_repl_closure_qp_comp [lemma, in ReplacementTyping]
replacement_repl_closure_qp3 [lemma, in ReplacementTyping]
replacement_repl_closure_qp2 [lemma, in ReplacementTyping]
replacement_repl_closure_qp [lemma, in ReplacementTyping]
repl_to_invertible_obj [lemma, in ReplacementTyping]
repl_andv [lemma, in ReplacementTyping]
repl_sngl_trans [lemma, in ReplacementTyping]
repl_to_invertible_sngl [lemma, in ReplacementTyping]
repl_to_invertible_sngl_repl_comp [lemma, in ReplacementTyping]
repl_fld [lemma, in ReplacementTyping]
repl_prec_exists [lemma, in ReplacementTyping]
repl_top [lemma, in ReplacementTyping]
repl_to_inv [lemma, in ReplacementTyping]
repl_rec_intro [lemma, in ReplacementTyping]
repl_and [lemma, in ReplacementTyping]
repl_to_precise_rcd [lemma, in ReplacementTyping]
repl_to_precise_typ_all [lemma, in ReplacementTyping]
repl_typ_subst [lemma, in Replacement]
repl_typ_subst_mutind [lemma, in Replacement]
repl_prefixes_sel [lemma, in Replacement]
repl_prefixes_sngl [lemma, in Replacement]
repl_field_elim [lemma, in Replacement]
repl_field_elim_mutind [lemma, in Replacement]
repl_insert [lemma, in Replacement]
repl_insert_mutind [lemma, in Replacement]
repl_comp_open [lemma, in Replacement]
repl_comp_open_rec [lemma, in Replacement]
repl_star_trm [lemma, in Replacement]
repl_star_typ2 [lemma, in Replacement]
repl_star_typ1 [lemma, in Replacement]
repl_star_all2 [lemma, in Replacement]
repl_star_all1 [lemma, in Replacement]
repl_star_bnd [lemma, in Replacement]
repl_star_and2 [lemma, in Replacement]
repl_star_and1 [lemma, in Replacement]
repl_star_rcd [lemma, in Replacement]
repl_repeat_dec [abbreviation, in Replacement]
repl_repeat_typ [abbreviation, in Replacement]
repl_open_var [lemma, in Replacement]
repl_open [lemma, in Replacement]
repl_open_rec [lemma, in Replacement]
repl_intro_sngl [lemma, in Replacement]
repl_swap [lemma, in Replacement]
repl_mutind [definition, in Definitions]
repl_dec_mut [definition, in Definitions]
repl_typ_mut [definition, in Definitions]
repl_dec [inductive, in Definitions]
repl_typ [inductive, in Definitions]
repl_composition_sub [lemma, in InvertibleTyping]
repl_sub [lemma, in InvertibleTyping]
repl_composition_fld_elim [lemma, in PreciseTyping]
repl_comp_trans_record_has [lemma, in PreciseTyping]
repl_comp_trans_open [lemma, in PreciseTyping]
repl_composition_weaken [lemma, in PreciseTyping]
repl_composition_weaken_one [lemma, in PreciseTyping]
repl_composition_open [lemma, in PreciseTyping]
repl_comp_record_has1 [lemma, in PreciseTyping]
repl_comp_record_has2 [lemma, in PreciseTyping]
repl_comp_typ_and2 [lemma, in PreciseTyping]
repl_comp_typ_and1 [lemma, in PreciseTyping]
repl_comp_trm_rcd' [lemma, in PreciseTyping]
repl_comp_trm_rcd [lemma, in PreciseTyping]
repl_comp_bnd' [lemma, in PreciseTyping]
repl_comp_bnd_inv2 [lemma, in PreciseTyping]
repl_comp_bnd_inv1 [lemma, in PreciseTyping]
repl_comp_sngl_inv2 [lemma, in PreciseTyping]
repl_comp_sngl_inv1 [lemma, in PreciseTyping]
repl_comp_to_prec' [lemma, in PreciseTyping]
repl_composition_qp [definition, in PreciseTyping]
rh_andr [constructor, in Definitions]
rh_andl [constructor, in Definitions]
rh_one [constructor, in Definitions]
rpath [constructor, in Definitions]
rrcd [constructor, in Definitions]
rsngl [constructor, in Definitions]
rt_cons [constructor, in Definitions]
rt_one [constructor, in Definitions]
rules_mutind [definition, in Definitions]
rules_subtyp [definition, in Definitions]
rules_defs_mut [definition, in Definitions]
rules_def_mut [definition, in Definitions]
rules_trm_mut [definition, in Definitions]
S
safety [lemma, in Safety]Safety [section, in Safety]
Safety [library]
safety_helper [lemma, in Safety]
_ ==> _ = _ => _ [notation, in Safety]
sel_sub_fields [lemma, in Binding]
sel_fields_equal [lemma, in Binding]
sel_field_to_fields [lemma, in Binding]
sel_fields_subst [lemma, in Binding]
sel_fields_open [lemma, in Binding]
sel_fieldss_subst [lemma, in Replacement]
sel_fields [definition, in Definitions]
sel_field [definition, in Definitions]
sel_replacement [lemma, in GeneralToTight]
SEQUENCES [section, in Sequences]
Sequences [library]
SEQUENCES.A [variable, in Sequences]
SEQUENCES.R [variable, in Sequences]
SEQUENCES.R_functional [variable, in Sequences]
SingletonTypeExample [section, in SingletonTypeExample]
SingletonTypeExample [library]
SingletonTypeExample.C [variable, in SingletonTypeExample]
SingletonTypeExample.CD [variable, in SingletonTypeExample]
SingletonTypeExample.d [variable, in SingletonTypeExample]
SingletonTypeExample.D [variable, in SingletonTypeExample]
SingletonTypeExample.decr [variable, in SingletonTypeExample]
SingletonTypeExample.di [variable, in SingletonTypeExample]
SingletonTypeExample.incr [variable, in SingletonTypeExample]
sngl_path_lookup [lemma, in CanonicalForms]
sngl_typed3 [lemma, in PreciseTyping]
sngl_typed2 [lemma, in PreciseTyping]
sngl_typed [lemma, in PreciseTyping]
sngl_replacement [lemma, in GeneralToTight]
sssssuper [abbreviation, in ExampleTactics]
ssssuper [abbreviation, in ExampleTactics]
sssuper [abbreviation, in ExampleTactics]
ssuper [abbreviation, in ExampleTactics]
sta [definition, in Definitions]
star [inductive, in Sequences]
star_star_inv [lemma, in Sequences]
star_plus_trans [lemma, in Sequences]
star_trans [lemma, in Sequences]
star_one [lemma, in Sequences]
star_step [constructor, in Sequences]
star_refl [constructor, in Sequences]
subenv [inductive, in Subenvironments]
Subenvironments [library]
subenv_implies_ok [lemma, in Subenvironments]
subenv_last [lemma, in Subenvironments]
subenv_extend [lemma, in Subenvironments]
subenv_refl [lemma, in Subenvironments]
subenv_push [constructor, in Subenvironments]
subenv_empty [constructor, in Subenvironments]
Substitution [library]
subst_defs_hasnt_label [lemma, in Binding]
subst_defs_hasnt [lemma, in Binding]
subst_label_of_def [lemma, in Binding]
subst_intro_defs [lemma, in Binding]
subst_intro_typ [lemma, in Binding]
subst_intro_trm [lemma, in Binding]
subst_open_commut_defs_p [lemma, in Binding]
subst_open_commut_trm_p [lemma, in Binding]
subst_open_commut_trm_val_def_defs_p [lemma, in Binding]
subst_open_commut_typ_p [lemma, in Binding]
subst_open_commut_typ_dec_p [lemma, in Binding]
subst_open_commut_path_p [lemma, in Binding]
subst_open_commut_defs [lemma, in Binding]
subst_open_commut_trm [lemma, in Binding]
subst_open_commut_trm_val_def_defs [lemma, in Binding]
subst_open_commut_typ [lemma, in Binding]
subst_open_commut_typ_dec [lemma, in Binding]
subst_open_commut_path [lemma, in Binding]
subst_open_commut_avar [lemma, in Binding]
subst_fresh_ctx [lemma, in Binding]
subst_fresh_trm_val_def_defs [lemma, in Binding]
subst_fresh_typ [definition, in Binding]
subst_fresh_typ_dec [lemma, in Binding]
subst_fresh_path [lemma, in Binding]
subst_ctx [definition, in Binding]
subst_defrhs [definition, in Binding]
subst_defs [definition, in Binding]
subst_def [definition, in Binding]
subst_val [definition, in Binding]
subst_trm [definition, in Binding]
subst_dec [definition, in Binding]
subst_typ [definition, in Binding]
subst_path [definition, in Binding]
subst_avar [definition, in Binding]
subst_var_p [definition, in Binding]
subst_var [definition, in Binding]
subst_fresh_var_path [lemma, in Substitution]
subst_var_path [lemma, in Substitution]
subst_ty_trm [lemma, in Substitution]
subst_rules [lemma, in Substitution]
subtyp [inductive, in Definitions]
subtyp_all [constructor, in Definitions]
subtyp_sel1 [constructor, in Definitions]
subtyp_sel2 [constructor, in Definitions]
subtyp_sngl_qp [constructor, in Definitions]
subtyp_sngl_pq [constructor, in Definitions]
subtyp_typ [constructor, in Definitions]
subtyp_fld [constructor, in Definitions]
subtyp_and2 [constructor, in Definitions]
subtyp_and12 [constructor, in Definitions]
subtyp_and11 [constructor, in Definitions]
subtyp_trans [constructor, in Definitions]
subtyp_refl [constructor, in Definitions]
subtyp_bot [constructor, in Definitions]
subtyp_top [constructor, in Definitions]
subtyp_all_t [constructor, in TightTyping]
subtyp_sel1_t [constructor, in TightTyping]
subtyp_sel2_t [constructor, in TightTyping]
subtyp_sngl_qp_t [constructor, in TightTyping]
subtyp_sngl_pq_t [constructor, in TightTyping]
subtyp_typ_t [constructor, in TightTyping]
subtyp_fld_t [constructor, in TightTyping]
subtyp_and2_t [constructor, in TightTyping]
subtyp_and12_t [constructor, in TightTyping]
subtyp_and11_t [constructor, in TightTyping]
subtyp_trans_t [constructor, in TightTyping]
subtyp_refl_t [constructor, in TightTyping]
subtyp_bot_t [constructor, in TightTyping]
subtyp_top_t [constructor, in TightTyping]
subtyp_t [inductive, in TightTyping]
super [abbreviation, in ExampleTactics]
SymbolImpl [abbreviation, in CompilerExample]
symbolsType [abbreviation, in CompilerExample]
T
T [abbreviation, in CompilerExample]t [definition, in CompilerExample]
T [abbreviation, in SingletonTypeExample]
t [abbreviation, in SingletonTypeExample]
t [definition, in ListExample]
tds_mutind [definition, in Definitions]
tds_subtyp [definition, in Definitions]
tds_ty_defs_mut [definition, in Definitions]
tds_ty_def_mut [definition, in Definitions]
tds_ty_trm_mut [definition, in Definitions]
this [abbreviation, in ExampleTactics]
TightTyping [library]
tight_bounds_dec [definition, in Definitions]
tight_bounds [definition, in Definitions]
tight_bounds_subst [lemma, in Substitution]
tight_bounds_subst_mut [lemma, in Substitution]
tight_to_general [lemma, in TightTyping]
tight_to_prec_exists [lemma, in GeneralToTight]
TpeImpl [abbreviation, in CompilerExample]
trm [inductive, in Definitions]
trm_mutind [definition, in Definitions]
trm_mut [definition, in Definitions]
trm_path [constructor, in Definitions]
trm_let [constructor, in Definitions]
trm_app [constructor, in Definitions]
trm_val [constructor, in Definitions]
trm_label [axiom, in Definitions]
ts_mutind [definition, in Definitions]
ts_subtyp [definition, in Definitions]
ts_ty_trm_mut [definition, in Definitions]
ts_mutind_ts [definition, in TightTyping]
ts_subtyp_ts [definition, in TightTyping]
ts_ty_trm_mut_ts [definition, in TightTyping]
tvar [abbreviation, in Definitions]
typ [inductive, in Definitions]
typecheck [lemma, in SingletonTypeExample]
typed_path_lookup3 [lemma, in CanonicalForms]
typed_path_lookup_helper [lemma, in CanonicalForms]
typed_path_lookup_same_var3 [lemma, in CanonicalForms]
typed_path_lookup_same_var2 [lemma, in CanonicalForms]
typed_paths_named [lemma, in Binding]
typed_repl_comp_qp [definition, in PreciseTyping]
typesType [abbreviation, in CompilerExample]
typing_empty_false [lemma, in Binding]
typing_implies_bound [lemma, in Binding]
typ_to_lookup3 [lemma, in CanonicalForms]
typ_to_lookup2 [lemma, in CanonicalForms]
typ_to_lookup1 [lemma, in CanonicalForms]
typ_mutind [definition, in Definitions]
typ_mut [definition, in Definitions]
typ_sngl [constructor, in Definitions]
typ_all [constructor, in Definitions]
typ_bnd [constructor, in Definitions]
typ_path [constructor, in Definitions]
typ_and [constructor, in Definitions]
typ_rcd [constructor, in Definitions]
typ_bot [constructor, in Definitions]
typ_top [constructor, in Definitions]
typ_label [axiom, in Definitions]
ty_sel_qp_rv [constructor, in ReplacementTyping]
ty_rec_qp_rv [constructor, in ReplacementTyping]
ty_sel_rv [constructor, in ReplacementTyping]
ty_and_rv [constructor, in ReplacementTyping]
ty_inv_rv [constructor, in ReplacementTyping]
ty_replv [inductive, in ReplacementTyping]
ty_sngl_qp_r [constructor, in ReplacementTyping]
ty_sel_qp_r [constructor, in ReplacementTyping]
ty_rec_qp_r [constructor, in ReplacementTyping]
ty_rcd_intro_r [constructor, in ReplacementTyping]
ty_sel_r [constructor, in ReplacementTyping]
ty_bnd_r [constructor, in ReplacementTyping]
ty_and_r [constructor, in ReplacementTyping]
ty_inv_r [constructor, in ReplacementTyping]
ty_repl [inductive, in ReplacementTyping]
ty_defs_record_type [lemma, in RecordAndInertTypes]
ty_defs_record_type_helper [lemma, in RecordAndInertTypes]
ty_def_mutind [definition, in Definitions]
ty_defs_mut' [definition, in Definitions]
ty_def_mut' [definition, in Definitions]
ty_mutind [definition, in Definitions]
ty_defs_mut [definition, in Definitions]
ty_def_mut [definition, in Definitions]
ty_trm_mut [definition, in Definitions]
ty_defs_cons [constructor, in Definitions]
ty_defs_one [constructor, in Definitions]
ty_defs [inductive, in Definitions]
ty_def_path [constructor, in Definitions]
ty_def_new [constructor, in Definitions]
ty_def_all [constructor, in Definitions]
ty_def_typ [constructor, in Definitions]
ty_def [inductive, in Definitions]
ty_sub [constructor, in Definitions]
ty_and_intro [constructor, in Definitions]
ty_rec_elim [constructor, in Definitions]
ty_rec_intro [constructor, in Definitions]
ty_path_elim [constructor, in Definitions]
ty_sngl [constructor, in Definitions]
ty_let [constructor, in Definitions]
ty_rcd_intro [constructor, in Definitions]
ty_new_elim [constructor, in Definitions]
ty_new_intro [constructor, in Definitions]
ty_all_elim [constructor, in Definitions]
ty_all_intro [constructor, in Definitions]
ty_var [constructor, in Definitions]
ty_trm [inductive, in Definitions]
ty_rec_pq_invv [constructor, in InvertibleTyping]
ty_top_invv [constructor, in InvertibleTyping]
ty_and_invv [constructor, in InvertibleTyping]
ty_all_invv [constructor, in InvertibleTyping]
ty_precise_invv [constructor, in InvertibleTyping]
ty_val_inv [inductive, in InvertibleTyping]
ty_sngl_pq_inv [constructor, in InvertibleTyping]
ty_sel_pq_inv [constructor, in InvertibleTyping]
ty_rec_pq_inv [constructor, in InvertibleTyping]
ty_top_inv [constructor, in InvertibleTyping]
ty_and_inv [constructor, in InvertibleTyping]
ty_all_inv [constructor, in InvertibleTyping]
ty_dec_typ_inv [constructor, in InvertibleTyping]
ty_dec_trm_inv [constructor, in InvertibleTyping]
ty_precise_inv [constructor, in InvertibleTyping]
ty_path_inv [inductive, in InvertibleTyping]
ty_new_intro_p [constructor, in PreciseFlow]
ty_all_intro_p [constructor, in PreciseFlow]
ty_val_p [inductive, in PreciseFlow]
ty_sub_t [constructor, in TightTyping]
ty_and_intro_t [constructor, in TightTyping]
ty_rec_elim_t [constructor, in TightTyping]
ty_rcd_intro_t [constructor, in TightTyping]
ty_path_elim_t [constructor, in TightTyping]
ty_sngl_t [constructor, in TightTyping]
ty_let_t [constructor, in TightTyping]
ty_rec_intro_t [constructor, in TightTyping]
ty_new_elim_t [constructor, in TightTyping]
ty_new_intro_t [constructor, in TightTyping]
ty_all_elim_t [constructor, in TightTyping]
ty_all_intro_t [constructor, in TightTyping]
ty_var_t [constructor, in TightTyping]
ty_trm_t [inductive, in TightTyping]
U
unique_rcd_trm [lemma, in RecordAndInertTypes]unique_rcd_typ [lemma, in RecordAndInertTypes]
V
val [inductive, in Definitions]val_mut [definition, in Definitions]
val_lambda [constructor, in Definitions]
val_new [constructor, in Definitions]
val_typ_all_to_lambda [lemma, in GeneralToTight]
val_typing [lemma, in Safety]
W
Weakening [library]weaken_ty_defs [lemma, in Weakening]
weaken_subtyp [lemma, in Weakening]
weaken_ty_trm [lemma, in Weakening]
weaken_rules [lemma, in Weakening]
well_typed_notin_dom [lemma, in Binding]
well_typed_to_ok_G [lemma, in Binding]
well_typed_push [constructor, in Definitions]
well_typed_empty [constructor, in Definitions]
well_typed [inductive, in Definitions]
wf [inductive, in PreciseTyping]
wfe_push [constructor, in PreciseTyping]
wfe_empty [constructor, in PreciseTyping]
wf_prefix [lemma, in PreciseTyping]
wf_prefix_one [lemma, in PreciseTyping]
wt_to_ok_γ [lemma, in Binding]
wt_prefix [lemma, in Binding]
other
_ ⊢//v _ : _ [notation, in ReplacementTyping]_ ⊢// _ : _ [notation, in ReplacementTyping]
_ Λ _ [notation, in ExampleTactics]
_ ⫶ _ [notation, in Definitions]
_ ⊢ _ <: _ [notation, in Definitions]
_ ; _ ; _ ⊢ _ :: _ [notation, in Definitions]
_ ; _ ; _ ⊢ _ : _ [notation, in Definitions]
_ ⊢ _ : _ [notation, in Definitions]
_ •• _ [notation, in Definitions]
_ • _ [notation, in Definitions]
_ ↓ _ [notation, in Definitions]
_ ∧ _ [notation, in Definitions]
_ ⊢##v _ : _ [notation, in InvertibleTyping]
_ ⊢## _ : _ [notation, in InvertibleTyping]
_ ⟼* _ [notation, in Reduction]
_ ⟼ _ [notation, in Reduction]
_ ⟦ _ ⤳* _ ⟧ [notation, in Lookup]
_ ⟦ _ ⤳ _ ⟧ [notation, in Lookup]
_ ⊢! _ : _ ⪼ _ [notation, in PreciseFlow]
_ ⊢!v _ : _ [notation, in PreciseFlow]
_ ⊢# _ <: _ [notation, in TightTyping]
_ ⊢# _ : _ [notation, in TightTyping]
_ ⪯ _ [notation, in Subenvironments]
_ ⊩ _ ⟿' _ ⬳ _ [notation, in PreciseTyping]
_ ⊩ _ ⟿ _ ⬳ _ [notation, in PreciseTyping]
_ ⊢ _ ⟿' _ [notation, in PreciseTyping]
_ ⊢ _ ⟿ _ [notation, in PreciseTyping]
_ ⊢!!! _ : _ [notation, in PreciseTyping]
_ ⊢!! _ : _ [notation, in PreciseTyping]
{ _ ⦂= _ } [notation, in Definitions]
{ _ :=v _ } [notation, in Definitions]
{ _ :=p _ } [notation, in Definitions]
{ _ := _ } [notation, in Definitions]
{ _ >: _ <: _ } [notation, in Definitions]
{ _ ⦂ _ } [notation, in Definitions]
{{ _ }} [notation, in Definitions]
∀ ( _ ) _ [notation, in Definitions]
⊤ [notation, in Definitions]
⊥ [notation, in Definitions]
λ ( _ ) _ [notation, in Definitions]
μ _ [notation, in Definitions]
ν ( _ ) _ [notation, in Definitions]
Notation Index
E
_ ↠* _ [in Safety]_ ↠ _ [in Safety]
S
_ ==> _ = _ => _ [in Safety]other
_ ⊢//v _ : _ [in ReplacementTyping]_ ⊢// _ : _ [in ReplacementTyping]
_ Λ _ [in ExampleTactics]
_ ⫶ _ [in Definitions]
_ ⊢ _ <: _ [in Definitions]
_ ; _ ; _ ⊢ _ :: _ [in Definitions]
_ ; _ ; _ ⊢ _ : _ [in Definitions]
_ ⊢ _ : _ [in Definitions]
_ •• _ [in Definitions]
_ • _ [in Definitions]
_ ↓ _ [in Definitions]
_ ∧ _ [in Definitions]
_ ⊢##v _ : _ [in InvertibleTyping]
_ ⊢## _ : _ [in InvertibleTyping]
_ ⟼* _ [in Reduction]
_ ⟼ _ [in Reduction]
_ ⟦ _ ⤳* _ ⟧ [in Lookup]
_ ⟦ _ ⤳ _ ⟧ [in Lookup]
_ ⊢! _ : _ ⪼ _ [in PreciseFlow]
_ ⊢!v _ : _ [in PreciseFlow]
_ ⊢# _ <: _ [in TightTyping]
_ ⊢# _ : _ [in TightTyping]
_ ⪯ _ [in Subenvironments]
_ ⊩ _ ⟿' _ ⬳ _ [in PreciseTyping]
_ ⊩ _ ⟿ _ ⬳ _ [in PreciseTyping]
_ ⊢ _ ⟿' _ [in PreciseTyping]
_ ⊢ _ ⟿ _ [in PreciseTyping]
_ ⊢!!! _ : _ [in PreciseTyping]
_ ⊢!! _ : _ [in PreciseTyping]
{ _ ⦂= _ } [in Definitions]
{ _ :=v _ } [in Definitions]
{ _ :=p _ } [in Definitions]
{ _ := _ } [in Definitions]
{ _ >: _ <: _ } [in Definitions]
{ _ ⦂ _ } [in Definitions]
{{ _ }} [in Definitions]
∀ ( _ ) _ [in Definitions]
⊤ [in Definitions]
⊥ [in Definitions]
λ ( _ ) _ [in Definitions]
μ _ [in Definitions]
ν ( _ ) _ [in Definitions]
Variable Index
C
CompilerExample.denotation [in CompilerExample]CompilerExample.dottyCore [in CompilerExample]
CompilerExample.DottyCore [in CompilerExample]
CompilerExample.srcPos [in CompilerExample]
CompilerExample.ST [in CompilerExample]
CompilerExample.symb [in CompilerExample]
CompilerExample.symbol [in CompilerExample]
CompilerExample.Symbol [in CompilerExample]
CompilerExample.symbols [in CompilerExample]
CompilerExample.tpe [in CompilerExample]
CompilerExample.Tpe [in CompilerExample]
CompilerExample.TS [in CompilerExample]
CompilerExample.TS' [in CompilerExample]
CompilerExample.typeRef [in CompilerExample]
CompilerExample.types [in CompilerExample]
L
ListExample.A [in ListExample]ListExample.Cons [in ListExample]
ListExample.head [in ListExample]
ListExample.HT [in ListExample]
ListExample.List [in ListExample]
ListExample.NC [in ListExample]
ListExample.Nil [in ListExample]
ListExample.tail [in ListExample]
S
SEQUENCES.A [in Sequences]SEQUENCES.R [in Sequences]
SEQUENCES.R_functional [in Sequences]
SingletonTypeExample.C [in SingletonTypeExample]
SingletonTypeExample.CD [in SingletonTypeExample]
SingletonTypeExample.d [in SingletonTypeExample]
SingletonTypeExample.D [in SingletonTypeExample]
SingletonTypeExample.decr [in SingletonTypeExample]
SingletonTypeExample.di [in SingletonTypeExample]
SingletonTypeExample.incr [in SingletonTypeExample]
Library Index
B
BindingC
CanonicalFormsCompilerExample
D
DefinitionsE
ExampleTacticsG
GeneralToTightI
InvertibleTypingL
ListExampleLookup
N
NarrowingP
PreciseFlowPreciseTyping
R
RecordAndInertTypesReduction
Replacement
ReplacementTyping
S
SafetySequences
SingletonTypeExample
Subenvironments
Substitution
T
TightTypingW
WeakeningLemma Index
A
app_sel_fields [in Binding]app_inv_right [in Binding]
B
binds_destruct [in Binding]binds_inert [in PreciseFlow]
C
canonical_forms_fun [in CanonicalForms]compiler_typecheck [in CompilerExample]
corresponding_types_fun [in CanonicalForms]
cycle_infseq [in Sequences]
D
defs_has_hasnt_neq [in Binding]defs_has_inv [in Binding]
defs_invert_trm [in RecordAndInertTypes]
defs_has_open' [in RecordAndInertTypes]
defs_has_open [in RecordAndInertTypes]
defs_typing_rhs [in Safety]
defs_typing_sngl_rhs [in Safety]
def_typing_rhs [in Safety]
E
env_ok_inv' [in Binding]env_ok_inv [in Binding]
extended_safety [in Safety]
extend_infseq [in Safety]
F
field_sel_nil [in Binding]field_sel_open [in Binding]
field_typing_comp2 [in PreciseTyping]
field_typing_comp1 [in PreciseTyping]
field_elim_q3 [in PreciseTyping]
field_elim_q2 [in PreciseTyping]
field_elim_q [in PreciseTyping]
field_elim_q0' [in PreciseTyping]
field_elim_q0 [in PreciseTyping]
finseq_unique [in Sequences]
fresh_subst_typ_dec [in Binding]
fv_ctx_types_push_eq [in Binding]
G
general_to_tight_typing [in GeneralToTight]general_to_tight [in GeneralToTight]
H
hasnt_notin [in RecordAndInertTypes]I
inert_prefix [in RecordAndInertTypes]inert_prefix_one [in RecordAndInertTypes]
inert_concat [in RecordAndInertTypes]
inert_record_has [in RecordAndInertTypes]
inert_ok [in PreciseFlow]
infseq_all_seq_inf [in Sequences]
infseq_finseq_excl [in Sequences]
infseq_star_inv [in Sequences]
infseq_or_finseq [in Sequences]
infseq_from_function [in Sequences]
infseq_if_all_seq_inf [in Sequences]
infseq_coinduction_principle_2 [in Sequences]
infseq_coinduction_principle [in Sequences]
invertible_typing_closure_tight_v [in ReplacementTyping]
invertible_andv [in ReplacementTyping]
invertible_to_precise_obj [in InvertibleTyping]
invertible_val_to_precise_lambda [in InvertibleTyping]
invertible_repl_closure_v [in InvertibleTyping]
invertible_repl_closure_v_helper [in InvertibleTyping]
invertible_repl_closure_comp_typed [in InvertibleTyping]
invertible_bnd [in InvertibleTyping]
invertible_and [in InvertibleTyping]
invertible_bot [in InvertibleTyping]
invertible_repl_closure [in InvertibleTyping]
invertible_repl_closure_helper [in InvertibleTyping]
invertible_to_precise_rcd [in InvertibleTyping]
invertible_to_precise_typ_all [in InvertibleTyping]
invert_fv_ctx_types_push [in Binding]
inv_sngl_trans [in ReplacementTyping]
inv_backtrack [in InvertibleTyping]
inv_to_prec [in InvertibleTyping]
inv_to_precise_sngl [in InvertibleTyping]
inv_to_precise_sngl_repl_comp [in InvertibleTyping]
L
last_field [in Binding]last_path [in PreciseTyping]
lfs_defs_typing [in Safety]
lft_typ_sngl_inv [in Safety]
lft_typ_all_inv [in Safety]
lft_unique [in Safety]
lft_inert [in Safety]
list_typing [in ListExample]
lookup_same_var_same_type [in CanonicalForms]
lookup_step_preservation_sngl_prec3 [in CanonicalForms]
lookup_preservation_forall [in CanonicalForms]
lookup_pres [in CanonicalForms]
lookup_step_pres [in CanonicalForms]
lookup_step_preservation_prec3_fun [in CanonicalForms]
lookup_step_preservation_inert_prec3 [in CanonicalForms]
lookup_step_preservation_prec2 [in CanonicalForms]
lookup_step_preservation_prec1 [in CanonicalForms]
lookup_weaken [in Lookup]
lookup_weaken_one [in Lookup]
lookup_step_weaken [in Lookup]
lookup_step_weaken_one [in Lookup]
lookup_func [in Lookup]
lookup_irred [in Lookup]
lookup_step_func [in Lookup]
lookup_val_inv [in Lookup]
lookup_strengthen [in Lookup]
lookup_strengthen_one [in Lookup]
lookup_empty [in Lookup]
M
map_lookup_extend [in Safety]map_red_extend [in Safety]
N
named_lookup_step [in Lookup]narrow_defs [in Narrowing]
narrow_subtyping [in Narrowing]
narrow_typing [in Narrowing]
narrow_rules [in Narrowing]
O
object_typing [in CanonicalForms]open_env_last_defs [in Binding]
open_env_rules [in Binding]
open_fresh_typ_dec_injective [in Binding]
open_fresh_path_injective [in Binding]
open_fresh_avar_injective [in Binding]
open_var_trm_eq [in Binding]
open_var_defs_eq [in Binding]
open_var_trm_val_def_eq [in Binding]
open_var_typ_eq [in Binding]
open_var_typ_dec_eq [in Binding]
open_var_path_eq [in Binding]
open_named_path [in Binding]
open_record_type_p [in RecordAndInertTypes]
open_record_typ_p [in RecordAndInertTypes]
open_record_p [in RecordAndInertTypes]
open_dec_preserves_label_p [in RecordAndInertTypes]
open_dec_preserves_label [in RecordAndInertTypes]
open_typ_subst [in Substitution]
P
path_sel_repl_inv_v [in ReplacementTyping]path_sel_repl_v [in ReplacementTyping]
path_sel_repl2_v [in ReplacementTyping]
path_elim_repl [in ReplacementTyping]
path_sel_repl_inv [in ReplacementTyping]
path_sel_repl [in ReplacementTyping]
path_sel_repl2 [in ReplacementTyping]
path_sel_inv_v [in InvertibleTyping]
path_sel_inv [in InvertibleTyping]
path_elim_prec [in PreciseTyping]
path_typ_all_to_precise [in GeneralToTight]
path_safety [in Safety]
pfv_inert [in PreciseFlow]
pf_sngl_sel_unique [in PreciseFlow]
pf_sngl_flds_elim [in PreciseFlow]
pf_sngl_fld_elim [in PreciseFlow]
pf_weaken [in PreciseFlow]
pf_weaken_one [in PreciseFlow]
pf_sngl [in PreciseFlow]
pf_path_sel [in PreciseFlow]
pf_strengthen [in PreciseFlow]
pf_dec_typ_tight [in PreciseFlow]
pf_T_unique [in PreciseFlow]
pf_dec_typ_unique [in PreciseFlow]
pf_record_has_U [in PreciseFlow]
pf_record_has_T [in PreciseFlow]
pf_psel [in PreciseFlow]
pf_bot [in PreciseFlow]
pf_binds [in PreciseFlow]
pf_forall_T [in PreciseFlow]
pf_bnd_T2 [in PreciseFlow]
pf_sngl_T [in PreciseFlow]
pf_bnd_T [in PreciseFlow]
pf_sngl_U [in PreciseFlow]
pf_rec_rcd_U [in PreciseFlow]
pf_rcd_T [in PreciseFlow]
pf_inert [in PreciseFlow]
pf_inertsngl [in PreciseFlow]
pf_forall_U [in PreciseFlow]
pf_strengthen_from_pt3 [in PreciseTyping]
pf_strengthen_one_helper [in PreciseTyping]
pf_inert_pt3_sngl_false [in PreciseTyping]
pf_inert_pt2_sngl_false [in PreciseTyping]
pf_pt3_unique [in PreciseTyping]
pf_pt3_trans_inv_mult' [in PreciseTyping]
pf_pt3_trans_inv_mult [in PreciseTyping]
pf_pt2_trans_inv_mult [in PreciseTyping]
pf_strengthen_full [in PreciseTyping]
pf_pt2_sngl_invert [in PreciseTyping]
pf_pt2_sngl [in PreciseTyping]
pf_pt2 [in PreciseTyping]
pf_sngl_to_lft [in Safety]
plus_right [in Sequences]
plus_star_trans [in Sequences]
plus_star [in Sequences]
plus_one [in Sequences]
precise_to_general_v [in PreciseFlow]
precise_to_general [in PreciseFlow]
precise_to_general_h [in PreciseFlow]
precise_to_general3 [in PreciseTyping]
precise_to_general2 [in PreciseTyping]
preservation [in Safety]
prev_var_exists [in CanonicalForms]
progress [in Safety]
proj_rewrite' [in Binding]
proj_rewrite_mult [in Binding]
proj_rewrite [in Binding]
pt2_strengthen_from_pf [in PreciseTyping]
pt2_strengthen_full [in PreciseTyping]
pt2_strengthen [in PreciseTyping]
pt2_fld_strengthen [in PreciseTyping]
pt2_strengthen_one [in PreciseTyping]
pt2_strengthen_one_helper [in PreciseTyping]
pt2_qbs_typed [in PreciseTyping]
pt2_dec_typ_tight [in PreciseTyping]
pt2_exists [in PreciseTyping]
pt2_bnd [in PreciseTyping]
pt2_to_pf [in PreciseTyping]
pt2_var_sngl [in PreciseTyping]
pt2_destruct_env [in PreciseTyping]
pt2_weaken [in PreciseTyping]
pt2_weaken_one [in PreciseTyping]
pt2_backtrack [in PreciseTyping]
pt2_sngl_unique' [in PreciseTyping]
pt2_sngl_unique [in PreciseTyping]
pt2_sngl_exists [in PreciseTyping]
pt2_psel [in PreciseTyping]
pt2_inertsngl [in PreciseTyping]
pt2_and_destruct2 [in PreciseTyping]
pt2_and_destruct1 [in PreciseTyping]
pt23_invert [in PreciseTyping]
pt3_fld_strengthen [in PreciseTyping]
pt3_strengthen_full [in PreciseTyping]
pt3_strengthen [in PreciseTyping]
pt3_strengthen_one [in PreciseTyping]
pt3_dec_typ_tight [in PreciseTyping]
pt3_inert_sngl_invert [in PreciseTyping]
pt3_inert_pt2_sngl_invert [in PreciseTyping]
pt3_var_sngl [in PreciseTyping]
pt3_invert [in PreciseTyping]
pt3_bnd [in PreciseTyping]
pt3_trans_trans [in PreciseTyping]
pt3_weaken [in PreciseTyping]
pt3_weaken_one [in PreciseTyping]
pt3_field_trans' [in PreciseTyping]
pt3_field_trans [in PreciseTyping]
pt3_sngl_trans3 [in PreciseTyping]
pt3_backtrack [in PreciseTyping]
pt3_field_elim_p [in PreciseTyping]
pt3_field_elim [in PreciseTyping]
pt3_trans2 [in PreciseTyping]
pt3_trans [in PreciseTyping]
pt3_psel [in PreciseTyping]
pt3_inertsngl [in PreciseTyping]
pt3_and_destruct2 [in PreciseTyping]
pt3_and_destruct1 [in PreciseTyping]
pt3_exists [in GeneralToTight]
R
record_has_ty_defs [in Binding]record_typ_has_label_in [in RecordAndInertTypes]
record_open_tight [in RecordAndInertTypes]
record_open [in RecordAndInertTypes]
rename_defs [in Substitution]
rename_def_defs [in Substitution]
rename_ty_trm [in Substitution]
replacement_closure_v [in ReplacementTyping]
replacement_repl_closure_pq3_v [in ReplacementTyping]
replacement_repl_closure_pq2_v [in ReplacementTyping]
replacement_repl_closure_pq_v [in ReplacementTyping]
replacement_repl_closure_qp3_v [in ReplacementTyping]
replacement_repl_closure_qp2_v [in ReplacementTyping]
replacement_repl_closure_qp_v [in ReplacementTyping]
replacement_closure [in ReplacementTyping]
replacement_repl_closure_comp_typed [in ReplacementTyping]
replacement_subtyping_closure [in ReplacementTyping]
replacement_repl_closure_pq_comp [in ReplacementTyping]
replacement_repl_closure_pq3 [in ReplacementTyping]
replacement_repl_closure_pq2 [in ReplacementTyping]
replacement_repl_closure_pq [in ReplacementTyping]
replacement_repl_closure_pq_helper [in ReplacementTyping]
replacement_repl_closure_pq_helper_mutind [in ReplacementTyping]
replacement_repl_closure_qp_comp [in ReplacementTyping]
replacement_repl_closure_qp3 [in ReplacementTyping]
replacement_repl_closure_qp2 [in ReplacementTyping]
replacement_repl_closure_qp [in ReplacementTyping]
repl_to_invertible_obj [in ReplacementTyping]
repl_andv [in ReplacementTyping]
repl_sngl_trans [in ReplacementTyping]
repl_to_invertible_sngl [in ReplacementTyping]
repl_to_invertible_sngl_repl_comp [in ReplacementTyping]
repl_fld [in ReplacementTyping]
repl_prec_exists [in ReplacementTyping]
repl_top [in ReplacementTyping]
repl_to_inv [in ReplacementTyping]
repl_rec_intro [in ReplacementTyping]
repl_and [in ReplacementTyping]
repl_to_precise_rcd [in ReplacementTyping]
repl_to_precise_typ_all [in ReplacementTyping]
repl_typ_subst [in Replacement]
repl_typ_subst_mutind [in Replacement]
repl_prefixes_sel [in Replacement]
repl_prefixes_sngl [in Replacement]
repl_field_elim [in Replacement]
repl_field_elim_mutind [in Replacement]
repl_insert [in Replacement]
repl_insert_mutind [in Replacement]
repl_comp_open [in Replacement]
repl_comp_open_rec [in Replacement]
repl_star_trm [in Replacement]
repl_star_typ2 [in Replacement]
repl_star_typ1 [in Replacement]
repl_star_all2 [in Replacement]
repl_star_all1 [in Replacement]
repl_star_bnd [in Replacement]
repl_star_and2 [in Replacement]
repl_star_and1 [in Replacement]
repl_star_rcd [in Replacement]
repl_open_var [in Replacement]
repl_open [in Replacement]
repl_open_rec [in Replacement]
repl_intro_sngl [in Replacement]
repl_swap [in Replacement]
repl_composition_sub [in InvertibleTyping]
repl_sub [in InvertibleTyping]
repl_composition_fld_elim [in PreciseTyping]
repl_comp_trans_record_has [in PreciseTyping]
repl_comp_trans_open [in PreciseTyping]
repl_composition_weaken [in PreciseTyping]
repl_composition_weaken_one [in PreciseTyping]
repl_composition_open [in PreciseTyping]
repl_comp_record_has1 [in PreciseTyping]
repl_comp_record_has2 [in PreciseTyping]
repl_comp_typ_and2 [in PreciseTyping]
repl_comp_typ_and1 [in PreciseTyping]
repl_comp_trm_rcd' [in PreciseTyping]
repl_comp_trm_rcd [in PreciseTyping]
repl_comp_bnd' [in PreciseTyping]
repl_comp_bnd_inv2 [in PreciseTyping]
repl_comp_bnd_inv1 [in PreciseTyping]
repl_comp_sngl_inv2 [in PreciseTyping]
repl_comp_sngl_inv1 [in PreciseTyping]
repl_comp_to_prec' [in PreciseTyping]
S
safety [in Safety]safety_helper [in Safety]
sel_sub_fields [in Binding]
sel_fields_equal [in Binding]
sel_field_to_fields [in Binding]
sel_fields_subst [in Binding]
sel_fields_open [in Binding]
sel_fieldss_subst [in Replacement]
sel_replacement [in GeneralToTight]
sngl_path_lookup [in CanonicalForms]
sngl_typed3 [in PreciseTyping]
sngl_typed2 [in PreciseTyping]
sngl_typed [in PreciseTyping]
sngl_replacement [in GeneralToTight]
star_star_inv [in Sequences]
star_plus_trans [in Sequences]
star_trans [in Sequences]
star_one [in Sequences]
subenv_implies_ok [in Subenvironments]
subenv_last [in Subenvironments]
subenv_extend [in Subenvironments]
subenv_refl [in Subenvironments]
subst_defs_hasnt_label [in Binding]
subst_defs_hasnt [in Binding]
subst_label_of_def [in Binding]
subst_intro_defs [in Binding]
subst_intro_typ [in Binding]
subst_intro_trm [in Binding]
subst_open_commut_defs_p [in Binding]
subst_open_commut_trm_p [in Binding]
subst_open_commut_trm_val_def_defs_p [in Binding]
subst_open_commut_typ_p [in Binding]
subst_open_commut_typ_dec_p [in Binding]
subst_open_commut_path_p [in Binding]
subst_open_commut_defs [in Binding]
subst_open_commut_trm [in Binding]
subst_open_commut_trm_val_def_defs [in Binding]
subst_open_commut_typ [in Binding]
subst_open_commut_typ_dec [in Binding]
subst_open_commut_path [in Binding]
subst_open_commut_avar [in Binding]
subst_fresh_ctx [in Binding]
subst_fresh_trm_val_def_defs [in Binding]
subst_fresh_typ_dec [in Binding]
subst_fresh_path [in Binding]
subst_fresh_var_path [in Substitution]
subst_var_path [in Substitution]
subst_ty_trm [in Substitution]
subst_rules [in Substitution]
T
tight_bounds_subst [in Substitution]tight_bounds_subst_mut [in Substitution]
tight_to_general [in TightTyping]
tight_to_prec_exists [in GeneralToTight]
typecheck [in SingletonTypeExample]
typed_path_lookup3 [in CanonicalForms]
typed_path_lookup_helper [in CanonicalForms]
typed_path_lookup_same_var3 [in CanonicalForms]
typed_path_lookup_same_var2 [in CanonicalForms]
typed_paths_named [in Binding]
typing_empty_false [in Binding]
typing_implies_bound [in Binding]
typ_to_lookup3 [in CanonicalForms]
typ_to_lookup2 [in CanonicalForms]
typ_to_lookup1 [in CanonicalForms]
ty_defs_record_type [in RecordAndInertTypes]
ty_defs_record_type_helper [in RecordAndInertTypes]
U
unique_rcd_trm [in RecordAndInertTypes]unique_rcd_typ [in RecordAndInertTypes]
V
val_typ_all_to_lambda [in GeneralToTight]val_typing [in Safety]
W
weaken_ty_defs [in Weakening]weaken_subtyp [in Weakening]
weaken_ty_trm [in Weakening]
weaken_rules [in Weakening]
well_typed_notin_dom [in Binding]
well_typed_to_ok_G [in Binding]
wf_prefix [in PreciseTyping]
wf_prefix_one [in PreciseTyping]
wt_to_ok_γ [in Binding]
wt_prefix [in Binding]
Constructor Index
A
avar_f [in Definitions]avar_b [in Definitions]
D
dec_trm [in Definitions]dec_typ [in Definitions]
defp [in Definitions]
defs_cons [in Definitions]
defs_nil [in Definitions]
defv [in Definitions]
def_trm [in Definitions]
def_typ [in Definitions]
E
er_lookup [in Safety]er_red [in Safety]
I
inert_push [in Definitions]inert_empty [in Definitions]
inert_typ_bnd [in Definitions]
inert_typ_all [in Definitions]
infseq_step [in Sequences]
L
label_trm [in Definitions]label_typ [in Definitions]
lft_cons [in Safety]
lft_empty [in Safety]
lookup_sel_v [in Lookup]
lookup_sel_p [in Lookup]
lookup_var [in Lookup]
N
nf_val [in Reduction]nf_path [in Reduction]
P
pf_and2 [in PreciseFlow]pf_and1 [in PreciseFlow]
pf_open [in PreciseFlow]
pf_fld [in PreciseFlow]
pf_bind [in PreciseFlow]
plus_left [in Sequences]
pt2 [in PreciseTyping]
pt2_sngl_trans [in PreciseTyping]
pt3 [in PreciseTyping]
pt3_sngl_trans [in PreciseTyping]
p_sel [in Definitions]
R
rall1 [in Definitions]rall2 [in Definitions]
rand1 [in Definitions]
rand2 [in Definitions]
rbnd [in Definitions]
rdtrm [in Definitions]
rdtyp1 [in Definitions]
rdtyp2 [in Definitions]
rd_trm_sngl [in Definitions]
rd_trm [in Definitions]
rd_typ [in Definitions]
red_let_tgt [in Reduction]
red_let_path [in Reduction]
red_let_val [in Reduction]
red_app [in Reduction]
rh_andr [in Definitions]
rh_andl [in Definitions]
rh_one [in Definitions]
rpath [in Definitions]
rrcd [in Definitions]
rsngl [in Definitions]
rt_cons [in Definitions]
rt_one [in Definitions]
S
star_step [in Sequences]star_refl [in Sequences]
subenv_push [in Subenvironments]
subenv_empty [in Subenvironments]
subtyp_all [in Definitions]
subtyp_sel1 [in Definitions]
subtyp_sel2 [in Definitions]
subtyp_sngl_qp [in Definitions]
subtyp_sngl_pq [in Definitions]
subtyp_typ [in Definitions]
subtyp_fld [in Definitions]
subtyp_and2 [in Definitions]
subtyp_and12 [in Definitions]
subtyp_and11 [in Definitions]
subtyp_trans [in Definitions]
subtyp_refl [in Definitions]
subtyp_bot [in Definitions]
subtyp_top [in Definitions]
subtyp_all_t [in TightTyping]
subtyp_sel1_t [in TightTyping]
subtyp_sel2_t [in TightTyping]
subtyp_sngl_qp_t [in TightTyping]
subtyp_sngl_pq_t [in TightTyping]
subtyp_typ_t [in TightTyping]
subtyp_fld_t [in TightTyping]
subtyp_and2_t [in TightTyping]
subtyp_and12_t [in TightTyping]
subtyp_and11_t [in TightTyping]
subtyp_trans_t [in TightTyping]
subtyp_refl_t [in TightTyping]
subtyp_bot_t [in TightTyping]
subtyp_top_t [in TightTyping]
T
trm_path [in Definitions]trm_let [in Definitions]
trm_app [in Definitions]
trm_val [in Definitions]
typ_sngl [in Definitions]
typ_all [in Definitions]
typ_bnd [in Definitions]
typ_path [in Definitions]
typ_and [in Definitions]
typ_rcd [in Definitions]
typ_bot [in Definitions]
typ_top [in Definitions]
ty_sel_qp_rv [in ReplacementTyping]
ty_rec_qp_rv [in ReplacementTyping]
ty_sel_rv [in ReplacementTyping]
ty_and_rv [in ReplacementTyping]
ty_inv_rv [in ReplacementTyping]
ty_sngl_qp_r [in ReplacementTyping]
ty_sel_qp_r [in ReplacementTyping]
ty_rec_qp_r [in ReplacementTyping]
ty_rcd_intro_r [in ReplacementTyping]
ty_sel_r [in ReplacementTyping]
ty_bnd_r [in ReplacementTyping]
ty_and_r [in ReplacementTyping]
ty_inv_r [in ReplacementTyping]
ty_defs_cons [in Definitions]
ty_defs_one [in Definitions]
ty_def_path [in Definitions]
ty_def_new [in Definitions]
ty_def_all [in Definitions]
ty_def_typ [in Definitions]
ty_sub [in Definitions]
ty_and_intro [in Definitions]
ty_rec_elim [in Definitions]
ty_rec_intro [in Definitions]
ty_path_elim [in Definitions]
ty_sngl [in Definitions]
ty_let [in Definitions]
ty_rcd_intro [in Definitions]
ty_new_elim [in Definitions]
ty_new_intro [in Definitions]
ty_all_elim [in Definitions]
ty_all_intro [in Definitions]
ty_var [in Definitions]
ty_rec_pq_invv [in InvertibleTyping]
ty_top_invv [in InvertibleTyping]
ty_and_invv [in InvertibleTyping]
ty_all_invv [in InvertibleTyping]
ty_precise_invv [in InvertibleTyping]
ty_sngl_pq_inv [in InvertibleTyping]
ty_sel_pq_inv [in InvertibleTyping]
ty_rec_pq_inv [in InvertibleTyping]
ty_top_inv [in InvertibleTyping]
ty_and_inv [in InvertibleTyping]
ty_all_inv [in InvertibleTyping]
ty_dec_typ_inv [in InvertibleTyping]
ty_dec_trm_inv [in InvertibleTyping]
ty_precise_inv [in InvertibleTyping]
ty_new_intro_p [in PreciseFlow]
ty_all_intro_p [in PreciseFlow]
ty_sub_t [in TightTyping]
ty_and_intro_t [in TightTyping]
ty_rec_elim_t [in TightTyping]
ty_rcd_intro_t [in TightTyping]
ty_path_elim_t [in TightTyping]
ty_sngl_t [in TightTyping]
ty_let_t [in TightTyping]
ty_rec_intro_t [in TightTyping]
ty_new_elim_t [in TightTyping]
ty_new_intro_t [in TightTyping]
ty_all_elim_t [in TightTyping]
ty_all_intro_t [in TightTyping]
ty_var_t [in TightTyping]
V
val_lambda [in Definitions]val_new [in Definitions]
W
well_typed_push [in Definitions]well_typed_empty [in Definitions]
wfe_push [in PreciseTyping]
wfe_empty [in PreciseTyping]
Axiom Index
T
trm_label [in Definitions]typ_label [in Definitions]
Inductive Index
A
avar [in Definitions]D
dec [in Definitions]def [in Definitions]
defs [in Definitions]
def_rhs [in Definitions]
E
extended_red [in Safety]I
inert [in Definitions]inert_typ [in Definitions]
infseq [in Sequences]
L
label [in Definitions]lookup_step [in Lookup]
lookup_fields_typ [in Safety]
N
norm_form [in Reduction]P
path [in Definitions]plus [in Sequences]
precise_flow [in PreciseFlow]
precise_typing3 [in PreciseTyping]
precise_typing2 [in PreciseTyping]
R
record_has [in Definitions]record_typ [in Definitions]
record_dec [in Definitions]
red [in Reduction]
repl_dec [in Definitions]
repl_typ [in Definitions]
S
star [in Sequences]subenv [in Subenvironments]
subtyp [in Definitions]
subtyp_t [in TightTyping]
T
trm [in Definitions]typ [in Definitions]
ty_replv [in ReplacementTyping]
ty_repl [in ReplacementTyping]
ty_defs [in Definitions]
ty_def [in Definitions]
ty_trm [in Definitions]
ty_val_inv [in InvertibleTyping]
ty_path_inv [in InvertibleTyping]
ty_val_p [in PreciseFlow]
ty_trm_t [in TightTyping]
V
val [in Definitions]W
well_typed [in Definitions]wf [in PreciseTyping]
Section Index
C
CompilerExample [in CompilerExample]E
ExtendedSafety [in Safety]L
ListExample [in ListExample]P
PathSafety [in Safety]S
Safety [in Safety]SEQUENCES [in Sequences]
SingletonTypeExample [in SingletonTypeExample]
Abbreviation Index
D
DottyCoreAbstract [in CompilerExample]DottyCorePackage [in CompilerExample]
DottyCoreTight [in CompilerExample]
I
Id [in ExampleTactics]id [in ExampleTactics]
L
Lazy [in ExampleTactics]lazy [in ExampleTactics]
let_trm [in ExampleTactics]
ListObjType [in ListExample]
ListType [in ListExample]
ListTypeA [in ListExample]
P
path_ref [in ExampleTactics]pvar [in Definitions]
R
repl_repeat_dec [in Replacement]repl_repeat_typ [in Replacement]
S
sssssuper [in ExampleTactics]ssssuper [in ExampleTactics]
sssuper [in ExampleTactics]
ssuper [in ExampleTactics]
super [in ExampleTactics]
SymbolImpl [in CompilerExample]
symbolsType [in CompilerExample]
T
T [in CompilerExample]T [in SingletonTypeExample]
t [in SingletonTypeExample]
this [in ExampleTactics]
TpeImpl [in CompilerExample]
tvar [in Definitions]
typesType [in CompilerExample]
Definition Index
A
all_seq_inf [in Sequences]C
ctx [in Definitions]cyclic_path [in Safety]
D
dec_mut [in Definitions]defrhs_mut [in Definitions]
defs_mut [in Definitions]
defs_hasnt [in Definitions]
defs_has [in Definitions]
deftrm [in CanonicalForms]
def_mut [in Definitions]
diverges [in Safety]
diverges' [in Safety]
F
fields [in Definitions]fv_sta_vals [in Definitions]
fv_ctx_types [in Definitions]
fv_defrhs [in Definitions]
fv_defs [in Definitions]
fv_def [in Definitions]
fv_val [in Definitions]
fv_trm [in Definitions]
fv_dec [in Definitions]
fv_typ [in Definitions]
fv_path [in Definitions]
fv_avar [in Definitions]
G
get_def [in Definitions]I
inert_sngl [in RecordAndInertTypes]inert_mut [in Definitions]
infseq_with_function [in Sequences]
irred [in Sequences]
is_sngl [in RecordAndInertTypes]
L
label_of_dec [in Definitions]label_of_def [in Definitions]
N
named_path [in Binding]O
open_defrhs_p [in Definitions]open_defs_p [in Definitions]
open_def_p [in Definitions]
open_val_p [in Definitions]
open_trm_p [in Definitions]
open_path_p [in Definitions]
open_dec_p [in Definitions]
open_typ_p [in Definitions]
open_avar_p [in Definitions]
open_rec_defrhs_p [in Definitions]
open_rec_defs_p [in Definitions]
open_rec_def_p [in Definitions]
open_rec_val_p [in Definitions]
open_rec_trm_p [in Definitions]
open_rec_dec_p [in Definitions]
open_rec_typ_p [in Definitions]
open_rec_path_p [in Definitions]
open_rec_avar_p [in Definitions]
open_paths [in Definitions]
open_path [in Definitions]
open_defrhsdd [in Definitions]
open_defs [in Definitions]
open_def [in Definitions]
open_val [in Definitions]
open_trm [in Definitions]
open_dec [in Definitions]
open_typ [in Definitions]
open_avar [in Definitions]
open_rec_defrhs [in Definitions]
open_rec_defs [in Definitions]
open_rec_def [in Definitions]
open_rec_val [in Definitions]
open_rec_trm [in Definitions]
open_rec_dec [in Definitions]
open_rec_typ [in Definitions]
open_rec_path [in Definitions]
open_rec_avar [in Definitions]
R
rcd_mutind [in Definitions]rcd_typ_mut [in Definitions]
rcd_dec_mut [in Definitions]
record_type [in Definitions]
repl_mutind [in Definitions]
repl_dec_mut [in Definitions]
repl_typ_mut [in Definitions]
repl_composition_qp [in PreciseTyping]
rules_mutind [in Definitions]
rules_subtyp [in Definitions]
rules_defs_mut [in Definitions]
rules_def_mut [in Definitions]
rules_trm_mut [in Definitions]
S
sel_fields [in Definitions]sel_field [in Definitions]
sta [in Definitions]
subst_fresh_typ [in Binding]
subst_ctx [in Binding]
subst_defrhs [in Binding]
subst_defs [in Binding]
subst_def [in Binding]
subst_val [in Binding]
subst_trm [in Binding]
subst_dec [in Binding]
subst_typ [in Binding]
subst_path [in Binding]
subst_avar [in Binding]
subst_var_p [in Binding]
subst_var [in Binding]
T
t [in CompilerExample]t [in ListExample]
tds_mutind [in Definitions]
tds_subtyp [in Definitions]
tds_ty_defs_mut [in Definitions]
tds_ty_def_mut [in Definitions]
tds_ty_trm_mut [in Definitions]
tight_bounds_dec [in Definitions]
tight_bounds [in Definitions]
trm_mutind [in Definitions]
trm_mut [in Definitions]
ts_mutind [in Definitions]
ts_subtyp [in Definitions]
ts_ty_trm_mut [in Definitions]
ts_mutind_ts [in TightTyping]
ts_subtyp_ts [in TightTyping]
ts_ty_trm_mut_ts [in TightTyping]
typed_repl_comp_qp [in PreciseTyping]
typ_mutind [in Definitions]
typ_mut [in Definitions]
ty_def_mutind [in Definitions]
ty_defs_mut' [in Definitions]
ty_def_mut' [in Definitions]
ty_mutind [in Definitions]
ty_defs_mut [in Definitions]
ty_def_mut [in Definitions]
ty_trm_mut [in Definitions]
V
val_mut [in Definitions]| 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 | (882 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 | (45 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 | (33 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 | (23 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 | (403 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 | (171 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 | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 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 | (7 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 | (29 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 | (127 entries) |