| 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 | (580 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 | (2 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 | (9 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 | (32 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 | (246 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 | (118 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| 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 | (1 entry) |
| 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 | (160 entries) |
Global Index
A
abstract_term_var_cancel [lemma, in RefinementTypes.SubstLemmas]abstract_term_var [definition, in RefinementTypes.Subst]
AccTy [definition, in RefinementTypes.Examples]
Adequacy [library]
AlgorithmicTyping [library]
avoid [definition, in RefinementTypes.Avoid]
Avoid [library]
AvoidLemmas [library]
avoid_subst_shift_id [lemma, in RefinementTypes.AvoidLemmas]
avoid_subst_shift_id_gen [lemma, in RefinementTypes.AvoidLemmas]
avoid_not_mentions [lemma, in RefinementTypes.AvoidLemmas]
avoid_var0 [definition, in RefinementTypes.Avoid]
B
base_ty [definition, in RefinementTypes.FirstOrder]BinOp [inductive, in RefinementTypes.Syntax]
BinOp_sind [definition, in RefinementTypes.Syntax]
BinOp_rec [definition, in RefinementTypes.Syntax]
BinOp_ind [definition, in RefinementTypes.Syntax]
BinOp_rect [definition, in RefinementTypes.Syntax]
bin_op_val_pair_compat [definition, in RefinementTypes.Eval]
bin_op_result_ty [definition, in RefinementTypes.FirstOrder]
bin_op_ty_compat [definition, in RefinementTypes.FirstOrder]
bin_op_ty_interp_val_pair_compat [lemma, in RefinementTypes.FirstOrderLemmas]
bin_op_eq_dec [lemma, in RefinementTypes.Syntax]
bool_ty [definition, in RefinementTypes.FirstOrder]
bool_ty_interp_pair_compat [lemma, in RefinementTypes.FirstOrderLemmas]
bot_eq_refine_false [lemma, in RefinementTypes.ExamplesPartialSoundness]
C
collect_tm [definition, in RefinementTypes.ExamplesCollect]collect_ty [definition, in RefinementTypes.ExamplesCollect]
D
diverge_and_false_not_implies_false [lemma, in RefinementTypes.ExamplesPartialSoundness]diverge_and_false_not_sub_false [lemma, in RefinementTypes.ExamplesPartialSoundness]
diverge_not_sub_false [lemma, in RefinementTypes.ExamplesPartialSoundness]
E
env_subst_compat_cons [lemma, in RefinementTypes.EvalSubstLemmas]env_subst_compat_sind [definition, in RefinementTypes.EvalSubstLemmas]
env_subst_compat_ind [definition, in RefinementTypes.EvalSubstLemmas]
env_subst_compat [inductive, in RefinementTypes.EvalSubstLemmas]
env_incr_wf [lemma, in RefinementTypes.WfLemmas]
erase_ty_in_tm_subst [lemma, in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm_subst_gen [lemma, in RefinementTypes.EvalTypeErasure]
erase_ty_in_val_vbool_true [lemma, in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm_ren [lemma, in RefinementTypes.EvalTypeErasure]
erase_ty_in_val [definition, in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm [definition, in RefinementTypes.EvalTypeErasure]
esc_subst [constructor, in RefinementTypes.EvalSubstLemmas]
esc_id [constructor, in RefinementTypes.EvalSubstLemmas]
eval [definition, in RefinementTypes.Eval]
Eval [library]
EvalLemmas [library]
EvalShiftLemmas [library]
EvalSubstLemmas [library]
evals_to_same [definition, in RefinementTypes.Wf]
EvalTypeErasure [library]
eval_and_bool [lemma, in RefinementTypes.ExamplesPartialSoundness]
eval_tdiverge [lemma, in RefinementTypes.ExamplesPartialSoundness]
eval_to_true_subst_env [lemma, in RefinementTypes.InterpSubstLemmas]
eval_bin_op [definition, in RefinementTypes.Eval]
eval_erase_ty [lemma, in RefinementTypes.EvalTypeErasure]
eval_to_true_shift_env [lemma, in RefinementTypes.InterpShiftLemmas]
eval_to_true_subst_ty_gen [lemma, in RefinementTypes.InterpShiftLemmas]
eval_to_true_subst_ty [lemma, in RefinementTypes.InterpShiftLemmas]
eval_to_true_ren_ty [lemma, in RefinementTypes.InterpShiftLemmas]
eval_to_true_erase_eq [lemma, in RefinementTypes.InterpShiftLemmas]
eval_shift_env_bwd [lemma, in RefinementTypes.EvalShiftLemmas]
eval_shift_env_fwd [lemma, in RefinementTypes.EvalShiftLemmas]
eval_weaken_compat [lemma, in RefinementTypes.EvalShiftLemmas]
eval_bin_op_val_weaken_compat [lemma, in RefinementTypes.EvalShiftLemmas]
eval_bin_op_result_in_interp [lemma, in RefinementTypes.FirstOrderLemmas]
eval_subst_env_bwd [lemma, in RefinementTypes.EvalSubstLemmas]
eval_subst_env_fwd [lemma, in RefinementTypes.EvalSubstLemmas]
eval_term_subst_compat_bwd [lemma, in RefinementTypes.EvalSubstLemmas]
eval_term_subst_compat_fwd [lemma, in RefinementTypes.EvalSubstLemmas]
eval_bin_op_val_subst_compat [lemma, in RefinementTypes.EvalSubstLemmas]
eval_bin_op_defined [lemma, in RefinementTypes.EvalLemmas]
eval_bin_op_eq_refl [lemma, in RefinementTypes.EvalLemmas]
eval_bin_op_eq_fo_defined [lemma, in RefinementTypes.EvalLemmas]
eval_tbin_op [lemma, in RefinementTypes.EvalLemmas]
eval_fuel_mono [lemma, in RefinementTypes.EvalLemmas]
eval_to_true [definition, in RefinementTypes.Interp]
eval_false_not_true [lemma, in RefinementTypes.AvoidLemmas]
Examples [library]
ExamplesCollect [library]
ExamplesPartialSoundness [library]
F
FirstOrder [library]FirstOrderLemmas [library]
flip_polarity [definition, in RefinementTypes.Avoid]
fo [definition, in RefinementTypes.FirstOrder]
Forall_Forall2_refl [lemma, in RefinementTypes.ListLemmas]
Forall2_refl [lemma, in RefinementTypes.ListLemmas]
Forall2_exists2_r [lemma, in RefinementTypes.ListLemmas]
Forall2_exists2 [lemma, in RefinementTypes.ListLemmas]
fo_val [definition, in RefinementTypes.Eval]
fo_interp_is_fo_val [lemma, in RefinementTypes.FirstOrderLemmas]
full_safety [lemma, in RefinementTypes.AlgorithmicTyping]
funcomp [definition, in RefinementTypes.Subst]
I
interp [definition, in RefinementTypes.Interp]Interp [library]
InterpShiftLemmas [library]
InterpSubstLemmas [library]
interp_subst [lemma, in RefinementTypes.InterpSubstLemmas]
interp_subst_gen [lemma, in RefinementTypes.InterpSubstLemmas]
interp_weaken_both [lemma, in RefinementTypes.InterpSubstLemmas]
interp_subst_term [lemma, in RefinementTypes.InterpSubstLemmas]
interp_subst_up_term [lemma, in RefinementTypes.InterpSubstLemmas]
interp_env_ren_type [lemma, in RefinementTypes.InterpShiftLemmas]
interp_weaken_type [lemma, in RefinementTypes.InterpShiftLemmas]
interp_env_ren_term [lemma, in RefinementTypes.InterpShiftLemmas]
interp_weaken_term [lemma, in RefinementTypes.InterpShiftLemmas]
interp_mu_eq_ext [lemma, in RefinementTypes.Interp]
interp_mu [definition, in RefinementTypes.Interp]
interp_bot [definition, in RefinementTypes.Interp]
interp_top [definition, in RefinementTypes.Interp]
interp_and [definition, in RefinementTypes.Interp]
interp_or [definition, in RefinementTypes.Interp]
interp_sum [definition, in RefinementTypes.Interp]
interp_sigma [definition, in RefinementTypes.Interp]
interp_refine [definition, in RefinementTypes.Interp]
interp_forall [definition, in RefinementTypes.Interp]
interp_fun [definition, in RefinementTypes.Interp]
interp_int32 [definition, in RefinementTypes.Interp]
interp_bool [definition, in RefinementTypes.Interp]
interp_unit [definition, in RefinementTypes.Interp]
interp_var [definition, in RefinementTypes.Interp]
interp_shift_type_by [lemma, in RefinementTypes.WfLemmas]
interp_env_shift_term [lemma, in RefinementTypes.WfLemmas]
interp_mu_mono [lemma, in RefinementTypes.PositivityLemmas]
interp_spos_distribute [lemma, in RefinementTypes.PositivityLemmas]
interp_spos_mono [lemma, in RefinementTypes.PositivityLemmas]
interp_ty_var_absent [lemma, in RefinementTypes.PositivityLemmas]
interp_avoid_shift [lemma, in RefinementTypes.AvoidLemmas]
interp_avoid_var0 [lemma, in RefinementTypes.AvoidLemmas]
interp_avoid_neg [lemma, in RefinementTypes.AvoidLemmas]
interp_avoid_pos [lemma, in RefinementTypes.AvoidLemmas]
interp_avoid_pos_neg [lemma, in RefinementTypes.AvoidLemmas]
int_le [definition, in RefinementTypes.Examples]
int32_wrap [definition, in RefinementTypes.Eval]
is_positive [definition, in RefinementTypes.ExamplesCollect]
iter_up_tm [lemma, in RefinementTypes.SubstLemmas]
L
ListLemmas [library]ListTy [definition, in RefinementTypes.ExamplesCollect]
ListTy [definition, in RefinementTypes.Examples]
ListTy_refined [definition, in RefinementTypes.ExamplesCollect]
ListTy_unfolded [definition, in RefinementTypes.Examples]
list_value [definition, in RefinementTypes.ExamplesCollect]
list_term [definition, in RefinementTypes.ExamplesCollect]
list_unfold_sub [lemma, in RefinementTypes.Examples]
list_term [definition, in RefinementTypes.Examples]
M
map_erase_cons [lemma, in RefinementTypes.EvalTypeErasure]maximum_typed [lemma, in RefinementTypes.Examples]
maximum_tm [definition, in RefinementTypes.Examples]
maximum_ty [definition, in RefinementTypes.Examples]
N
Neg [constructor, in RefinementTypes.Avoid]no_converging_term_has_refine_false [lemma, in RefinementTypes.ExamplesPartialSoundness]
no_converging_term_has_bot [lemma, in RefinementTypes.ExamplesPartialSoundness]
no_value_in_bot [lemma, in RefinementTypes.ExamplesPartialSoundness]
nth_error_map [lemma, in RefinementTypes.EvalTypeErasure]
O
oov_map [definition, in RefinementTypes.EvalTypeErasure]OpAdd [constructor, in RefinementTypes.Syntax]
OpAnd [constructor, in RefinementTypes.Syntax]
OpDiv [constructor, in RefinementTypes.Syntax]
OpEq [constructor, in RefinementTypes.Syntax]
OpGe [constructor, in RefinementTypes.Syntax]
OpGt [constructor, in RefinementTypes.Syntax]
OpLe [constructor, in RefinementTypes.Syntax]
OpLt [constructor, in RefinementTypes.Syntax]
OpMod [constructor, in RefinementTypes.Syntax]
OpMul [constructor, in RefinementTypes.Syntax]
OpNeq [constructor, in RefinementTypes.Syntax]
OpOr [constructor, in RefinementTypes.Syntax]
OpSub [constructor, in RefinementTypes.Syntax]
OptionTy [definition, in RefinementTypes.Examples]
ordered [definition, in RefinementTypes.FirstOrder]
ordered_interp_vint32_base_ty [lemma, in RefinementTypes.FirstOrderLemmas]
ordered_interp_pair_compat [lemma, in RefinementTypes.FirstOrderLemmas]
OrderingTy [definition, in RefinementTypes.Examples]
ordering_sub [lemma, in RefinementTypes.Examples]
or_same_sub [lemma, in RefinementTypes.Examples]
P
Polarity [inductive, in RefinementTypes.Avoid]Polarity_sind [definition, in RefinementTypes.Avoid]
Polarity_rec [definition, in RefinementTypes.Avoid]
Polarity_ind [definition, in RefinementTypes.Avoid]
Polarity_rect [definition, in RefinementTypes.Avoid]
Pos [constructor, in RefinementTypes.Avoid]
Positivity [library]
PositivityLemmas [library]
R
rc_some_some [constructor, in RefinementTypes.EvalShiftLemmas]rc_some_none [constructor, in RefinementTypes.EvalShiftLemmas]
rc_none [constructor, in RefinementTypes.EvalShiftLemmas]
RefinedByP [definition, in RefinementTypes.ExamplesCollect]
refine_true_eq_base [lemma, in RefinementTypes.ExamplesPartialSoundness]
refine_diverge_eq_refine_true [lemma, in RefinementTypes.ExamplesPartialSoundness]
ren_tm_tabs_annotation [definition, in RefinementTypes.SubstExamples]
ren_ty_refine_propagates [definition, in RefinementTypes.SubstExamples]
ren_tm_refine_free [definition, in RefinementTypes.SubstExamples]
ren_tm_refine_bound [definition, in RefinementTypes.SubstExamples]
ren_ty_forall_free [definition, in RefinementTypes.SubstExamples]
ren_ty_forall [definition, in RefinementTypes.SubstExamples]
ren_tm_preserves_tyvar [definition, in RefinementTypes.SubstExamples]
ren_ty_preserves_tmvar [definition, in RefinementTypes.SubstExamples]
ren_tm_shift_tmvar [definition, in RefinementTypes.SubstExamples]
ren_ty_shift_tvar [definition, in RefinementTypes.SubstExamples]
ren_subst_comp_tm [lemma, in RefinementTypes.SubstLemmas]
ren_subst_comp_ty [lemma, in RefinementTypes.SubstLemmas]
ren_comp_tm [lemma, in RefinementTypes.SubstLemmas]
ren_comp_ty [lemma, in RefinementTypes.SubstLemmas]
ren_subst_tm [lemma, in RefinementTypes.SubstLemmas]
ren_subst_ty [lemma, in RefinementTypes.SubstLemmas]
ren_tm_upren_upren_id [lemma, in RefinementTypes.SubstLemmas]
ren_ty_upren_upren_id [lemma, in RefinementTypes.SubstLemmas]
ren_tm_upren_id [lemma, in RefinementTypes.SubstLemmas]
ren_ty_upren_id [lemma, in RefinementTypes.SubstLemmas]
ren_tm_id [lemma, in RefinementTypes.SubstLemmas]
ren_ty_id [lemma, in RefinementTypes.SubstLemmas]
ren_tm_ext [lemma, in RefinementTypes.SubstLemmas]
ren_ty_ext [lemma, in RefinementTypes.SubstLemmas]
ren_tm [definition, in RefinementTypes.Subst]
ren_ty [definition, in RefinementTypes.Subst]
ResTy [definition, in RefinementTypes.Examples]
res_weaken_compat_refl [lemma, in RefinementTypes.EvalShiftLemmas]
res_weaken_compat_sind [definition, in RefinementTypes.EvalShiftLemmas]
res_weaken_compat_ind [definition, in RefinementTypes.EvalShiftLemmas]
res_weaken_compat [inductive, in RefinementTypes.EvalShiftLemmas]
res_subst_compat_refl [lemma, in RefinementTypes.EvalSubstLemmas]
res_subst_compat_sind [definition, in RefinementTypes.EvalSubstLemmas]
res_subst_compat_ind [definition, in RefinementTypes.EvalSubstLemmas]
res_subst_compat [inductive, in RefinementTypes.EvalSubstLemmas]
rsc_some_some [constructor, in RefinementTypes.EvalSubstLemmas]
rsc_some_none [constructor, in RefinementTypes.EvalSubstLemmas]
rsc_none [constructor, in RefinementTypes.EvalSubstLemmas]
run_loop [definition, in RefinementTypes.Eval]
run_loop_erase_ty [lemma, in RefinementTypes.EvalTypeErasure]
run_loop_weaken_compat [lemma, in RefinementTypes.EvalShiftLemmas]
run_loop_subst_compat_bwd [lemma, in RefinementTypes.EvalSubstLemmas]
run_loop_subst_compat_fwd [lemma, in RefinementTypes.EvalSubstLemmas]
run_loop_typed [lemma, in RefinementTypes.EvalLemmas]
run_loop_mono [lemma, in RefinementTypes.EvalLemmas]
S
scons [definition, in RefinementTypes.Subst]SemanticImplies [library]
SemanticSubtyping [library]
SemanticTyping [library]
SemTy [definition, in RefinementTypes.Interp]
sem_subtype_base_refine_diverge [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_diverge_base [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_base_refine_true [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_true_base [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_true_diverge [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_diverge_true [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_implies_and_false_terminating [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_terminates [definition, in RefinementTypes.ExamplesPartialSoundness]
sem_implies_and_true [lemma, in RefinementTypes.ExamplesPartialSoundness]
sem_implies [definition, in RefinementTypes.SemanticImplies]
sem_subtype_mu_fold [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_mu_unfold [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_tvar_lower [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_tvar_upper [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_bot [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_top [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_refine [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_refine_base [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_and [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_and_r [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_and_l [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_or [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_or_r [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_or_l [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_sigma [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_forall [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_fun [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_trans [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype_refl [lemma, in RefinementTypes.SemanticSubtyping]
sem_subtype [definition, in RefinementTypes.SemanticSubtyping]
sem_typed_match_sum [lemma, in RefinementTypes.SemanticTyping]
sem_typed_inr [lemma, in RefinementTypes.SemanticTyping]
sem_typed_inl [lemma, in RefinementTypes.SemanticTyping]
sem_typed_match_pair [lemma, in RefinementTypes.SemanticTyping]
sem_typed_pair_anf [lemma, in RefinementTypes.SemanticTyping]
sem_typed_sub [lemma, in RefinementTypes.SemanticTyping]
sem_typed_selfify [lemma, in RefinementTypes.SemanticTyping]
sem_typed_loop [lemma, in RefinementTypes.SemanticTyping]
sem_typed_if [lemma, in RefinementTypes.SemanticTyping]
sem_typed_bin_op [lemma, in RefinementTypes.SemanticTyping]
sem_typed_let [lemma, in RefinementTypes.SemanticTyping]
sem_typed_tapp [lemma, in RefinementTypes.SemanticTyping]
sem_typed_tabs [lemma, in RefinementTypes.SemanticTyping]
sem_typed_app_anf [lemma, in RefinementTypes.SemanticTyping]
sem_typed_abs [lemma, in RefinementTypes.SemanticTyping]
sem_typed_var [lemma, in RefinementTypes.SemanticTyping]
sem_typed_int32 [lemma, in RefinementTypes.SemanticTyping]
sem_typed_bool [lemma, in RefinementTypes.SemanticTyping]
sem_typed_unit [lemma, in RefinementTypes.SemanticTyping]
sem_typed_diverge [lemma, in RefinementTypes.SemanticTyping]
sem_typed [definition, in RefinementTypes.SemanticTyping]
shift_scons_comp_id [lemma, in RefinementTypes.AvoidLemmas]
sigma_gen_zero [lemma, in RefinementTypes.InterpSubstLemmas]
sigma_gen_up_tm_ty [lemma, in RefinementTypes.InterpSubstLemmas]
sigma_gen_up_ty_ty [lemma, in RefinementTypes.InterpSubstLemmas]
sigma_gen [definition, in RefinementTypes.InterpSubstLemmas]
skipn_extend [lemma, in RefinementTypes.WfLemmas]
spos [definition, in RefinementTypes.Positivity]
spos_avoid [definition, in RefinementTypes.AvoidLemmas]
spos_ty_var_absent_avoid [lemma, in RefinementTypes.AvoidLemmas]
SSub_Mu_Fold [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Mu_Unfold [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_TVar_Lower [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_TVar_Upper [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Bot [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Top [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Refine [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Refine_Base [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_And [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_And_R [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_And_L [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Or [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Or_R [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Or_L [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Sigma [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Forall [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Fun [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Trans [constructor, in RefinementTypes.SyntacticSubtyping]
SSub_Refl [constructor, in RefinementTypes.SyntacticSubtyping]
ST_MatchSum [constructor, in RefinementTypes.SyntacticTyping]
ST_Inr [constructor, in RefinementTypes.SyntacticTyping]
ST_Inl [constructor, in RefinementTypes.SyntacticTyping]
ST_MatchPair [constructor, in RefinementTypes.SyntacticTyping]
ST_Pair [constructor, in RefinementTypes.SyntacticTyping]
ST_Sub [constructor, in RefinementTypes.SyntacticTyping]
ST_Selfify [constructor, in RefinementTypes.SyntacticTyping]
ST_Loop [constructor, in RefinementTypes.SyntacticTyping]
ST_If [constructor, in RefinementTypes.SyntacticTyping]
ST_BinOp [constructor, in RefinementTypes.SyntacticTyping]
ST_Let [constructor, in RefinementTypes.SyntacticTyping]
ST_TApp [constructor, in RefinementTypes.SyntacticTyping]
ST_TAbs [constructor, in RefinementTypes.SyntacticTyping]
ST_App [constructor, in RefinementTypes.SyntacticTyping]
ST_Abs [constructor, in RefinementTypes.SyntacticTyping]
ST_Var [constructor, in RefinementTypes.SyntacticTyping]
ST_Int32 [constructor, in RefinementTypes.SyntacticTyping]
ST_Bool [constructor, in RefinementTypes.SyntacticTyping]
ST_Unit [constructor, in RefinementTypes.SyntacticTyping]
ST_Diverge [constructor, in RefinementTypes.SyntacticTyping]
Subst [library]
SubstExamples [library]
SubstLemmas [library]
subst_tm_preserves_tyvar [definition, in RefinementTypes.SubstExamples]
subst_ty_preserves_tmvar [definition, in RefinementTypes.SubstExamples]
subst_tm_id [definition, in RefinementTypes.SubstExamples]
subst_ty_id [definition, in RefinementTypes.SubstExamples]
subst_tm_refine_free [definition, in RefinementTypes.SubstExamples]
subst_tm_refine_bound [definition, in RefinementTypes.SubstExamples]
subst_tm_tabs_annotation [definition, in RefinementTypes.SubstExamples]
subst_ty_refine_propagates [definition, in RefinementTypes.SubstExamples]
subst_ty_forall_free_shift [definition, in RefinementTypes.SubstExamples]
subst_ty_forall_free [definition, in RefinementTypes.SubstExamples]
subst_ty_forall_bound [definition, in RefinementTypes.SubstExamples]
subst_ty_other_var [definition, in RefinementTypes.SubstExamples]
subst_ty_basic [definition, in RefinementTypes.SubstExamples]
subst_ty_up_ty_TVar_shift [lemma, in RefinementTypes.SubstLemmas]
subst_tm_up_ty_TVar_shift [lemma, in RefinementTypes.SubstLemmas]
subst_tm_up_upn_shift0 [lemma, in RefinementTypes.SubstLemmas]
subst_tm_shift0 [lemma, in RefinementTypes.SubstLemmas]
subst_tm_upn_shift0 [lemma, in RefinementTypes.SubstLemmas]
subst_comp_tm [lemma, in RefinementTypes.SubstLemmas]
subst_comp_ty [lemma, in RefinementTypes.SubstLemmas]
subst_ren_tm [lemma, in RefinementTypes.SubstLemmas]
subst_ren_ty [lemma, in RefinementTypes.SubstLemmas]
subst_tm_up_tm_tm_up_tm_tm_tvar [lemma, in RefinementTypes.SubstLemmas]
subst_tm_up_tm_tm_tvar [lemma, in RefinementTypes.SubstLemmas]
subst_tm_up_tm_ty_TVar [lemma, in RefinementTypes.SubstLemmas]
subst_ty_up_tm_ty_TVar [lemma, in RefinementTypes.SubstLemmas]
subst_tm_id [lemma, in RefinementTypes.SubstLemmas]
subst_ty_id [lemma, in RefinementTypes.SubstLemmas]
subst_tm_ext [lemma, in RefinementTypes.SubstLemmas]
subst_ty_ext [lemma, in RefinementTypes.SubstLemmas]
subst_tm [definition, in RefinementTypes.Subst]
subst_ty [definition, in RefinementTypes.Subst]
subst_not_mentions_tm [lemma, in RefinementTypes.AvoidLemmas]
subst_not_mentions_ty [lemma, in RefinementTypes.AvoidLemmas]
SyntacticSubtyping [library]
SyntacticTyping [library]
Syntax [library]
syn_typed_adequate [lemma, in RefinementTypes.Adequacy]
syn_subtype_adequate [lemma, in RefinementTypes.Adequacy]
syn_subtype_sind [definition, in RefinementTypes.SyntacticSubtyping]
syn_subtype_ind [definition, in RefinementTypes.SyntacticSubtyping]
syn_subtype [inductive, in RefinementTypes.SyntacticSubtyping]
syn_typed_sind [definition, in RefinementTypes.SyntacticTyping]
syn_typed_ind [definition, in RefinementTypes.SyntacticTyping]
syn_typed [inductive, in RefinementTypes.SyntacticTyping]
T
tabs [constructor, in RefinementTypes.Syntax]Tactics [library]
TAnd [constructor, in RefinementTypes.Syntax]
tapp [constructor, in RefinementTypes.Syntax]
tbin_op [constructor, in RefinementTypes.Syntax]
tbool [constructor, in RefinementTypes.Syntax]
TBool [constructor, in RefinementTypes.Syntax]
TBot [constructor, in RefinementTypes.Syntax]
TBounds [definition, in RefinementTypes.Wf]
tbounds_shift_term [definition, in RefinementTypes.Wf]
tbounds_shift_term_hd [lemma, in RefinementTypes.Examples]
tdiverge [constructor, in RefinementTypes.Syntax]
tenv_shift_type [definition, in RefinementTypes.WfLemmas]
Term [inductive, in RefinementTypes.Syntax]
term_eq_dec [definition, in RefinementTypes.Syntax]
Term_sind [definition, in RefinementTypes.Syntax]
Term_rec [definition, in RefinementTypes.Syntax]
Term_ind [definition, in RefinementTypes.Syntax]
Term_rect [definition, in RefinementTypes.Syntax]
term_has_semtype [definition, in RefinementTypes.Interp]
term_has_semtype_mono [lemma, in RefinementTypes.PositivityLemmas]
term_mentions_ty [definition, in RefinementTypes.Avoid]
term_mentions [definition, in RefinementTypes.Avoid]
test_collect_none_ok [definition, in RefinementTypes.ExamplesCollect]
test_collect_none [definition, in RefinementTypes.ExamplesCollect]
test_collect_empty_ok [definition, in RefinementTypes.ExamplesCollect]
test_collect_empty [definition, in RefinementTypes.ExamplesCollect]
test_collect_ok [definition, in RefinementTypes.ExamplesCollect]
test_collect [definition, in RefinementTypes.ExamplesCollect]
test_maximum_singleton [definition, in RefinementTypes.Examples]
test_maximum_empty [definition, in RefinementTypes.Examples]
test_maximum_nonempty [definition, in RefinementTypes.Examples]
TForall [constructor, in RefinementTypes.Syntax]
TFun [constructor, in RefinementTypes.Syntax]
tif [constructor, in RefinementTypes.Syntax]
tinl [constructor, in RefinementTypes.Syntax]
tinr [constructor, in RefinementTypes.Syntax]
tint32 [constructor, in RefinementTypes.Syntax]
TInt32 [constructor, in RefinementTypes.Syntax]
tlet [constructor, in RefinementTypes.Syntax]
tloop [constructor, in RefinementTypes.Syntax]
tmatch_sum [constructor, in RefinementTypes.Syntax]
tmatch_pair [constructor, in RefinementTypes.Syntax]
TMuAll [constructor, in RefinementTypes.Syntax]
tm_shift_0_eq [lemma, in RefinementTypes.SubstLemmas]
tm_shift [definition, in RefinementTypes.SubstLemmas]
TOr [constructor, in RefinementTypes.Syntax]
tpair [constructor, in RefinementTypes.Syntax]
transport_fun_rev [lemma, in RefinementTypes.PositivityLemmas]
transport_fun [lemma, in RefinementTypes.PositivityLemmas]
TRefine [constructor, in RefinementTypes.Syntax]
TSigma [constructor, in RefinementTypes.Syntax]
TSum [constructor, in RefinementTypes.Syntax]
ttabs [constructor, in RefinementTypes.Syntax]
ttapp [constructor, in RefinementTypes.Syntax]
TTop [constructor, in RefinementTypes.Syntax]
tunit [constructor, in RefinementTypes.Syntax]
TUnit [constructor, in RefinementTypes.Syntax]
tvar [constructor, in RefinementTypes.Syntax]
TVar [constructor, in RefinementTypes.Syntax]
Ty [inductive, in RefinementTypes.Syntax]
typeof [definition, in RefinementTypes.AlgorithmicTyping]
ty_var_absent [definition, in RefinementTypes.Positivity]
ty_subst_shifts_under_tfun [definition, in RefinementTypes.SubstExamples]
ty_subst_refine_propagates [definition, in RefinementTypes.SubstExamples]
ty_subst_basic [definition, in RefinementTypes.SubstExamples]
ty_eq_dec [definition, in RefinementTypes.Syntax]
Ty_sind [definition, in RefinementTypes.Syntax]
Ty_rec [definition, in RefinementTypes.Syntax]
Ty_ind [definition, in RefinementTypes.Syntax]
Ty_rect [definition, in RefinementTypes.Syntax]
ty_subst [definition, in RefinementTypes.Subst]
U
unit_with_true_eq_unit_with_diverge [lemma, in RefinementTypes.ExamplesPartialSoundness]unit_eq_unit_with_true [lemma, in RefinementTypes.ExamplesPartialSoundness]
upn_tm_shift0_ids [lemma, in RefinementTypes.SubstLemmas]
upn_tm_ids [lemma, in RefinementTypes.SubstLemmas]
upn_tm_ext [lemma, in RefinementTypes.SubstLemmas]
upn_tm [definition, in RefinementTypes.Subst]
upren [definition, in RefinementTypes.Subst]
upren_upren_comp [lemma, in RefinementTypes.SubstLemmas]
upren_comp [lemma, in RefinementTypes.SubstLemmas]
upren_upren_id [lemma, in RefinementTypes.SubstLemmas]
upren_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_tvar_ext [lemma, in RefinementTypes.EvalTypeErasure]
up_ty_tm_tvar_ext [lemma, in RefinementTypes.EvalTypeErasure]
up_tm_tm_tvar_ext [lemma, in RefinementTypes.EvalTypeErasure]
up_ty_tm_upn_tm_scons_tvar [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_upn_tm_shift [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_shift0_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_subst_comp [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_ren_subst [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_subst_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_ren [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_ren [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_ren [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_id [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_id [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_id [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm_ext [lemma, in RefinementTypes.SubstLemmas]
up_tm_ty_ext [lemma, in RefinementTypes.SubstLemmas]
up_ty_tm_ext [lemma, in RefinementTypes.SubstLemmas]
up_ty_ty_ext [lemma, in RefinementTypes.SubstLemmas]
up_tm_tm [definition, in RefinementTypes.Subst]
up_tm_ty [definition, in RefinementTypes.Subst]
up_ty_tm [definition, in RefinementTypes.Subst]
up_ty_ty [definition, in RefinementTypes.Subst]
up_tm_tm_not_i [lemma, in RefinementTypes.AvoidLemmas]
U_sub_T [lemma, in RefinementTypes.Examples]
V
vabs [constructor, in RefinementTypes.Syntax]Value [inductive, in RefinementTypes.Syntax]
Value_ind_nested [definition, in RefinementTypes.Syntax]
Value_ind_nested.Htabs [variable, in RefinementTypes.Syntax]
Value_ind_nested.Habs [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hinr [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hinl [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hpair [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hint32 [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hbool [variable, in RefinementTypes.Syntax]
Value_ind_nested.Hunit [variable, in RefinementTypes.Syntax]
Value_ind_nested.P [variable, in RefinementTypes.Syntax]
Value_ind_nested [section, in RefinementTypes.Syntax]
Value_sind [definition, in RefinementTypes.Syntax]
Value_rec [definition, in RefinementTypes.Syntax]
Value_ind [definition, in RefinementTypes.Syntax]
Value_rect [definition, in RefinementTypes.Syntax]
val_weaken_compat_refl [lemma, in RefinementTypes.EvalShiftLemmas]
val_weaken_compat_sind [definition, in RefinementTypes.EvalShiftLemmas]
val_weaken_compat_ind [definition, in RefinementTypes.EvalShiftLemmas]
val_weaken_compat [inductive, in RefinementTypes.EvalShiftLemmas]
val_subst_compat_refl [lemma, in RefinementTypes.EvalSubstLemmas]
val_subst_compat_sind [definition, in RefinementTypes.EvalSubstLemmas]
val_subst_compat_ind [definition, in RefinementTypes.EvalSubstLemmas]
val_subst_compat [inductive, in RefinementTypes.EvalSubstLemmas]
var [definition, in RefinementTypes.Syntax]
vbool [constructor, in RefinementTypes.Syntax]
vc_tabs [constructor, in RefinementTypes.EvalShiftLemmas]
vc_abs [constructor, in RefinementTypes.EvalShiftLemmas]
vc_inr [constructor, in RefinementTypes.EvalShiftLemmas]
vc_inl [constructor, in RefinementTypes.EvalShiftLemmas]
vc_pair [constructor, in RefinementTypes.EvalShiftLemmas]
vc_int32 [constructor, in RefinementTypes.EvalShiftLemmas]
vc_bool [constructor, in RefinementTypes.EvalShiftLemmas]
vc_unit [constructor, in RefinementTypes.EvalShiftLemmas]
vinl [constructor, in RefinementTypes.Syntax]
vinr [constructor, in RefinementTypes.Syntax]
vint32 [constructor, in RefinementTypes.Syntax]
vpair [constructor, in RefinementTypes.Syntax]
vsc_tabs [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_abs [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_inr [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_inl [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_pair [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_int32 [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_bool [constructor, in RefinementTypes.EvalSubstLemmas]
vsc_unit [constructor, in RefinementTypes.EvalSubstLemmas]
vtabs [constructor, in RefinementTypes.Syntax]
vunit [constructor, in RefinementTypes.Syntax]
W
Wf [library]WfLemmas [library]
wf_benv [definition, in RefinementTypes.Wf]
wf_facts [definition, in RefinementTypes.Wf]
wf_env [definition, in RefinementTypes.Wf]
wf_facts_cons [lemma, in RefinementTypes.WfLemmas]
wf_benv_lookup [lemma, in RefinementTypes.WfLemmas]
wf_benv_double_shift_term [lemma, in RefinementTypes.WfLemmas]
wf_benv_shift_term [lemma, in RefinementTypes.WfLemmas]
wf_benv_cons [lemma, in RefinementTypes.WfLemmas]
wf_facts_extend [lemma, in RefinementTypes.WfLemmas]
wf_env_lookup [lemma, in RefinementTypes.WfLemmas]
wf_env_length [lemma, in RefinementTypes.WfLemmas]
wf_env_cons [lemma, in RefinementTypes.WfLemmas]
other
_ .: _ [notation, in RefinementTypes.Subst]_ >> _ [notation, in RefinementTypes.Subst]
Notation Index
other
_ .: _ [in RefinementTypes.Subst]_ >> _ [in RefinementTypes.Subst]
Variable Index
V
Value_ind_nested.Htabs [in RefinementTypes.Syntax]Value_ind_nested.Habs [in RefinementTypes.Syntax]
Value_ind_nested.Hinr [in RefinementTypes.Syntax]
Value_ind_nested.Hinl [in RefinementTypes.Syntax]
Value_ind_nested.Hpair [in RefinementTypes.Syntax]
Value_ind_nested.Hint32 [in RefinementTypes.Syntax]
Value_ind_nested.Hbool [in RefinementTypes.Syntax]
Value_ind_nested.Hunit [in RefinementTypes.Syntax]
Value_ind_nested.P [in RefinementTypes.Syntax]
Library Index
A
AdequacyAlgorithmicTyping
Avoid
AvoidLemmas
E
EvalEvalLemmas
EvalShiftLemmas
EvalSubstLemmas
EvalTypeErasure
Examples
ExamplesCollect
ExamplesPartialSoundness
F
FirstOrderFirstOrderLemmas
I
InterpInterpShiftLemmas
InterpSubstLemmas
L
ListLemmasP
PositivityPositivityLemmas
S
SemanticImpliesSemanticSubtyping
SemanticTyping
Subst
SubstExamples
SubstLemmas
SyntacticSubtyping
SyntacticTyping
Syntax
T
TacticsW
WfWfLemmas
Lemma Index
A
abstract_term_var_cancel [in RefinementTypes.SubstLemmas]avoid_subst_shift_id [in RefinementTypes.AvoidLemmas]
avoid_subst_shift_id_gen [in RefinementTypes.AvoidLemmas]
avoid_not_mentions [in RefinementTypes.AvoidLemmas]
B
bin_op_ty_interp_val_pair_compat [in RefinementTypes.FirstOrderLemmas]bin_op_eq_dec [in RefinementTypes.Syntax]
bool_ty_interp_pair_compat [in RefinementTypes.FirstOrderLemmas]
bot_eq_refine_false [in RefinementTypes.ExamplesPartialSoundness]
D
diverge_and_false_not_implies_false [in RefinementTypes.ExamplesPartialSoundness]diverge_and_false_not_sub_false [in RefinementTypes.ExamplesPartialSoundness]
diverge_not_sub_false [in RefinementTypes.ExamplesPartialSoundness]
E
env_subst_compat_cons [in RefinementTypes.EvalSubstLemmas]env_incr_wf [in RefinementTypes.WfLemmas]
erase_ty_in_tm_subst [in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm_subst_gen [in RefinementTypes.EvalTypeErasure]
erase_ty_in_val_vbool_true [in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm_ren [in RefinementTypes.EvalTypeErasure]
eval_and_bool [in RefinementTypes.ExamplesPartialSoundness]
eval_tdiverge [in RefinementTypes.ExamplesPartialSoundness]
eval_to_true_subst_env [in RefinementTypes.InterpSubstLemmas]
eval_erase_ty [in RefinementTypes.EvalTypeErasure]
eval_to_true_shift_env [in RefinementTypes.InterpShiftLemmas]
eval_to_true_subst_ty_gen [in RefinementTypes.InterpShiftLemmas]
eval_to_true_subst_ty [in RefinementTypes.InterpShiftLemmas]
eval_to_true_ren_ty [in RefinementTypes.InterpShiftLemmas]
eval_to_true_erase_eq [in RefinementTypes.InterpShiftLemmas]
eval_shift_env_bwd [in RefinementTypes.EvalShiftLemmas]
eval_shift_env_fwd [in RefinementTypes.EvalShiftLemmas]
eval_weaken_compat [in RefinementTypes.EvalShiftLemmas]
eval_bin_op_val_weaken_compat [in RefinementTypes.EvalShiftLemmas]
eval_bin_op_result_in_interp [in RefinementTypes.FirstOrderLemmas]
eval_subst_env_bwd [in RefinementTypes.EvalSubstLemmas]
eval_subst_env_fwd [in RefinementTypes.EvalSubstLemmas]
eval_term_subst_compat_bwd [in RefinementTypes.EvalSubstLemmas]
eval_term_subst_compat_fwd [in RefinementTypes.EvalSubstLemmas]
eval_bin_op_val_subst_compat [in RefinementTypes.EvalSubstLemmas]
eval_bin_op_defined [in RefinementTypes.EvalLemmas]
eval_bin_op_eq_refl [in RefinementTypes.EvalLemmas]
eval_bin_op_eq_fo_defined [in RefinementTypes.EvalLemmas]
eval_tbin_op [in RefinementTypes.EvalLemmas]
eval_fuel_mono [in RefinementTypes.EvalLemmas]
eval_false_not_true [in RefinementTypes.AvoidLemmas]
F
Forall_Forall2_refl [in RefinementTypes.ListLemmas]Forall2_refl [in RefinementTypes.ListLemmas]
Forall2_exists2_r [in RefinementTypes.ListLemmas]
Forall2_exists2 [in RefinementTypes.ListLemmas]
fo_interp_is_fo_val [in RefinementTypes.FirstOrderLemmas]
full_safety [in RefinementTypes.AlgorithmicTyping]
I
interp_subst [in RefinementTypes.InterpSubstLemmas]interp_subst_gen [in RefinementTypes.InterpSubstLemmas]
interp_weaken_both [in RefinementTypes.InterpSubstLemmas]
interp_subst_term [in RefinementTypes.InterpSubstLemmas]
interp_subst_up_term [in RefinementTypes.InterpSubstLemmas]
interp_env_ren_type [in RefinementTypes.InterpShiftLemmas]
interp_weaken_type [in RefinementTypes.InterpShiftLemmas]
interp_env_ren_term [in RefinementTypes.InterpShiftLemmas]
interp_weaken_term [in RefinementTypes.InterpShiftLemmas]
interp_mu_eq_ext [in RefinementTypes.Interp]
interp_shift_type_by [in RefinementTypes.WfLemmas]
interp_env_shift_term [in RefinementTypes.WfLemmas]
interp_mu_mono [in RefinementTypes.PositivityLemmas]
interp_spos_distribute [in RefinementTypes.PositivityLemmas]
interp_spos_mono [in RefinementTypes.PositivityLemmas]
interp_ty_var_absent [in RefinementTypes.PositivityLemmas]
interp_avoid_shift [in RefinementTypes.AvoidLemmas]
interp_avoid_var0 [in RefinementTypes.AvoidLemmas]
interp_avoid_neg [in RefinementTypes.AvoidLemmas]
interp_avoid_pos [in RefinementTypes.AvoidLemmas]
interp_avoid_pos_neg [in RefinementTypes.AvoidLemmas]
iter_up_tm [in RefinementTypes.SubstLemmas]
L
list_unfold_sub [in RefinementTypes.Examples]M
map_erase_cons [in RefinementTypes.EvalTypeErasure]maximum_typed [in RefinementTypes.Examples]
N
no_converging_term_has_refine_false [in RefinementTypes.ExamplesPartialSoundness]no_converging_term_has_bot [in RefinementTypes.ExamplesPartialSoundness]
no_value_in_bot [in RefinementTypes.ExamplesPartialSoundness]
nth_error_map [in RefinementTypes.EvalTypeErasure]
O
ordered_interp_vint32_base_ty [in RefinementTypes.FirstOrderLemmas]ordered_interp_pair_compat [in RefinementTypes.FirstOrderLemmas]
ordering_sub [in RefinementTypes.Examples]
or_same_sub [in RefinementTypes.Examples]
R
refine_true_eq_base [in RefinementTypes.ExamplesPartialSoundness]refine_diverge_eq_refine_true [in RefinementTypes.ExamplesPartialSoundness]
ren_subst_comp_tm [in RefinementTypes.SubstLemmas]
ren_subst_comp_ty [in RefinementTypes.SubstLemmas]
ren_comp_tm [in RefinementTypes.SubstLemmas]
ren_comp_ty [in RefinementTypes.SubstLemmas]
ren_subst_tm [in RefinementTypes.SubstLemmas]
ren_subst_ty [in RefinementTypes.SubstLemmas]
ren_tm_upren_upren_id [in RefinementTypes.SubstLemmas]
ren_ty_upren_upren_id [in RefinementTypes.SubstLemmas]
ren_tm_upren_id [in RefinementTypes.SubstLemmas]
ren_ty_upren_id [in RefinementTypes.SubstLemmas]
ren_tm_id [in RefinementTypes.SubstLemmas]
ren_ty_id [in RefinementTypes.SubstLemmas]
ren_tm_ext [in RefinementTypes.SubstLemmas]
ren_ty_ext [in RefinementTypes.SubstLemmas]
res_weaken_compat_refl [in RefinementTypes.EvalShiftLemmas]
res_subst_compat_refl [in RefinementTypes.EvalSubstLemmas]
run_loop_erase_ty [in RefinementTypes.EvalTypeErasure]
run_loop_weaken_compat [in RefinementTypes.EvalShiftLemmas]
run_loop_subst_compat_bwd [in RefinementTypes.EvalSubstLemmas]
run_loop_subst_compat_fwd [in RefinementTypes.EvalSubstLemmas]
run_loop_typed [in RefinementTypes.EvalLemmas]
run_loop_mono [in RefinementTypes.EvalLemmas]
S
sem_subtype_base_refine_diverge [in RefinementTypes.ExamplesPartialSoundness]sem_subtype_refine_diverge_base [in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_base_refine_true [in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_true_base [in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_true_diverge [in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_refine_diverge_true [in RefinementTypes.ExamplesPartialSoundness]
sem_implies_and_false_terminating [in RefinementTypes.ExamplesPartialSoundness]
sem_implies_and_true [in RefinementTypes.ExamplesPartialSoundness]
sem_subtype_mu_fold [in RefinementTypes.SemanticSubtyping]
sem_subtype_mu_unfold [in RefinementTypes.SemanticSubtyping]
sem_subtype_tvar_lower [in RefinementTypes.SemanticSubtyping]
sem_subtype_tvar_upper [in RefinementTypes.SemanticSubtyping]
sem_subtype_bot [in RefinementTypes.SemanticSubtyping]
sem_subtype_top [in RefinementTypes.SemanticSubtyping]
sem_subtype_refine [in RefinementTypes.SemanticSubtyping]
sem_subtype_refine_base [in RefinementTypes.SemanticSubtyping]
sem_subtype_and [in RefinementTypes.SemanticSubtyping]
sem_subtype_and_r [in RefinementTypes.SemanticSubtyping]
sem_subtype_and_l [in RefinementTypes.SemanticSubtyping]
sem_subtype_or [in RefinementTypes.SemanticSubtyping]
sem_subtype_or_r [in RefinementTypes.SemanticSubtyping]
sem_subtype_or_l [in RefinementTypes.SemanticSubtyping]
sem_subtype_sigma [in RefinementTypes.SemanticSubtyping]
sem_subtype_forall [in RefinementTypes.SemanticSubtyping]
sem_subtype_fun [in RefinementTypes.SemanticSubtyping]
sem_subtype_trans [in RefinementTypes.SemanticSubtyping]
sem_subtype_refl [in RefinementTypes.SemanticSubtyping]
sem_typed_match_sum [in RefinementTypes.SemanticTyping]
sem_typed_inr [in RefinementTypes.SemanticTyping]
sem_typed_inl [in RefinementTypes.SemanticTyping]
sem_typed_match_pair [in RefinementTypes.SemanticTyping]
sem_typed_pair_anf [in RefinementTypes.SemanticTyping]
sem_typed_sub [in RefinementTypes.SemanticTyping]
sem_typed_selfify [in RefinementTypes.SemanticTyping]
sem_typed_loop [in RefinementTypes.SemanticTyping]
sem_typed_if [in RefinementTypes.SemanticTyping]
sem_typed_bin_op [in RefinementTypes.SemanticTyping]
sem_typed_let [in RefinementTypes.SemanticTyping]
sem_typed_tapp [in RefinementTypes.SemanticTyping]
sem_typed_tabs [in RefinementTypes.SemanticTyping]
sem_typed_app_anf [in RefinementTypes.SemanticTyping]
sem_typed_abs [in RefinementTypes.SemanticTyping]
sem_typed_var [in RefinementTypes.SemanticTyping]
sem_typed_int32 [in RefinementTypes.SemanticTyping]
sem_typed_bool [in RefinementTypes.SemanticTyping]
sem_typed_unit [in RefinementTypes.SemanticTyping]
sem_typed_diverge [in RefinementTypes.SemanticTyping]
shift_scons_comp_id [in RefinementTypes.AvoidLemmas]
sigma_gen_zero [in RefinementTypes.InterpSubstLemmas]
sigma_gen_up_tm_ty [in RefinementTypes.InterpSubstLemmas]
sigma_gen_up_ty_ty [in RefinementTypes.InterpSubstLemmas]
skipn_extend [in RefinementTypes.WfLemmas]
spos_ty_var_absent_avoid [in RefinementTypes.AvoidLemmas]
subst_ty_up_ty_TVar_shift [in RefinementTypes.SubstLemmas]
subst_tm_up_ty_TVar_shift [in RefinementTypes.SubstLemmas]
subst_tm_up_upn_shift0 [in RefinementTypes.SubstLemmas]
subst_tm_shift0 [in RefinementTypes.SubstLemmas]
subst_tm_upn_shift0 [in RefinementTypes.SubstLemmas]
subst_comp_tm [in RefinementTypes.SubstLemmas]
subst_comp_ty [in RefinementTypes.SubstLemmas]
subst_ren_tm [in RefinementTypes.SubstLemmas]
subst_ren_ty [in RefinementTypes.SubstLemmas]
subst_tm_up_tm_tm_up_tm_tm_tvar [in RefinementTypes.SubstLemmas]
subst_tm_up_tm_tm_tvar [in RefinementTypes.SubstLemmas]
subst_tm_up_tm_ty_TVar [in RefinementTypes.SubstLemmas]
subst_ty_up_tm_ty_TVar [in RefinementTypes.SubstLemmas]
subst_tm_id [in RefinementTypes.SubstLemmas]
subst_ty_id [in RefinementTypes.SubstLemmas]
subst_tm_ext [in RefinementTypes.SubstLemmas]
subst_ty_ext [in RefinementTypes.SubstLemmas]
subst_not_mentions_tm [in RefinementTypes.AvoidLemmas]
subst_not_mentions_ty [in RefinementTypes.AvoidLemmas]
syn_typed_adequate [in RefinementTypes.Adequacy]
syn_subtype_adequate [in RefinementTypes.Adequacy]
T
tbounds_shift_term_hd [in RefinementTypes.Examples]term_has_semtype_mono [in RefinementTypes.PositivityLemmas]
tm_shift_0_eq [in RefinementTypes.SubstLemmas]
transport_fun_rev [in RefinementTypes.PositivityLemmas]
transport_fun [in RefinementTypes.PositivityLemmas]
U
unit_with_true_eq_unit_with_diverge [in RefinementTypes.ExamplesPartialSoundness]unit_eq_unit_with_true [in RefinementTypes.ExamplesPartialSoundness]
upn_tm_shift0_ids [in RefinementTypes.SubstLemmas]
upn_tm_ids [in RefinementTypes.SubstLemmas]
upn_tm_ext [in RefinementTypes.SubstLemmas]
upren_upren_comp [in RefinementTypes.SubstLemmas]
upren_comp [in RefinementTypes.SubstLemmas]
upren_upren_id [in RefinementTypes.SubstLemmas]
upren_id [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_tvar_ext [in RefinementTypes.EvalTypeErasure]
up_ty_tm_tvar_ext [in RefinementTypes.EvalTypeErasure]
up_tm_tm_tvar_ext [in RefinementTypes.EvalTypeErasure]
up_ty_tm_upn_tm_scons_tvar [in RefinementTypes.SubstLemmas]
up_ty_tm_upn_tm_shift [in RefinementTypes.SubstLemmas]
up_tm_tm_shift0_id [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_subst_comp [in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_subst_comp [in RefinementTypes.SubstLemmas]
up_tm_tm_subst_comp [in RefinementTypes.SubstLemmas]
up_tm_ty_subst_comp [in RefinementTypes.SubstLemmas]
up_ty_tm_subst_comp [in RefinementTypes.SubstLemmas]
up_ty_ty_subst_comp [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_ren_subst [in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_ren_subst [in RefinementTypes.SubstLemmas]
up_tm_tm_ren_subst [in RefinementTypes.SubstLemmas]
up_tm_ty_ren_subst [in RefinementTypes.SubstLemmas]
up_ty_tm_ren_subst [in RefinementTypes.SubstLemmas]
up_ty_ty_ren_subst [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_subst_ren [in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_subst_ren [in RefinementTypes.SubstLemmas]
up_tm_tm_subst_ren [in RefinementTypes.SubstLemmas]
up_tm_ty_subst_ren [in RefinementTypes.SubstLemmas]
up_ty_tm_subst_ren [in RefinementTypes.SubstLemmas]
up_ty_ty_subst_ren [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_ren [in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_ren [in RefinementTypes.SubstLemmas]
up_tm_tm_ren [in RefinementTypes.SubstLemmas]
up_tm_ty_ren [in RefinementTypes.SubstLemmas]
up_ty_tm_ren [in RefinementTypes.SubstLemmas]
up_ty_ty_ren [in RefinementTypes.SubstLemmas]
up_tm_tm_up_tm_tm_id [in RefinementTypes.SubstLemmas]
up_tm_ty_up_tm_ty_id [in RefinementTypes.SubstLemmas]
up_tm_tm_id [in RefinementTypes.SubstLemmas]
up_tm_ty_id [in RefinementTypes.SubstLemmas]
up_ty_tm_id [in RefinementTypes.SubstLemmas]
up_ty_ty_id [in RefinementTypes.SubstLemmas]
up_tm_tm_ext [in RefinementTypes.SubstLemmas]
up_tm_ty_ext [in RefinementTypes.SubstLemmas]
up_ty_tm_ext [in RefinementTypes.SubstLemmas]
up_ty_ty_ext [in RefinementTypes.SubstLemmas]
up_tm_tm_not_i [in RefinementTypes.AvoidLemmas]
U_sub_T [in RefinementTypes.Examples]
V
val_weaken_compat_refl [in RefinementTypes.EvalShiftLemmas]val_subst_compat_refl [in RefinementTypes.EvalSubstLemmas]
W
wf_facts_cons [in RefinementTypes.WfLemmas]wf_benv_lookup [in RefinementTypes.WfLemmas]
wf_benv_double_shift_term [in RefinementTypes.WfLemmas]
wf_benv_shift_term [in RefinementTypes.WfLemmas]
wf_benv_cons [in RefinementTypes.WfLemmas]
wf_facts_extend [in RefinementTypes.WfLemmas]
wf_env_lookup [in RefinementTypes.WfLemmas]
wf_env_length [in RefinementTypes.WfLemmas]
wf_env_cons [in RefinementTypes.WfLemmas]
Constructor Index
E
esc_subst [in RefinementTypes.EvalSubstLemmas]esc_id [in RefinementTypes.EvalSubstLemmas]
N
Neg [in RefinementTypes.Avoid]O
OpAdd [in RefinementTypes.Syntax]OpAnd [in RefinementTypes.Syntax]
OpDiv [in RefinementTypes.Syntax]
OpEq [in RefinementTypes.Syntax]
OpGe [in RefinementTypes.Syntax]
OpGt [in RefinementTypes.Syntax]
OpLe [in RefinementTypes.Syntax]
OpLt [in RefinementTypes.Syntax]
OpMod [in RefinementTypes.Syntax]
OpMul [in RefinementTypes.Syntax]
OpNeq [in RefinementTypes.Syntax]
OpOr [in RefinementTypes.Syntax]
OpSub [in RefinementTypes.Syntax]
P
Pos [in RefinementTypes.Avoid]R
rc_some_some [in RefinementTypes.EvalShiftLemmas]rc_some_none [in RefinementTypes.EvalShiftLemmas]
rc_none [in RefinementTypes.EvalShiftLemmas]
rsc_some_some [in RefinementTypes.EvalSubstLemmas]
rsc_some_none [in RefinementTypes.EvalSubstLemmas]
rsc_none [in RefinementTypes.EvalSubstLemmas]
S
SSub_Mu_Fold [in RefinementTypes.SyntacticSubtyping]SSub_Mu_Unfold [in RefinementTypes.SyntacticSubtyping]
SSub_TVar_Lower [in RefinementTypes.SyntacticSubtyping]
SSub_TVar_Upper [in RefinementTypes.SyntacticSubtyping]
SSub_Bot [in RefinementTypes.SyntacticSubtyping]
SSub_Top [in RefinementTypes.SyntacticSubtyping]
SSub_Refine [in RefinementTypes.SyntacticSubtyping]
SSub_Refine_Base [in RefinementTypes.SyntacticSubtyping]
SSub_And [in RefinementTypes.SyntacticSubtyping]
SSub_And_R [in RefinementTypes.SyntacticSubtyping]
SSub_And_L [in RefinementTypes.SyntacticSubtyping]
SSub_Or [in RefinementTypes.SyntacticSubtyping]
SSub_Or_R [in RefinementTypes.SyntacticSubtyping]
SSub_Or_L [in RefinementTypes.SyntacticSubtyping]
SSub_Sigma [in RefinementTypes.SyntacticSubtyping]
SSub_Forall [in RefinementTypes.SyntacticSubtyping]
SSub_Fun [in RefinementTypes.SyntacticSubtyping]
SSub_Trans [in RefinementTypes.SyntacticSubtyping]
SSub_Refl [in RefinementTypes.SyntacticSubtyping]
ST_MatchSum [in RefinementTypes.SyntacticTyping]
ST_Inr [in RefinementTypes.SyntacticTyping]
ST_Inl [in RefinementTypes.SyntacticTyping]
ST_MatchPair [in RefinementTypes.SyntacticTyping]
ST_Pair [in RefinementTypes.SyntacticTyping]
ST_Sub [in RefinementTypes.SyntacticTyping]
ST_Selfify [in RefinementTypes.SyntacticTyping]
ST_Loop [in RefinementTypes.SyntacticTyping]
ST_If [in RefinementTypes.SyntacticTyping]
ST_BinOp [in RefinementTypes.SyntacticTyping]
ST_Let [in RefinementTypes.SyntacticTyping]
ST_TApp [in RefinementTypes.SyntacticTyping]
ST_TAbs [in RefinementTypes.SyntacticTyping]
ST_App [in RefinementTypes.SyntacticTyping]
ST_Abs [in RefinementTypes.SyntacticTyping]
ST_Var [in RefinementTypes.SyntacticTyping]
ST_Int32 [in RefinementTypes.SyntacticTyping]
ST_Bool [in RefinementTypes.SyntacticTyping]
ST_Unit [in RefinementTypes.SyntacticTyping]
ST_Diverge [in RefinementTypes.SyntacticTyping]
T
tabs [in RefinementTypes.Syntax]TAnd [in RefinementTypes.Syntax]
tapp [in RefinementTypes.Syntax]
tbin_op [in RefinementTypes.Syntax]
tbool [in RefinementTypes.Syntax]
TBool [in RefinementTypes.Syntax]
TBot [in RefinementTypes.Syntax]
tdiverge [in RefinementTypes.Syntax]
TForall [in RefinementTypes.Syntax]
TFun [in RefinementTypes.Syntax]
tif [in RefinementTypes.Syntax]
tinl [in RefinementTypes.Syntax]
tinr [in RefinementTypes.Syntax]
tint32 [in RefinementTypes.Syntax]
TInt32 [in RefinementTypes.Syntax]
tlet [in RefinementTypes.Syntax]
tloop [in RefinementTypes.Syntax]
tmatch_sum [in RefinementTypes.Syntax]
tmatch_pair [in RefinementTypes.Syntax]
TMuAll [in RefinementTypes.Syntax]
TOr [in RefinementTypes.Syntax]
tpair [in RefinementTypes.Syntax]
TRefine [in RefinementTypes.Syntax]
TSigma [in RefinementTypes.Syntax]
TSum [in RefinementTypes.Syntax]
ttabs [in RefinementTypes.Syntax]
ttapp [in RefinementTypes.Syntax]
TTop [in RefinementTypes.Syntax]
tunit [in RefinementTypes.Syntax]
TUnit [in RefinementTypes.Syntax]
tvar [in RefinementTypes.Syntax]
TVar [in RefinementTypes.Syntax]
V
vabs [in RefinementTypes.Syntax]vbool [in RefinementTypes.Syntax]
vc_tabs [in RefinementTypes.EvalShiftLemmas]
vc_abs [in RefinementTypes.EvalShiftLemmas]
vc_inr [in RefinementTypes.EvalShiftLemmas]
vc_inl [in RefinementTypes.EvalShiftLemmas]
vc_pair [in RefinementTypes.EvalShiftLemmas]
vc_int32 [in RefinementTypes.EvalShiftLemmas]
vc_bool [in RefinementTypes.EvalShiftLemmas]
vc_unit [in RefinementTypes.EvalShiftLemmas]
vinl [in RefinementTypes.Syntax]
vinr [in RefinementTypes.Syntax]
vint32 [in RefinementTypes.Syntax]
vpair [in RefinementTypes.Syntax]
vsc_tabs [in RefinementTypes.EvalSubstLemmas]
vsc_abs [in RefinementTypes.EvalSubstLemmas]
vsc_inr [in RefinementTypes.EvalSubstLemmas]
vsc_inl [in RefinementTypes.EvalSubstLemmas]
vsc_pair [in RefinementTypes.EvalSubstLemmas]
vsc_int32 [in RefinementTypes.EvalSubstLemmas]
vsc_bool [in RefinementTypes.EvalSubstLemmas]
vsc_unit [in RefinementTypes.EvalSubstLemmas]
vtabs [in RefinementTypes.Syntax]
vunit [in RefinementTypes.Syntax]
Inductive Index
B
BinOp [in RefinementTypes.Syntax]E
env_subst_compat [in RefinementTypes.EvalSubstLemmas]P
Polarity [in RefinementTypes.Avoid]R
res_weaken_compat [in RefinementTypes.EvalShiftLemmas]res_subst_compat [in RefinementTypes.EvalSubstLemmas]
S
syn_subtype [in RefinementTypes.SyntacticSubtyping]syn_typed [in RefinementTypes.SyntacticTyping]
T
Term [in RefinementTypes.Syntax]Ty [in RefinementTypes.Syntax]
V
Value [in RefinementTypes.Syntax]val_weaken_compat [in RefinementTypes.EvalShiftLemmas]
val_subst_compat [in RefinementTypes.EvalSubstLemmas]
Section Index
V
Value_ind_nested [in RefinementTypes.Syntax]Definition Index
A
abstract_term_var [in RefinementTypes.Subst]AccTy [in RefinementTypes.Examples]
avoid [in RefinementTypes.Avoid]
avoid_var0 [in RefinementTypes.Avoid]
B
base_ty [in RefinementTypes.FirstOrder]BinOp_sind [in RefinementTypes.Syntax]
BinOp_rec [in RefinementTypes.Syntax]
BinOp_ind [in RefinementTypes.Syntax]
BinOp_rect [in RefinementTypes.Syntax]
bin_op_val_pair_compat [in RefinementTypes.Eval]
bin_op_result_ty [in RefinementTypes.FirstOrder]
bin_op_ty_compat [in RefinementTypes.FirstOrder]
bool_ty [in RefinementTypes.FirstOrder]
C
collect_tm [in RefinementTypes.ExamplesCollect]collect_ty [in RefinementTypes.ExamplesCollect]
E
env_subst_compat_sind [in RefinementTypes.EvalSubstLemmas]env_subst_compat_ind [in RefinementTypes.EvalSubstLemmas]
erase_ty_in_val [in RefinementTypes.EvalTypeErasure]
erase_ty_in_tm [in RefinementTypes.EvalTypeErasure]
eval [in RefinementTypes.Eval]
evals_to_same [in RefinementTypes.Wf]
eval_bin_op [in RefinementTypes.Eval]
eval_to_true [in RefinementTypes.Interp]
F
flip_polarity [in RefinementTypes.Avoid]fo [in RefinementTypes.FirstOrder]
fo_val [in RefinementTypes.Eval]
funcomp [in RefinementTypes.Subst]
I
interp [in RefinementTypes.Interp]interp_mu [in RefinementTypes.Interp]
interp_bot [in RefinementTypes.Interp]
interp_top [in RefinementTypes.Interp]
interp_and [in RefinementTypes.Interp]
interp_or [in RefinementTypes.Interp]
interp_sum [in RefinementTypes.Interp]
interp_sigma [in RefinementTypes.Interp]
interp_refine [in RefinementTypes.Interp]
interp_forall [in RefinementTypes.Interp]
interp_fun [in RefinementTypes.Interp]
interp_int32 [in RefinementTypes.Interp]
interp_bool [in RefinementTypes.Interp]
interp_unit [in RefinementTypes.Interp]
interp_var [in RefinementTypes.Interp]
int_le [in RefinementTypes.Examples]
int32_wrap [in RefinementTypes.Eval]
is_positive [in RefinementTypes.ExamplesCollect]
L
ListTy [in RefinementTypes.ExamplesCollect]ListTy [in RefinementTypes.Examples]
ListTy_refined [in RefinementTypes.ExamplesCollect]
ListTy_unfolded [in RefinementTypes.Examples]
list_value [in RefinementTypes.ExamplesCollect]
list_term [in RefinementTypes.ExamplesCollect]
list_term [in RefinementTypes.Examples]
M
maximum_tm [in RefinementTypes.Examples]maximum_ty [in RefinementTypes.Examples]
O
oov_map [in RefinementTypes.EvalTypeErasure]OptionTy [in RefinementTypes.Examples]
ordered [in RefinementTypes.FirstOrder]
OrderingTy [in RefinementTypes.Examples]
P
Polarity_sind [in RefinementTypes.Avoid]Polarity_rec [in RefinementTypes.Avoid]
Polarity_ind [in RefinementTypes.Avoid]
Polarity_rect [in RefinementTypes.Avoid]
R
RefinedByP [in RefinementTypes.ExamplesCollect]ren_tm_tabs_annotation [in RefinementTypes.SubstExamples]
ren_ty_refine_propagates [in RefinementTypes.SubstExamples]
ren_tm_refine_free [in RefinementTypes.SubstExamples]
ren_tm_refine_bound [in RefinementTypes.SubstExamples]
ren_ty_forall_free [in RefinementTypes.SubstExamples]
ren_ty_forall [in RefinementTypes.SubstExamples]
ren_tm_preserves_tyvar [in RefinementTypes.SubstExamples]
ren_ty_preserves_tmvar [in RefinementTypes.SubstExamples]
ren_tm_shift_tmvar [in RefinementTypes.SubstExamples]
ren_ty_shift_tvar [in RefinementTypes.SubstExamples]
ren_tm [in RefinementTypes.Subst]
ren_ty [in RefinementTypes.Subst]
ResTy [in RefinementTypes.Examples]
res_weaken_compat_sind [in RefinementTypes.EvalShiftLemmas]
res_weaken_compat_ind [in RefinementTypes.EvalShiftLemmas]
res_subst_compat_sind [in RefinementTypes.EvalSubstLemmas]
res_subst_compat_ind [in RefinementTypes.EvalSubstLemmas]
run_loop [in RefinementTypes.Eval]
S
scons [in RefinementTypes.Subst]SemTy [in RefinementTypes.Interp]
sem_terminates [in RefinementTypes.ExamplesPartialSoundness]
sem_implies [in RefinementTypes.SemanticImplies]
sem_subtype [in RefinementTypes.SemanticSubtyping]
sem_typed [in RefinementTypes.SemanticTyping]
sigma_gen [in RefinementTypes.InterpSubstLemmas]
spos [in RefinementTypes.Positivity]
spos_avoid [in RefinementTypes.AvoidLemmas]
subst_tm_preserves_tyvar [in RefinementTypes.SubstExamples]
subst_ty_preserves_tmvar [in RefinementTypes.SubstExamples]
subst_tm_id [in RefinementTypes.SubstExamples]
subst_ty_id [in RefinementTypes.SubstExamples]
subst_tm_refine_free [in RefinementTypes.SubstExamples]
subst_tm_refine_bound [in RefinementTypes.SubstExamples]
subst_tm_tabs_annotation [in RefinementTypes.SubstExamples]
subst_ty_refine_propagates [in RefinementTypes.SubstExamples]
subst_ty_forall_free_shift [in RefinementTypes.SubstExamples]
subst_ty_forall_free [in RefinementTypes.SubstExamples]
subst_ty_forall_bound [in RefinementTypes.SubstExamples]
subst_ty_other_var [in RefinementTypes.SubstExamples]
subst_ty_basic [in RefinementTypes.SubstExamples]
subst_tm [in RefinementTypes.Subst]
subst_ty [in RefinementTypes.Subst]
syn_subtype_sind [in RefinementTypes.SyntacticSubtyping]
syn_subtype_ind [in RefinementTypes.SyntacticSubtyping]
syn_typed_sind [in RefinementTypes.SyntacticTyping]
syn_typed_ind [in RefinementTypes.SyntacticTyping]
T
TBounds [in RefinementTypes.Wf]tbounds_shift_term [in RefinementTypes.Wf]
tenv_shift_type [in RefinementTypes.WfLemmas]
term_eq_dec [in RefinementTypes.Syntax]
Term_sind [in RefinementTypes.Syntax]
Term_rec [in RefinementTypes.Syntax]
Term_ind [in RefinementTypes.Syntax]
Term_rect [in RefinementTypes.Syntax]
term_has_semtype [in RefinementTypes.Interp]
term_mentions_ty [in RefinementTypes.Avoid]
term_mentions [in RefinementTypes.Avoid]
test_collect_none_ok [in RefinementTypes.ExamplesCollect]
test_collect_none [in RefinementTypes.ExamplesCollect]
test_collect_empty_ok [in RefinementTypes.ExamplesCollect]
test_collect_empty [in RefinementTypes.ExamplesCollect]
test_collect_ok [in RefinementTypes.ExamplesCollect]
test_collect [in RefinementTypes.ExamplesCollect]
test_maximum_singleton [in RefinementTypes.Examples]
test_maximum_empty [in RefinementTypes.Examples]
test_maximum_nonempty [in RefinementTypes.Examples]
tm_shift [in RefinementTypes.SubstLemmas]
typeof [in RefinementTypes.AlgorithmicTyping]
ty_var_absent [in RefinementTypes.Positivity]
ty_subst_shifts_under_tfun [in RefinementTypes.SubstExamples]
ty_subst_refine_propagates [in RefinementTypes.SubstExamples]
ty_subst_basic [in RefinementTypes.SubstExamples]
ty_eq_dec [in RefinementTypes.Syntax]
Ty_sind [in RefinementTypes.Syntax]
Ty_rec [in RefinementTypes.Syntax]
Ty_ind [in RefinementTypes.Syntax]
Ty_rect [in RefinementTypes.Syntax]
ty_subst [in RefinementTypes.Subst]
U
upn_tm [in RefinementTypes.Subst]upren [in RefinementTypes.Subst]
up_tm_tm [in RefinementTypes.Subst]
up_tm_ty [in RefinementTypes.Subst]
up_ty_tm [in RefinementTypes.Subst]
up_ty_ty [in RefinementTypes.Subst]
V
Value_ind_nested [in RefinementTypes.Syntax]Value_sind [in RefinementTypes.Syntax]
Value_rec [in RefinementTypes.Syntax]
Value_ind [in RefinementTypes.Syntax]
Value_rect [in RefinementTypes.Syntax]
val_weaken_compat_sind [in RefinementTypes.EvalShiftLemmas]
val_weaken_compat_ind [in RefinementTypes.EvalShiftLemmas]
val_subst_compat_sind [in RefinementTypes.EvalSubstLemmas]
val_subst_compat_ind [in RefinementTypes.EvalSubstLemmas]
var [in RefinementTypes.Syntax]
W
wf_benv [in RefinementTypes.Wf]wf_facts [in RefinementTypes.Wf]
wf_env [in RefinementTypes.Wf]
| 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 | (580 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 | (2 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 | (9 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 | (32 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 | (246 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 | (118 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| 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 | (1 entry) |
| 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 | (160 entries) |