| 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 | (1707 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 | (115 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 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 | (19 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 | (79 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 | (590 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 | (393 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (79 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (15 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (366 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
A
adjust_exp_eq_level [lemma, in Mcltt.Core.Semantic.Consequences]alg_type_infer_mut_ind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check_mut_ind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer_sind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer_ind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check_sind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check_ind [definition, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer [inductive, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check [inductive, in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer_pi_complete [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_typ_complete [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_complete [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_complete [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_conv [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_subtyp [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_pi_implies_alg_type_infer_pi [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_typ_implies_alg_type_infer_typ [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_normal [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_sound [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_sound [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_sound [lemma, in Mcltt.Algorithmic.Typing.Lemmas]
alg_subtyping_sound [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_complete [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_trans [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_refl [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_trans [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_sound [lemma, in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_sind [definition, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_ind [definition, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyp_run [constructor, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping [inductive, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf_sind [definition, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf_ind [definition, in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf [inductive, in Mcltt.Algorithmic.Subtyping.Definitions]
AllGood [constructor, in Mcltt.Entrypoint]
app_ctx_vlookup [lemma, in Mcltt.Core.Syntactic.Corollaries]
app_ctx_lookup [lemma, in Mcltt.Core.Syntactic.Corollaries]
ARROW [constructor, in Mcltt.Frontend.Parser]
asnf_pi [constructor, in Mcltt.Algorithmic.Subtyping.Definitions]
asnf_univ [constructor, in Mcltt.Algorithmic.Subtyping.Definitions]
asnf_refl [constructor, in Mcltt.Algorithmic.Subtyping.Definitions]
AT [constructor, in Mcltt.Frontend.Parser]
atc_ati [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_vlookup [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_app [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_fn [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_pi [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_natrec [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_succ [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_zero [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_nat [constructor, in Mcltt.Algorithmic.Typing.Definitions]
ati_typ [constructor, in Mcltt.Algorithmic.Typing.Definitions]
Aut [module, in Mcltt.Frontend.Parser]
Aut.action_table [definition, in Mcltt.Frontend.Parser]
Aut.first_nterm [definition, in Mcltt.Frontend.Parser]
Aut.goto_table [definition, in Mcltt.Frontend.Parser]
Aut.Gram [module, in Mcltt.Frontend.Parser]
Aut.GramDefs [module, in Mcltt.Frontend.Parser]
Aut.initstate [definition, in Mcltt.Frontend.Parser]
Aut.InitStateAlph [instance, in Mcltt.Frontend.Parser]
Aut.initstateNum [instance, in Mcltt.Frontend.Parser]
Aut.initstate' [inductive, in Mcltt.Frontend.Parser]
Aut.Init'0 [constructor, in Mcltt.Frontend.Parser]
Aut.items_of_state [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_51 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_50 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_49 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_48 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_46 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_45 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_44 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_43 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_42 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_41 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_40 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_39 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_38 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_37 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_36 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_35 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_34 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_33 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_32 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_31 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_30 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_29 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_28 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_27 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_26 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_25 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_24 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_23 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_22 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_21 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_20 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_19 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_18 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_17 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_16 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_15 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_14 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_13 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_12 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_11 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_10 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_9 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_8 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_7 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_6 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_5 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_4 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_3 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_2 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_1 [definition, in Mcltt.Frontend.Parser]
Aut.items_of_state_0 [definition, in Mcltt.Frontend.Parser]
Aut.last_symb_of_non_init_state [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_17 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_16 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_15 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_14 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_13 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_12 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_11 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_10 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_9 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_8 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_7 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_6 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_5 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_4 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_3 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_2 [definition, in Mcltt.Frontend.Parser]
Aut.lookahead_set_1 [definition, in Mcltt.Frontend.Parser]
Aut.Nis'1 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'10 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'11 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'12 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'13 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'14 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'15 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'16 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'17 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'18 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'19 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'2 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'20 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'21 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'22 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'23 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'24 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'25 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'26 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'27 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'28 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'29 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'3 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'30 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'31 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'32 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'33 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'34 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'35 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'36 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'37 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'38 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'39 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'4 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'40 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'41 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'42 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'43 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'44 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'45 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'46 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'48 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'49 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'5 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'50 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'51 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'6 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'7 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'8 [constructor, in Mcltt.Frontend.Parser]
Aut.Nis'9 [constructor, in Mcltt.Frontend.Parser]
Aut.noninitstate [definition, in Mcltt.Frontend.Parser]
Aut.NonInitStateAlph [instance, in Mcltt.Frontend.Parser]
Aut.noninitstateNum [instance, in Mcltt.Frontend.Parser]
Aut.noninitstate' [inductive, in Mcltt.Frontend.Parser]
Aut.nullable_nterm [definition, in Mcltt.Frontend.Parser]
Aut.N_of_state [definition, in Mcltt.Frontend.Parser]
Aut.past_state_of_non_init_state [definition, in Mcltt.Frontend.Parser]
Aut.past_symb_of_non_init_state [definition, in Mcltt.Frontend.Parser]
Aut.start_nt [definition, in Mcltt.Frontend.Parser]
Aut.state_set_37 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_36 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_35 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_34 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_33 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_32 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_31 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_30 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_29 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_28 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_27 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_26 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_25 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_24 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_23 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_22 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_21 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_20 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_19 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_18 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_17 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_16 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_15 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_14 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_13 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_12 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_11 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_10 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_9 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_8 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_7 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_6 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_5 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_4 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_3 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_2 [definition, in Mcltt.Frontend.Parser]
Aut.state_set_1 [definition, in Mcltt.Frontend.Parser]
a_extend [constructor, in Mcltt.Core.Syntactic.Syntax]
a_compose [constructor, in Mcltt.Core.Syntactic.Syntax]
a_weaken [constructor, in Mcltt.Core.Syntactic.Syntax]
a_id [constructor, in Mcltt.Core.Syntactic.Syntax]
a_sub [constructor, in Mcltt.Core.Syntactic.Syntax]
a_var [constructor, in Mcltt.Core.Syntactic.Syntax]
a_app [constructor, in Mcltt.Core.Syntactic.Syntax]
a_fn [constructor, in Mcltt.Core.Syntactic.Syntax]
a_pi [constructor, in Mcltt.Core.Syntactic.Syntax]
a_natrec [constructor, in Mcltt.Core.Syntactic.Syntax]
a_succ [constructor, in Mcltt.Core.Syntactic.Syntax]
a_zero [constructor, in Mcltt.Core.Syntactic.Syntax]
a_nat [constructor, in Mcltt.Core.Syntactic.Syntax]
a_typ [constructor, in Mcltt.Core.Syntactic.Syntax]
B
BAR [constructor, in Mcltt.Frontend.Parser]Base [library]
C
ca_natrec [constructor, in Mcltt.Frontend.Elaborator]ca_succ [constructor, in Mcltt.Frontend.Elaborator]
ca_type [constructor, in Mcltt.Frontend.Elaborator]
ca_zero [constructor, in Mcltt.Frontend.Elaborator]
ca_nat [constructor, in Mcltt.Frontend.Elaborator]
ca_app [constructor, in Mcltt.Frontend.Elaborator]
ca_pi [constructor, in Mcltt.Frontend.Elaborator]
ca_lam [constructor, in Mcltt.Frontend.Elaborator]
ca_var [constructor, in Mcltt.Frontend.Elaborator]
closed_at_sind [definition, in Mcltt.Frontend.Elaborator]
closed_at_ind [definition, in Mcltt.Frontend.Elaborator]
closed_at [inductive, in Mcltt.Frontend.Elaborator]
COLON [constructor, in Mcltt.Frontend.Parser]
COMMA [constructor, in Mcltt.Frontend.Parser]
complete [lemma, in Mcltt.Frontend.Parser]
completeness [lemma, in Mcltt.Core.Completeness]
Completeness [library]
completeness_fundamental_ctx_eq [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_subtyp [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub_eq [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp_eq [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx_subtyp [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [lemma, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [section, in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_ty [lemma, in Mcltt.Core.Completeness]
Consequences [library]
cons_glu_sub_pred_pi_helper [lemma, in Mcltt.Core.Soundness.FunctionCases]
cons_glu_sub_pred [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
cons_glu_sub_pred_q_nat_helper [lemma, in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_q_helper [lemma, in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_nat_helper [lemma, in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_helper [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_resp_wf_sub_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
ContextCases [library]
ContextCases [library]
Core [library]
CoreInversions [library]
CoreLemmas [library]
CoreTactics [library]
CoreTactics [library]
CoreTypeInversions [library]
Corollaries [library]
Cst [module, in Mcltt.Core.Syntactic.Syntax]
cst_variables [definition, in Mcltt.Frontend.Elaborator]
Cst.app [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.fn [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.nat [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.natrec [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.obj [inductive, in Mcltt.Core.Syntactic.Syntax]
Cst.obj_sind [definition, in Mcltt.Core.Syntactic.Syntax]
Cst.obj_rec [definition, in Mcltt.Core.Syntactic.Syntax]
Cst.obj_ind [definition, in Mcltt.Core.Syntactic.Syntax]
Cst.obj_rect [definition, in Mcltt.Core.Syntactic.Syntax]
Cst.pi [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.succ [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.typ [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.var [constructor, in Mcltt.Core.Syntactic.Syntax]
Cst.zero [constructor, in Mcltt.Core.Syntactic.Syntax]
ctx [abbreviation, in Mcltt.Core.Syntactic.Syntax]
CtxEq [library]
ctxeq_nbe_ty_eq' [lemma, in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_ty_eq [lemma, in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq' [lemma, in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq [lemma, in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_ctx_lookup [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctxeq_subtyp [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctxeq_sub_eq [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctxeq_sub [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctxeq_exp_eq [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctxeq_exp [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctxeq_weakening [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
CtxSub [library]
ctxsub_judg.ctxsub_subtyp [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_subtyp_helper [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq_helper [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_helper [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq_helper [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_helper [lemma, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg [module, in Mcltt.Core.Syntactic.CtxSub]
ctxsub_weakening [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
ctx_lookup_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
ctx_lookup_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
ctx_lookup [inductive, in Mcltt.Core.Syntactic.System.Definitions]
ctx_sub_ctx_lookup [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctx_lookup_wf [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
ctx_eq_trans [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctx_eq_sym [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctx_eq_refl [lemma, in Mcltt.Core.Syntactic.CtxEq]
ctx_lookup_functional [lemma, in Mcltt.Core.Syntactic.Corollaries]
ctx_sub_refl [lemma, in Mcltt.Core.Syntactic.CtxSub]
D
DARROW [constructor, in Mcltt.Frontend.Parser]Definition [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
domain [inductive, in Mcltt.Core.Semantic.Domain]
Domain [library]
domain:_ ↯ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:_ ↦ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:⇑! _ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:⇓ _ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:⇑ _ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:! _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:rec _ under _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:succ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:zero (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:Π _ _ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:𝕌 @ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:ℕ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:_ _ .. _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:λ _ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:_ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:~ _ (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
domain:( _ ) (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
d{{{ _ }}} (mcltt_scope) [notation, in Mcltt.Core.Semantic.Domain]
Domain_Notations [module, in Mcltt.Core.Semantic.Domain]
domain_nf_sind [definition, in Mcltt.Core.Semantic.Domain]
domain_nf_rec [definition, in Mcltt.Core.Semantic.Domain]
domain_nf_ind [definition, in Mcltt.Core.Semantic.Domain]
domain_nf_rect [definition, in Mcltt.Core.Semantic.Domain]
domain_ne_sind [definition, in Mcltt.Core.Semantic.Domain]
domain_ne_rec [definition, in Mcltt.Core.Semantic.Domain]
domain_ne_ind [definition, in Mcltt.Core.Semantic.Domain]
domain_ne_rect [definition, in Mcltt.Core.Semantic.Domain]
domain_sind [definition, in Mcltt.Core.Semantic.Domain]
domain_rec [definition, in Mcltt.Core.Semantic.Domain]
domain_ind [definition, in Mcltt.Core.Semantic.Domain]
domain_rect [definition, in Mcltt.Core.Semantic.Domain]
domain_nf [inductive, in Mcltt.Core.Semantic.Domain]
domain_ne [inductive, in Mcltt.Core.Semantic.Domain]
domain_app_per [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
drop_env_extend_env_cancel [lemma, in Mcltt.Core.Semantic.Domain]
drop_env [definition, in Mcltt.Core.Semantic.Domain]
d_dom [constructor, in Mcltt.Core.Semantic.Domain]
d_natrec [constructor, in Mcltt.Core.Semantic.Domain]
d_app [constructor, in Mcltt.Core.Semantic.Domain]
d_var [constructor, in Mcltt.Core.Semantic.Domain]
d_neut [constructor, in Mcltt.Core.Semantic.Domain]
d_fn [constructor, in Mcltt.Core.Semantic.Domain]
d_succ [constructor, in Mcltt.Core.Semantic.Domain]
d_zero [constructor, in Mcltt.Core.Semantic.Domain]
d_univ [constructor, in Mcltt.Core.Semantic.Domain]
d_pi [constructor, in Mcltt.Core.Semantic.Domain]
d_nat [constructor, in Mcltt.Core.Semantic.Domain]
E
eao_neut [constructor, in Mcltt.Extraction.Evaluation]eao_fn [constructor, in Mcltt.Extraction.Evaluation]
eeo_sub [constructor, in Mcltt.Extraction.Evaluation]
eeo_app [constructor, in Mcltt.Extraction.Evaluation]
eeo_fn [constructor, in Mcltt.Extraction.Evaluation]
eeo_pi [constructor, in Mcltt.Extraction.Evaluation]
eeo_natrec [constructor, in Mcltt.Extraction.Evaluation]
eeo_succ [constructor, in Mcltt.Extraction.Evaluation]
eeo_zero [constructor, in Mcltt.Extraction.Evaluation]
eeo_nat [constructor, in Mcltt.Extraction.Evaluation]
eeo_var [constructor, in Mcltt.Extraction.Evaluation]
eeo_typ [constructor, in Mcltt.Extraction.Evaluation]
elaborate [definition, in Mcltt.Frontend.Elaborator]
ElaborationFailure [constructor, in Mcltt.Entrypoint]
Elaborator [library]
elaborator_gives_user_exp [lemma, in Mcltt.Frontend.Elaborator]
empty_env [definition, in Mcltt.Core.Semantic.Domain]
END [constructor, in Mcltt.Frontend.Parser]
eno_neut [constructor, in Mcltt.Extraction.Evaluation]
eno_succ [constructor, in Mcltt.Extraction.Evaluation]
eno_zero [constructor, in Mcltt.Extraction.Evaluation]
Entrypoint [library]
EOF [constructor, in Mcltt.Frontend.Parser]
eso_compose [constructor, in Mcltt.Extraction.Evaluation]
eso_extend [constructor, in Mcltt.Extraction.Evaluation]
eso_weaken [constructor, in Mcltt.Extraction.Evaluation]
eso_id [constructor, in Mcltt.Extraction.Evaluation]
Evaluation [library]
Evaluation [library]
eval_natrec_sub_rel [lemma, in Mcltt.Core.Completeness.NatCases]
eval_natrec_rel [lemma, in Mcltt.Core.Completeness.NatCases]
eval_natrec_neut [lemma, in Mcltt.Core.Completeness.NatCases]
eval_natrec_sub_neut [lemma, in Mcltt.Core.Completeness.NatCases]
eval_sub_impl_complete [lemma, in Mcltt.Extraction.Evaluation]
eval_app_impl_complete [lemma, in Mcltt.Extraction.Evaluation]
eval_natrec_impl_complete [lemma, in Mcltt.Extraction.Evaluation]
eval_exp_impl_complete [lemma, in Mcltt.Extraction.Evaluation]
eval_sub_impl [definition, in Mcltt.Extraction.Evaluation]
eval_app_impl [definition, in Mcltt.Extraction.Evaluation]
eval_natrec_impl [definition, in Mcltt.Extraction.Evaluation]
eval_exp_impl [definition, in Mcltt.Extraction.Evaluation]
eval_sub_order_sound [lemma, in Mcltt.Extraction.Evaluation]
eval_app_order_sound [lemma, in Mcltt.Extraction.Evaluation]
eval_natrec_order_sound [lemma, in Mcltt.Extraction.Evaluation]
eval_exp_order_sound [lemma, in Mcltt.Extraction.Evaluation]
eval_sub_order_sind [definition, in Mcltt.Extraction.Evaluation]
eval_sub_order_ind [definition, in Mcltt.Extraction.Evaluation]
eval_app_order_sind [definition, in Mcltt.Extraction.Evaluation]
eval_app_order_ind [definition, in Mcltt.Extraction.Evaluation]
eval_natrec_order_sind [definition, in Mcltt.Extraction.Evaluation]
eval_natrec_order_ind [definition, in Mcltt.Extraction.Evaluation]
eval_exp_order_sind [definition, in Mcltt.Extraction.Evaluation]
eval_exp_order_ind [definition, in Mcltt.Extraction.Evaluation]
eval_sub_order [inductive, in Mcltt.Extraction.Evaluation]
eval_app_order [inductive, in Mcltt.Extraction.Evaluation]
eval_natrec_order [inductive, in Mcltt.Extraction.Evaluation]
eval_exp_order [inductive, in Mcltt.Extraction.Evaluation]
eval_sub_mut_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_mut_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_mut_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_mut_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_sind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_sind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_sind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_sind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_ind [definition, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_compose [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_extend [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_weaken [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_id [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub [inductive, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_neut [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_fn [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app [inductive, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_neut [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_succ [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_zero [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec [inductive, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_sub [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_app [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_fn [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_pi [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_natrec [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_succ [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_zero [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_nat [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_var [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_typ [constructor, in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp [inductive, in Mcltt.Core.Semantic.Evaluation.Definitions]
exp [inductive, in Mcltt.Core.Syntactic.Syntax]
ExpNoConfusion [library]
exp_eq_typ_implies_eq_level [lemma, in Mcltt.Core.Completeness.Consequences.Types]
exp_eq_var_1_sub_q_sigma_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_nat_helper [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub_to_nat_sub [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat2 [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat1 [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_typ_helper [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_typ_sub_sub [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ2' [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ1 [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_trans_typ_max [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_refl [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
exp_to_num [definition, in Mcltt.Core.Syntactic.Syntax]
exp_to_nat [definition, in Mcltt.Core.Syntactic.Syntax]
exp_sind [definition, in Mcltt.Core.Syntactic.Syntax]
exp_rec [definition, in Mcltt.Core.Syntactic.Syntax]
exp_ind [definition, in Mcltt.Core.Syntactic.Syntax]
exp_rect [definition, in Mcltt.Core.Syntactic.Syntax]
exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_sub_decompose_double_q_with_id_double_extend [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_var_sub_rhs_typ_gen [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_pi_eta_rhs_body [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_pi_sub_rhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_pi_sub_lhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_nat_beta_succ_rhs_typ_gen [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_sub_cong_typ2 [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_rhs_typ [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_lhs_typ_gen [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_natrec_cong_rhs_typ [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_succ_sub_rhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_succ_sub_lhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_zero_sub_lhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_nat_sub_lhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_typ_sub_lhs [lemma, in Mcltt.Core.Syntactic.Corollaries]
exp_eq_pi_inversion [lemma, in Mcltt.Core.Semantic.Consequences]
extend_env [definition, in Mcltt.Core.Semantic.Domain]
F
functional_alg_type_infer [lemma, in Mcltt.Algorithmic.Typing.Lemmas]functional_glu_univ_elem [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
functional_read_typ [lemma, in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read_ne [lemma, in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read_nf [lemma, in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read [lemma, in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read [section, in Mcltt.Core.Semantic.Readback.Lemmas]
functional_ctx_lookup [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
functional_nbe_ty [lemma, in Mcltt.Core.Semantic.NbE]
functional_nbe_of_typ [lemma, in Mcltt.Core.Semantic.NbE]
functional_nbe [lemma, in Mcltt.Core.Semantic.NbE]
functional_initial_env [lemma, in Mcltt.Core.Semantic.NbE]
functional_eval_sub [lemma, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_app [lemma, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_natrec [lemma, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_exp [lemma, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval [lemma, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval [section, in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_glu_ctx_env [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
FunctionCases [library]
FunctionCases [library]
FundamentalTheorem [library]
FundamentalTheorem [library]
G
get_subterms_of_pi_nf [definition, in Mcltt.Extraction.TypeCheck]get_level_of_type_nf [definition, in Mcltt.Extraction.TypeCheck]
Gluing [section, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction [section, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_neut [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_pi [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_nat [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_univ [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.motive [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gluing.glu_univ_typ_rec [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gluing.i [variable, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_ctx_extend [lemma, in Mcltt.Core.Soundness.ContextCases]
glu_rel_ctx_empty [lemma, in Mcltt.Core.Soundness.ContextCases]
glu_rel_exp_app [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_app_helper [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_fn [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_fn_helper [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_of_pi [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_pi [lemma, in Mcltt.Core.Soundness.FunctionCases]
glu_rel_sub [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_ctx [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_sub_with_sub [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_with_sub [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_sind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_ind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_cons [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_nil [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_typ_with_sub [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top_make [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top_make [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot_make [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_ind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_typ [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_sind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_ind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_neut [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_pi [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_nat [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_univ [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_sind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_ind [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_neut [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_succ [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_zero [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_exp_monotone [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_monotone [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion2 [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion1 [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_simple_constructor [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_core_univ' [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_exp_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_univ_lvl [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_typ [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_elem [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_univ [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk' [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_ctx_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_ctx_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_typ_exp_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_exp_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_lvl [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_readback [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_exp_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_ctx_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_per_nat [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_rel_exp_natrec [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_helper [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_neut_helper [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_succ_helper [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_zero_helper [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_sub_extend_nat [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_succ [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_zero [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_of_nat [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_clean_inversion2'' [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_sub_nat [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_nat [lemma, in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_sub [lemma, in Mcltt.Core.Soundness.TermStructureCases]
glu_rel_exp_vlookup [lemma, in Mcltt.Core.Soundness.TermStructureCases]
glu_rel_exp_sub_typ [lemma, in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_clean_inversion2' [lemma, in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_typ [lemma, in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_of_typ [lemma, in Mcltt.Core.Soundness.UniverseCases]
glu_rel_sub_wf_sub [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion3 [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion2 [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion1 [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_to_wf_exp [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion2 [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion2_result [definition, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion1 [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_monotone [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_subtyp_sub_if [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_cons_clean_inversion [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_resp_per_ctx_helper [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_ctx_env [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_wf_ctx [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_env [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_sub_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_ctx_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_conv [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_if [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_typ_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_right [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_left [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_right [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_left [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_ge [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_right [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_left [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_ge [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity_ge [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity [section, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_right [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_left [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_ge [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_iff [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_elem_typ_escape [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq' [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq_ge [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_extend [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_compose [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_weaken [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_id [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_conv [lemma, in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv [lemma, in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_sub_subtyp [lemma, in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_exp_subtyp [lemma, in Mcltt.Core.Soundness.SubtypingCases]
Gram [module, in Mcltt.Frontend.Parser]
Gram.app_obj'nt [constructor, in Mcltt.Frontend.Parser]
Gram.ARROW't [constructor, in Mcltt.Frontend.Parser]
Gram.atomic_obj'nt [constructor, in Mcltt.Frontend.Parser]
Gram.AT't [constructor, in Mcltt.Frontend.Parser]
Gram.BAR't [constructor, in Mcltt.Frontend.Parser]
Gram.COLON't [constructor, in Mcltt.Frontend.Parser]
Gram.COMMA't [constructor, in Mcltt.Frontend.Parser]
Gram.DARROW't [constructor, in Mcltt.Frontend.Parser]
Gram.END't [constructor, in Mcltt.Frontend.Parser]
Gram.EOF't [constructor, in Mcltt.Frontend.Parser]
Gram.fnbinder'nt [constructor, in Mcltt.Frontend.Parser]
Gram.INT't [constructor, in Mcltt.Frontend.Parser]
Gram.LAMBDA't [constructor, in Mcltt.Frontend.Parser]
Gram.LPAREN't [constructor, in Mcltt.Frontend.Parser]
Gram.NAT't [constructor, in Mcltt.Frontend.Parser]
Gram.nonterminal [definition, in Mcltt.Frontend.Parser]
Gram.NonTerminalAlph [instance, in Mcltt.Frontend.Parser]
Gram.nonterminalNum [instance, in Mcltt.Frontend.Parser]
Gram.nonterminal_semantic_type [definition, in Mcltt.Frontend.Parser]
Gram.nonterminal' [inductive, in Mcltt.Frontend.Parser]
Gram.obj'nt [constructor, in Mcltt.Frontend.Parser]
Gram.params'nt [constructor, in Mcltt.Frontend.Parser]
Gram.param'nt [constructor, in Mcltt.Frontend.Parser]
Gram.PI't [constructor, in Mcltt.Frontend.Parser]
Gram.production [definition, in Mcltt.Frontend.Parser]
Gram.ProductionAlph [instance, in Mcltt.Frontend.Parser]
Gram.productionNum [instance, in Mcltt.Frontend.Parser]
Gram.production' [inductive, in Mcltt.Frontend.Parser]
Gram.prod_action [definition, in Mcltt.Frontend.Parser]
Gram.prod_rhs_rev [definition, in Mcltt.Frontend.Parser]
Gram.prod_lhs [definition, in Mcltt.Frontend.Parser]
Gram.prod_contents [definition, in Mcltt.Frontend.Parser]
Gram.Prod'app_obj'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'app_obj'1 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'1 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'2 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'3 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'4 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'5 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'fnbinder'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'fnbinder'1 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'obj'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'obj'1 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'obj'2 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'obj'3 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'params'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'params'1 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'param'0 [constructor, in Mcltt.Frontend.Parser]
Gram.Prod'prog'0 [constructor, in Mcltt.Frontend.Parser]
Gram.prog'nt [constructor, in Mcltt.Frontend.Parser]
Gram.REC't [constructor, in Mcltt.Frontend.Parser]
Gram.RETURN't [constructor, in Mcltt.Frontend.Parser]
Gram.RPAREN't [constructor, in Mcltt.Frontend.Parser]
Gram.SUCC't [constructor, in Mcltt.Frontend.Parser]
Gram.symbol_semantic_type [definition, in Mcltt.Frontend.Parser]
Gram.terminal [definition, in Mcltt.Frontend.Parser]
Gram.TerminalAlph [instance, in Mcltt.Frontend.Parser]
Gram.terminalNum [instance, in Mcltt.Frontend.Parser]
Gram.terminal_semantic_type [definition, in Mcltt.Frontend.Parser]
Gram.terminal' [inductive, in Mcltt.Frontend.Parser]
Gram.token [definition, in Mcltt.Frontend.Parser]
Gram.token_sem [definition, in Mcltt.Frontend.Parser]
Gram.token_term [definition, in Mcltt.Frontend.Parser]
Gram.TYPE't [constructor, in Mcltt.Frontend.Parser]
Gram.VAR't [constructor, in Mcltt.Frontend.Parser]
Gram.ZERO't [constructor, in Mcltt.Frontend.Parser]
H
here [constructor, in Mcltt.Core.Syntactic.System.Definitions]I
idempotent_nbe_ty [lemma, in Mcltt.Core.Semantic.Consequences]ie_cons [constructor, in Mcltt.Extraction.NbE]
ie_nil [constructor, in Mcltt.Extraction.NbE]
InitialEnvImpl [section, in Mcltt.Extraction.NbE]
initial_env_sind [definition, in Mcltt.Core.Semantic.NbE]
initial_env_ind [definition, in Mcltt.Core.Semantic.NbE]
initial_env_cons [constructor, in Mcltt.Core.Semantic.NbE]
initial_env_nil [constructor, in Mcltt.Core.Semantic.NbE]
initial_env [inductive, in Mcltt.Core.Semantic.NbE]
initial_env_impl_complete [lemma, in Mcltt.Extraction.NbE]
initial_env_impl [definition, in Mcltt.Extraction.NbE]
initial_env_order_sound [lemma, in Mcltt.Extraction.NbE]
initial_env_order_sind [definition, in Mcltt.Extraction.NbE]
initial_env_order_ind [definition, in Mcltt.Extraction.NbE]
initial_env_order [inductive, in Mcltt.Extraction.NbE]
initial_env_glu_rel_exp [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
inspect [definition, in Mcltt.Entrypoint]
INT [constructor, in Mcltt.Frontend.Parser]
Inversions [library]
invert_compose_id [lemma, in Mcltt.Core.Syntactic.Corollaries]
invert_sub_id_typ [lemma, in Mcltt.Core.Syntactic.Corollaries]
invert_sub_id [lemma, in Mcltt.Core.Syntactic.Corollaries]
is_typ_constr_and_exp_eq_nat_implies_eq_nat [lemma, in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_typ_implies_eq_typ [lemma, in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr_sind [definition, in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr_ind [definition, in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr [inductive, in Mcltt.Core.Completeness.Consequences.Types]
L
LAMBDA [constructor, in Mcltt.Frontend.Parser]Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
LibTactics [library]
lift_exp_eq_max_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_eq_max_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_eq_ge [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_max_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_max_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_ge [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
lift_nbe_max_right [lemma, in Mcltt.Core.Semantic.NbE]
lift_nbe_max_left [lemma, in Mcltt.Core.Semantic.NbE]
lift_nbe_ge [lemma, in Mcltt.Core.Semantic.NbE]
loc [axiom, in Mcltt.Frontend.Parser]
LogicalRelation [library]
LogicalRelation [library]
lookup [definition, in Mcltt.Extraction.TypeCheck]
lookup [section, in Mcltt.Extraction.TypeCheck]
lookup [definition, in Mcltt.Frontend.Elaborator]
lookup_bound [lemma, in Mcltt.Frontend.Elaborator]
lookup_known [lemma, in Mcltt.Frontend.Elaborator]
LPAREN [constructor, in Mcltt.Frontend.Parser]
M
main [definition, in Mcltt.Entrypoint]main_result [inductive, in Mcltt.Entrypoint]
MenhirLibParser [module, in Mcltt.Frontend.Parser]
mk_glu_rel_sub_with_sub [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_exp_with_sub [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_cons_glu_sub_pred [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_typ_with_sub [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_exp_pred [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_typ_pred [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_neut_glu_exp_pred [constructor, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_rel_sub [constructor, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_exp [constructor, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_mod_app [constructor, in Mcltt.Core.Semantic.PER.Definitions]
mk_rel_mod_eval [constructor, in Mcltt.Core.Semantic.PER.Definitions]
mk_glu_rel_exp_with_sub'' [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_exp_with_sub' [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub'' [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub' [lemma, in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
N
NAT [constructor, in Mcltt.Frontend.Parser]NatCases [library]
NatCases [library]
nat_is_typ_constr [constructor, in Mcltt.Core.Completeness.Consequences.Types]
nat_glu_exp_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
nat_glu_typ_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
nat_to_exp [definition, in Mcltt.Core.Syntactic.Syntax]
nbe [inductive, in Mcltt.Core.Semantic.NbE]
NbE [library]
NbE [library]
NbEDef [section, in Mcltt.Extraction.NbE]
NbETyDef [section, in Mcltt.Extraction.NbE]
nbe_type_to_nbe_ty [lemma, in Mcltt.Core.Semantic.NbE]
nbe_ty_sind [definition, in Mcltt.Core.Semantic.NbE]
nbe_ty_ind [definition, in Mcltt.Core.Semantic.NbE]
nbe_ty_run [constructor, in Mcltt.Core.Semantic.NbE]
nbe_ty [inductive, in Mcltt.Core.Semantic.NbE]
nbe_cumu [lemma, in Mcltt.Core.Semantic.NbE]
nbe_sind [definition, in Mcltt.Core.Semantic.NbE]
nbe_ind [definition, in Mcltt.Core.Semantic.NbE]
nbe_run [constructor, in Mcltt.Core.Semantic.NbE]
nbe_ty_impl_complete [lemma, in Mcltt.Extraction.NbE]
nbe_ty_impl [definition, in Mcltt.Extraction.NbE]
nbe_ty_order_sound [lemma, in Mcltt.Extraction.NbE]
nbe_ty_order_sind [definition, in Mcltt.Extraction.NbE]
nbe_ty_order_rec [definition, in Mcltt.Extraction.NbE]
nbe_ty_order_ind [definition, in Mcltt.Extraction.NbE]
nbe_ty_order_rect [definition, in Mcltt.Extraction.NbE]
nbe_ty_order_run [constructor, in Mcltt.Extraction.NbE]
nbe_ty_order [inductive, in Mcltt.Extraction.NbE]
nbe_impl_complete [lemma, in Mcltt.Extraction.NbE]
nbe_impl [definition, in Mcltt.Extraction.NbE]
nbe_order_sound [lemma, in Mcltt.Extraction.NbE]
nbe_order_sind [definition, in Mcltt.Extraction.NbE]
nbe_order_rec [definition, in Mcltt.Extraction.NbE]
nbe_order_ind [definition, in Mcltt.Extraction.NbE]
nbe_order_rect [definition, in Mcltt.Extraction.NbE]
nbe_order_run [constructor, in Mcltt.Extraction.NbE]
nbe_order [inductive, in Mcltt.Extraction.NbE]
ne [inductive, in Mcltt.Core.Syntactic.Syntax]
neut_glu_exp_pred [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
neut_glu_typ_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
ne_eq_dec [lemma, in Mcltt.Core.Syntactic.Syntax]
ne_to_exp [definition, in Mcltt.Core.Syntactic.Syntax]
ne_sind [definition, in Mcltt.Core.Syntactic.Syntax]
ne_rec [definition, in Mcltt.Core.Syntactic.Syntax]
ne_ind [definition, in Mcltt.Core.Syntactic.Syntax]
ne_rect [definition, in Mcltt.Core.Syntactic.Syntax]
ne_var [constructor, in Mcltt.Core.Syntactic.Syntax]
ne_app [constructor, in Mcltt.Core.Syntactic.Syntax]
ne_natrec [constructor, in Mcltt.Core.Syntactic.Syntax]
nf [inductive, in Mcltt.Core.Syntactic.Syntax]
nf_eq_dec [lemma, in Mcltt.Core.Syntactic.Syntax]
nf_to_exp [definition, in Mcltt.Core.Syntactic.Syntax]
nf_sind [definition, in Mcltt.Core.Syntactic.Syntax]
nf_rec [definition, in Mcltt.Core.Syntactic.Syntax]
nf_ind [definition, in Mcltt.Core.Syntactic.Syntax]
nf_rect [definition, in Mcltt.Core.Syntactic.Syntax]
nf_neut [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_fn [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_pi [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_succ [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_zero [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_nat [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_typ [constructor, in Mcltt.Core.Syntactic.Syntax]
nf_of_pi [lemma, in Mcltt.Core.Semantic.Consequences]
nil_glu_sub_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
not_univ_pi [definition, in Mcltt.Algorithmic.Subtyping.Definitions]
num_to_exp [definition, in Mcltt.Core.Syntactic.Syntax]
P
Parser [library]ParserFailure [constructor, in Mcltt.Entrypoint]
ParserTimeout [constructor, in Mcltt.Entrypoint]
PER [library]
PERElem [record, in Mcltt.LibTactics]
PERElem [inductive, in Mcltt.LibTactics]
PERProper [instance, in Mcltt.LibTactics]
per_ctx_then_per_env_initial_env [lemma, in Mcltt.Core.Semantic.Realizability]
per_elem_then_per_top [lemma, in Mcltt.Core.Semantic.Realizability]
per_bot_then_per_elem [lemma, in Mcltt.Core.Semantic.Realizability]
per_univ_then_per_top_typ [lemma, in Mcltt.Core.Semantic.Realizability]
per_nat_then_per_top [lemma, in Mcltt.Core.Semantic.Realizability]
per_univ_elem_glu_univ_elem [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
per_univ_glu_univ_elem [lemma, in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
per_elem [projection, in Mcltt.LibTactics]
per_elem [constructor, in Mcltt.LibTactics]
PER_refl2 [lemma, in Mcltt.LibTactics]
PER_refl1 [lemma, in Mcltt.LibTactics]
per_ctx_subtyp_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_cons [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_nil [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp [inductive, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_cons [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_nil [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env [inductive, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_pi [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_univ [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_nat [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_neut [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp [inductive, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_ind' [definition, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_ne [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_Pi [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_N [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_U [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.motive [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def [section, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ' [lemma, in Mcltt.Core.Semantic.PER.Definitions]
per_univ [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_strong_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_ne [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Pi [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_nat [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_U [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.motive [variable, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_neut [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_pi [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_nat [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core [inductive, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.per_univ_rec [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.i [variable, in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def [section, in Mcltt.Core.Semantic.PER.Definitions]
per_ne_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ne_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ne_neut [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_ne [inductive, in Mcltt.Core.Semantic.PER.Definitions]
per_nat_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_nat_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_nat_neut [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_nat_succ [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_nat_zero [constructor, in Mcltt.Core.Semantic.PER.Definitions]
per_nat [inductive, in Mcltt.Core.Semantic.PER.Definitions]
per_top_typ [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_top [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_bot [definition, in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_trans_ins [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl2 [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl1 [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_subtyping [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_to_env [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_respects_length [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons_clean_inversion [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons' [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_env_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_env_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cross_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_left_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_env_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_right_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_right [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_left [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_transp [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_trans_ins [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_refl2 [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_refl1 [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_subtyping_gen [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_subtyping [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_to_univ_elem [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_right [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_left [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_ge [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi_clean_inversion [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi' [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_PER' [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_trans' [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cross_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_left_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_sym' [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_right_irrel [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_then_per_top [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_top_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_PER [instance, in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_trans [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_sym [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
PI [constructor, in Mcltt.Frontend.Parser]
pi_is_typ_constr [constructor, in Mcltt.Core.Completeness.Consequences.Types]
pi_glu_exp_pred [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
pi_glu_typ_pred [inductive, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
predicate_implication_equivalence [instance, in Mcltt.LibTactics]
Presup [library]
presup_subtyp_right [lemma, in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub_right [lemma, in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub_left [lemma, in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub [lemma, in Mcltt.Core.Syntactic.System.Definitions]
presup_rel_sub [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
presup_exp_eq_ctx [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_exp_ctx [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_right [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_left [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
presup_typ_glu_rel_exp [lemma, in Mcltt.Core.Soundness.TermStructureCases]
presup_ctx_glu_rel_exp [lemma, in Mcltt.Core.Soundness.TermStructureCases]
presup_glu_rel_exp [lemma, in Mcltt.Core.Soundness.TermStructureCases]
presup_subtyp [lemma, in Mcltt.Core.Syntactic.Presup]
presup_sub_eq [lemma, in Mcltt.Core.Syntactic.Presup]
presup_exp_eq [lemma, in Mcltt.Core.Syntactic.Presup]
presup_exp [lemma, in Mcltt.Core.Syntactic.Presup]
presup_rel_exp [lemma, in Mcltt.Core.Completeness.TermStructureCases]
presup_right_glu_rel_sub [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
presup_left_glu_rel_sub [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
presup_glu_rel_sub [lemma, in Mcltt.Core.Soundness.SubstitutionCases]
prog [definition, in Mcltt.Frontend.Parser]
prog_complete [lemma, in Mcltt.Frontend.Parser]
prog_correct [lemma, in Mcltt.Frontend.Parser]
PseudoMonadic [library]
Q
q [definition, in Mcltt.Core.Syntactic.Syntax]R
Readback [library]Readback [library]
read_typ_impl_complete [lemma, in Mcltt.Extraction.Readback]
read_ne_impl_complete [lemma, in Mcltt.Extraction.Readback]
read_nf_impl_complete [lemma, in Mcltt.Extraction.Readback]
read_typ_impl [definition, in Mcltt.Extraction.Readback]
read_ne_impl [definition, in Mcltt.Extraction.Readback]
read_nf_impl [definition, in Mcltt.Extraction.Readback]
read_typ_order_sound [lemma, in Mcltt.Extraction.Readback]
read_ne_order_sound [lemma, in Mcltt.Extraction.Readback]
read_nf_order_sound [lemma, in Mcltt.Extraction.Readback]
read_typ_order_sind [definition, in Mcltt.Extraction.Readback]
read_typ_order_ind [definition, in Mcltt.Extraction.Readback]
read_ne_order_sind [definition, in Mcltt.Extraction.Readback]
read_ne_order_ind [definition, in Mcltt.Extraction.Readback]
read_nf_order_sind [definition, in Mcltt.Extraction.Readback]
read_nf_order_ind [definition, in Mcltt.Extraction.Readback]
read_typ_order [inductive, in Mcltt.Extraction.Readback]
read_ne_order [inductive, in Mcltt.Extraction.Readback]
read_nf_order [inductive, in Mcltt.Extraction.Readback]
read_typ_mut_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_mut_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_mut_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_sind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_sind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_sind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_ind [definition, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_neut [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_pi [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_nat [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_univ [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_typ [inductive, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_natrec [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_app [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_var [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_ne [inductive, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_neut [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_fn [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_nat_neut [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_succ [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_zero [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_type [constructor, in Mcltt.Core.Semantic.Readback.Definitions]
read_nf [inductive, in Mcltt.Core.Semantic.Readback.Definitions]
Realizability [library]
Realizability [library]
realize_glu_elem_top [lemma, in Mcltt.Core.Soundness.Realizability]
realize_glu_elem_bot [lemma, in Mcltt.Core.Soundness.Realizability]
realize_glu_typ_top [lemma, in Mcltt.Core.Soundness.Realizability]
realize_glu_univ_elem_gen [lemma, in Mcltt.Core.Soundness.Realizability]
realize_per_univ_elem_gen [lemma, in Mcltt.Core.Semantic.Realizability]
REC [constructor, in Mcltt.Frontend.Parser]
rel_exp_nat_beta_succ [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_beta_succ_rel_typ [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_beta_zero [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_sub [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_sub_rel_typ [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_cong [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_cong_rel_typ [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_N [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_wkwk_succ_var1_inversion [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero_inversion [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_succ_cong [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_succ_sub [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_zero_sub [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_sub [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_nat [lemma, in Mcltt.Core.Completeness.NatCases]
rel_exp_of_nat_inversion [lemma, in Mcltt.Core.Completeness.NatCases]
rel_typ_implies_rel_exp [lemma, in Mcltt.Core.Completeness.LogicalRelation.Lemmas]
rel_exp_implies_rel_typ [lemma, in Mcltt.Core.Completeness.LogicalRelation.Lemmas]
rel_sub_under_ctx [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_sind [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_ind [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub [inductive, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_under_ctx [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_sind [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_ind [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp [inductive, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_eq_subtyp [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_conv [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_PER [instance, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_trans [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_sym [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_p_extend [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend_compose [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_compose_assoc [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_left [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_right [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend_cong [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_compose_cong [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_weaken [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id [lemma, in Mcltt.Core.Completeness.SubstitutionCases]
rel_exp_cumu [lemma, in Mcltt.Core.Completeness.UniverseCases]
rel_exp_typ_sub [lemma, in Mcltt.Core.Completeness.UniverseCases]
rel_exp_of_typ [lemma, in Mcltt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion [lemma, in Mcltt.Core.Completeness.UniverseCases]
rel_typ [definition, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_app_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_app_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_app [inductive, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval_sind [definition, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval_ind [definition, in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval [inductive, in Mcltt.Core.Semantic.PER.Definitions]
rel_ctx_sub_extend [lemma, in Mcltt.Core.Completeness.ContextCases]
rel_ctx_sub_empty [lemma, in Mcltt.Core.Completeness.ContextCases]
rel_ctx_extend' [lemma, in Mcltt.Core.Completeness.ContextCases]
rel_ctx_extend [lemma, in Mcltt.Core.Completeness.ContextCases]
rel_exp_pi_eta [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_beta [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_app_sub [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_app_cong [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_fn_sub [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_fn_cong [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_sub [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_cong [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_core [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_of_pi [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_of_pi_inversion [lemma, in Mcltt.Core.Completeness.FunctionCases]
rel_exp_var_weaken [lemma, in Mcltt.Core.Completeness.VariableCases]
rel_exp_var_S_sub [lemma, in Mcltt.Core.Completeness.VariableCases]
rel_exp_var_0_sub [lemma, in Mcltt.Core.Completeness.VariableCases]
rel_exp_eq_subtyp [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_PER [instance, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_trans [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sym [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_conv [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_compose [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_id [lemma, in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_cong [lemma, in Mcltt.Core.Completeness.TermStructureCases]
RETURN [constructor, in Mcltt.Frontend.Parser]
rne_natrec [constructor, in Mcltt.Extraction.Readback]
rne_app [constructor, in Mcltt.Extraction.Readback]
rne_var [constructor, in Mcltt.Extraction.Readback]
rnf_neut [constructor, in Mcltt.Extraction.Readback]
rnf_fn [constructor, in Mcltt.Extraction.Readback]
rnf_nat_neut [constructor, in Mcltt.Extraction.Readback]
rnf_succ [constructor, in Mcltt.Extraction.Readback]
rnf_zero [constructor, in Mcltt.Extraction.Readback]
rnf_type [constructor, in Mcltt.Extraction.Readback]
RPAREN [constructor, in Mcltt.Frontend.Parser]
rtyp_neut [constructor, in Mcltt.Extraction.Readback]
rtyp_pi [constructor, in Mcltt.Extraction.Readback]
rtyp_nat [constructor, in Mcltt.Extraction.Readback]
rtyp_univ [constructor, in Mcltt.Extraction.Readback]
Rules [library]
S
safe [lemma, in Mcltt.Frontend.Parser]soundness [lemma, in Mcltt.Core.Soundness]
Soundness [library]
soundness_fundamental_sub [lemma, in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_exp [lemma, in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_ctx [lemma, in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [lemma, in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [section, in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_ty' [lemma, in Mcltt.Core.Soundness]
soundness_ty [lemma, in Mcltt.Core.Soundness]
soundness' [lemma, in Mcltt.Core.Soundness]
StrSet [module, in Mcltt.Frontend.Elaborator]
StrSProp [module, in Mcltt.Frontend.Elaborator]
sub [inductive, in Mcltt.Core.Syntactic.Syntax]
Subset_to_In [lemma, in Mcltt.Frontend.Elaborator]
SubstitutionCases [library]
SubstitutionCases [library]
Subtyping [library]
SubtypingCases [library]
SubtypingCases [library]
subtyping_impl_complete [lemma, in Mcltt.Extraction.Subtyping]
subtyping_impl_complete' [lemma, in Mcltt.Extraction.Subtyping]
subtyping_impl [definition, in Mcltt.Extraction.Subtyping]
subtyping_order_sound [lemma, in Mcltt.Extraction.Subtyping]
subtyping_order_sind [definition, in Mcltt.Extraction.Subtyping]
subtyping_order_rec [definition, in Mcltt.Extraction.Subtyping]
subtyping_order_ind [definition, in Mcltt.Extraction.Subtyping]
subtyping_order_rect [definition, in Mcltt.Extraction.Subtyping]
subtyping_order_run [constructor, in Mcltt.Extraction.Subtyping]
subtyping_order [inductive, in Mcltt.Extraction.Subtyping]
subtyping_nf_impl_complete [lemma, in Mcltt.Extraction.Subtyping]
subtyping_nf_impl [definition, in Mcltt.Extraction.Subtyping]
subtyp_under_ctx [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
subtyp_pi [lemma, in Mcltt.Core.Completeness.SubtypingCases]
subtyp_univ [lemma, in Mcltt.Core.Completeness.SubtypingCases]
subtyp_Transitive [instance, in Mcltt.Core.Completeness.SubtypingCases]
subtyp_trans [lemma, in Mcltt.Core.Completeness.SubtypingCases]
subtyp_refl [lemma, in Mcltt.Core.Completeness.SubtypingCases]
sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_p_q_q_sigma_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_id_extend [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_sigma_compose_weak_id_extend [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_compose_sigma [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_nat_compose_sigma [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_weak_compose_weak_extend_succ_var_1 [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_extend_zero [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_q_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_q_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_q [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_id_extend [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_extend [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_on_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_extend_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_wk_var0_id [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_extend_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_refl [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
sub_sind [definition, in Mcltt.Core.Syntactic.Syntax]
sub_rec [definition, in Mcltt.Core.Syntactic.Syntax]
sub_ind [definition, in Mcltt.Core.Syntactic.Syntax]
sub_rect [definition, in Mcltt.Core.Syntactic.Syntax]
sub_eq_q_compose_nat [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_eq_q_compose [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_eq_p_q_sigma_compose_tau_extend [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_decompose_q_typ [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_decompose_q [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_q_eq [lemma, in Mcltt.Core.Syntactic.Corollaries]
sub_id_typ [lemma, in Mcltt.Core.Syntactic.Corollaries]
SUCC [constructor, in Mcltt.Frontend.Parser]
sumbool_sumor_failable_bind [definition, in Mcltt.Extraction.PseudoMonadic]
sumbool_failable_bind [definition, in Mcltt.Extraction.PseudoMonadic]
sumor_sumbool_failable_bind [definition, in Mcltt.Extraction.PseudoMonadic]
sumor_failable_bind [definition, in Mcltt.Extraction.PseudoMonadic]
Syntax [library]
nf:⇑ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:# _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:rec _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:succ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:zero (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:Π _ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:Type @ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:ℕ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:_ _ .. _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:~ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:⋅ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:q _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ ,, _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ ∘ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:Wk (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:Id (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:# _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:rec _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:succ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:zero (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:Π _ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:Type @ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:ℕ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ _ .. _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:~ _ (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [notation, in Mcltt.Core.Syntactic.Syntax]
Syntax_Notations [module, in Mcltt.Core.Syntactic.Syntax]
System [library]
SystemOpt [library]
T
Tactics [library]Tactics [library]
Tactics [library]
tc_ti [constructor, in Mcltt.Extraction.TypeCheck]
TermStructureCases [library]
TermStructureCases [library]
test_elab2 [definition, in Mcltt.Frontend.Elaborator]
test_elab [definition, in Mcltt.Frontend.Elaborator]
there [constructor, in Mcltt.Core.Syntactic.System.Definitions]
ti_vlookup [constructor, in Mcltt.Extraction.TypeCheck]
ti_app [constructor, in Mcltt.Extraction.TypeCheck]
ti_fn [constructor, in Mcltt.Extraction.TypeCheck]
ti_pi [constructor, in Mcltt.Extraction.TypeCheck]
ti_natrec [constructor, in Mcltt.Extraction.TypeCheck]
ti_succ [constructor, in Mcltt.Extraction.TypeCheck]
ti_zero [constructor, in Mcltt.Extraction.TypeCheck]
ti_nat [constructor, in Mcltt.Extraction.TypeCheck]
ti_typ [constructor, in Mcltt.Extraction.TypeCheck]
token [inductive, in Mcltt.Frontend.Parser]
typ [abbreviation, in Mcltt.Core.Syntactic.Syntax]
TYPE [constructor, in Mcltt.Frontend.Parser]
TypeCheck [library]
TypeCheckingFailure [constructor, in Mcltt.Entrypoint]
Types [library]
type_check_closed_complete [lemma, in Mcltt.Extraction.TypeCheck]
type_check_closed [definition, in Mcltt.Extraction.TypeCheck]
type_check_closed [section, in Mcltt.Extraction.TypeCheck]
type_infer_complete [lemma, in Mcltt.Extraction.TypeCheck]
type_check_complete' [lemma, in Mcltt.Extraction.TypeCheck]
type_check_order_soundness [lemma, in Mcltt.Extraction.TypeCheck]
type_infer_order_soundness [lemma, in Mcltt.Extraction.TypeCheck]
type_infer [definition, in Mcltt.Extraction.TypeCheck]
type_check [definition, in Mcltt.Extraction.TypeCheck]
type_infer_order_sind [definition, in Mcltt.Extraction.TypeCheck]
type_infer_order_ind [definition, in Mcltt.Extraction.TypeCheck]
type_check_order_sind [definition, in Mcltt.Extraction.TypeCheck]
type_check_order_ind [definition, in Mcltt.Extraction.TypeCheck]
type_infer_order [inductive, in Mcltt.Extraction.TypeCheck]
type_check_order [inductive, in Mcltt.Extraction.TypeCheck]
type_check [section, in Mcltt.Extraction.TypeCheck]
typ_is_typ_constr [constructor, in Mcltt.Core.Completeness.Consequences.Types]
U
UniverseCases [library]UniverseCases [library]
univ_glu_exp_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_exp_pred' [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_typ_pred [definition, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
user_exp_to_type_infer_order [lemma, in Mcltt.Extraction.TypeCheck]
user_exp_ne [lemma, in Mcltt.Frontend.Elaborator]
user_exp_nf [lemma, in Mcltt.Frontend.Elaborator]
user_exp_sind [definition, in Mcltt.Frontend.Elaborator]
user_exp_ind [definition, in Mcltt.Frontend.Elaborator]
user_exp_vlookup [constructor, in Mcltt.Frontend.Elaborator]
user_exp_app [constructor, in Mcltt.Frontend.Elaborator]
user_exp_fn [constructor, in Mcltt.Frontend.Elaborator]
user_exp_pi [constructor, in Mcltt.Frontend.Elaborator]
user_exp_natrec [constructor, in Mcltt.Frontend.Elaborator]
user_exp_succ [constructor, in Mcltt.Frontend.Elaborator]
user_exp_zero [constructor, in Mcltt.Frontend.Elaborator]
user_exp_nat [constructor, in Mcltt.Frontend.Elaborator]
user_exp_typ [constructor, in Mcltt.Frontend.Elaborator]
user_exp [inductive, in Mcltt.Frontend.Elaborator]
V
valid_exp_zero [lemma, in Mcltt.Core.Completeness.NatCases]valid_exp_nat [lemma, in Mcltt.Core.Completeness.NatCases]
valid_sub_under_ctx [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
valid_exp_under_ctx [definition, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
valid_exp_typ [lemma, in Mcltt.Core.Completeness.UniverseCases]
valid_ctx [definition, in Mcltt.Core.Semantic.PER.Definitions]
valid_ctx_empty [lemma, in Mcltt.Core.Completeness.ContextCases]
valid_exp_var [lemma, in Mcltt.Core.Completeness.VariableCases]
valid_lookup [lemma, in Mcltt.Core.Completeness.VariableCases]
VAR [constructor, in Mcltt.Frontend.Parser]
VariableCases [library]
var_glu_elem_bot [lemma, in Mcltt.Core.Soundness.Realizability]
var_weaken_gen [lemma, in Mcltt.Core.Soundness.Realizability]
var_arith [lemma, in Mcltt.Core.Soundness.Realizability]
var_per_elem [lemma, in Mcltt.Core.Semantic.Realizability]
var_per_bot [lemma, in Mcltt.Core.Semantic.PER.Lemmas]
var0_glu_elem [lemma, in Mcltt.Core.Soundness.Realizability]
version_check [definition, in Mcltt.Frontend.Parser]
vlookup_1_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_0_nat [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_1_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_0_typ [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
W
weakening [inductive, in Mcltt.Core.Soundness.Weakening.Definition]Weakening [library]
weakening_sind [definition, in Mcltt.Core.Soundness.Weakening.Definition]
weakening_ind [definition, in Mcltt.Core.Soundness.Weakening.Definition]
weakening_wk [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_id [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_compose [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_conv [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_resp_equiv [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_escape [lemma, in Mcltt.Core.Soundness.Weakening.Lemmas]
well_scoped [lemma, in Mcltt.Frontend.Elaborator]
wf_sub_extend_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_compose_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_weaken_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_id_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_exp_sub_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_vlookup_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_app_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_fn_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_natrec_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_succ_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_zero_inversion [lemma, in Mcltt.Core.Syntactic.CoreInversions]
wf_ctx_sub_ctx_lookup [lemma, in Mcltt.Core.Soundness.Realizability]
wf_sub_eq_per_elem [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_per_elem [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp' [lemma, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp' [lemma, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_subtyp' [lemma, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_subtyp' [lemma, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_Transitive [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_Symmetric [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_PER [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_PER [instance, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_empty [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind' [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind' [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind' [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_ind [definition, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_pi [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_univ [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_trans [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_refl [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_trans [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_sym [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_p_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_compose [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_assoc [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_left [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_right [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_weaken [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_trans [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sym [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_compose [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_id [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_weaken [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_S_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_0_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_eta [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_beta [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_succ [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_zero [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_cong [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_zero_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_typ_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_subtyp [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_compose [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_weaken [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_id [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_sub [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_subtyp [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_sub [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_vlookup [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_app [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_fn [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_pi [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_natrec [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_succ [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_zero [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_nat [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_typ [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_exp [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_empty [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_extend [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_empty [constructor, in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx [inductive, in Mcltt.Core.Syntactic.System.Definitions]
wf_pi_inversion' [lemma, in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_pi_inversion [lemma, in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_nat_inversion [lemma, in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_typ_inversion [lemma, in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_subtyp_univ_weaken [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_sub [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_ge [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_refl [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_sub_eq_conv [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_exp_eq_cumu [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_exp_eq_conv [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_sub_conv [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_cumu [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_conv [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_ctx_sub_refl [lemma, in Mcltt.Core.Syntactic.System.Lemmas]
wf_ctx_PER [instance, in Mcltt.Core.Syntactic.CtxEq]
wf_subtyp_subst [lemma, in Mcltt.Core.Syntactic.Corollaries]
wf_subtyp_subst_eq [lemma, in Mcltt.Core.Syntactic.Corollaries]
wf_ctx_sub_length [lemma, in Mcltt.Core.Syntactic.Corollaries]
wf_subtyp_pi' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_eta' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_beta' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_sub' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_cong' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_sub' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_cong' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong_max [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_sub_max [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_succ' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_zero' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_sub' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_cong' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_sub' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_typ_sub' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_app' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_fn' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_pi_max [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_natrec' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_nat' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_ctx_eq_extend' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_conv' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_conv' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_subtyp_refl' [lemma, in Mcltt.Core.Syntactic.SystemOpt]
wf_ctx_sub_trans_ins [instance, in Mcltt.Core.Syntactic.CtxSub]
wf_ctx_sub_trans [lemma, in Mcltt.Core.Syntactic.CtxSub]
wk_p [constructor, in Mcltt.Core.Soundness.Weakening.Definition]
wk_id [constructor, in Mcltt.Core.Soundness.Weakening.Definition]
Z
ZERO [constructor, in Mcltt.Frontend.Parser]_
__mark__ [definition, in Mcltt.LibTactics]other
judg:⊢ _ ≈ _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]judg:_ ⊢ _ ⊆ _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ ≈ _ : _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ≈ _ : _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ : _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ : _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:⊢ _ ⊆ _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:⊢ _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:# _ : _ ∈ _ (type_scope) [notation, in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢a _ ⟹ _ (type_scope) [notation, in Mcltt.Algorithmic.Typing.Definitions]
judg:_ ⊢a _ ⟸ _ (type_scope) [notation, in Mcltt.Algorithmic.Typing.Definitions]
judg:_ ⊢w _ : _ (type_scope) [notation, in Mcltt.Core.Soundness.Weakening.Definition]
judg:SubE _ <: _ (type_scope) [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:Sub _ <: _ at _ (type_scope) [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:Rtyp _ in _ ↘ _ (type_scope) [notation, in Mcltt.Core.Semantic.Readback.Definitions]
judg:Rne _ in _ ↘ _ (type_scope) [notation, in Mcltt.Core.Semantic.Readback.Definitions]
judg:Rnf _ in _ ↘ _ (type_scope) [notation, in Mcltt.Core.Semantic.Readback.Definitions]
judg:_ ⊢a _ ⊆ _ (type_scope) [notation, in Mcltt.Algorithmic.Subtyping.Definitions]
judg:⊢anf _ ⊆ _ (type_scope) [notation, in Mcltt.Algorithmic.Subtyping.Definitions]
judg:_ ⊩s _ : _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊩ _ : _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢s _ ® _ ∈ _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ : _ ® _ ∈ _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ ® _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊨s _ : _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨s _ ≈ _ : _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ : _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ⊆ _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ≈ _ : _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:DF _ ≈ _ ∈ _ ↘ _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:DG _ ∈ _ ↘ _ ↘ _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:Dom _ ≈ _ ∈ _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:EF _ ≈ _ ∈ _ ↘ _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:EG _ ∈ _ ↘ _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:Exp _ ≈ _ ∈ _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
judg:rec _ ⟦return _ | zero -> _ | succ -> _ end⟧ _ ↘ _ [notation, in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:$| _ & _ |↘ _ [notation, in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:⊨ _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:⊨ _ ≈ _ [notation, in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:⊩ _ [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:⟦ _ ⟧s _ ↘ _ [notation, in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:⟦ _ ⟧ _ ↘ _ [notation, in Mcltt.Core.Semantic.Evaluation.Definitions]
_ [<=] _ [notation, in Mcltt.Frontend.Elaborator]
_ <~> _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
_ ~> _ [notation, in Mcltt.Core.Semantic.PER.Definitions]
env [notation, in Mcltt.Core.Semantic.Domain]
glu_sub_pred_equivalence [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred_args [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_equivalence [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_args [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_equivalence [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_args [notation, in Mcltt.Core.Soundness.LogicalRelation.Definitions]
let*b _ := _ while _ in _ [notation, in Mcltt.Extraction.PseudoMonadic]
let*b->o _ := _ while _ in _ [notation, in Mcltt.Extraction.PseudoMonadic]
let*o _ := _ while _ in _ [notation, in Mcltt.Extraction.PseudoMonadic]
let*o->b _ := _ while _ in _ [notation, in Mcltt.Extraction.PseudoMonadic]
pureb _ [notation, in Mcltt.Extraction.PseudoMonadic]
pureo _ [notation, in Mcltt.Extraction.PseudoMonadic]
{{ _ }} [notation, in Mcltt.Core.Base]
Notation Index
D
domain:_ ↯ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]domain:_ ↦ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:⇑! _ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:⇓ _ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:⇑ _ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:! _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:rec _ under _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:succ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:zero (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:Π _ _ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:𝕌 @ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:ℕ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:_ _ .. _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:λ _ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:_ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:~ _ (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
domain:( _ ) (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
d{{{ _ }}} (mcltt_scope) [in Mcltt.Core.Semantic.Domain]
S
nf:⇑ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]nf:# _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:rec _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:succ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:zero (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:Π _ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:Type @ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:ℕ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:_ _ .. _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:~ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:⋅ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:q _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ ,, _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ ∘ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:Wk (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:Id (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:# _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:rec _ return _ | zero -> _ | succ -> _ end (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:succ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:zero (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:Π _ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:Type @ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:ℕ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ _ .. _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:~ _ (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [in Mcltt.Core.Syntactic.Syntax]
other
judg:⊢ _ ≈ _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]judg:_ ⊢ _ ⊆ _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ ≈ _ : _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ≈ _ : _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ : _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ : _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:⊢ _ ⊆ _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:⊢ _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:# _ : _ ∈ _ (type_scope) [in Mcltt.Core.Syntactic.System.Definitions]
judg:_ ⊢a _ ⟹ _ (type_scope) [in Mcltt.Algorithmic.Typing.Definitions]
judg:_ ⊢a _ ⟸ _ (type_scope) [in Mcltt.Algorithmic.Typing.Definitions]
judg:_ ⊢w _ : _ (type_scope) [in Mcltt.Core.Soundness.Weakening.Definition]
judg:SubE _ <: _ (type_scope) [in Mcltt.Core.Semantic.PER.Definitions]
judg:Sub _ <: _ at _ (type_scope) [in Mcltt.Core.Semantic.PER.Definitions]
judg:Rtyp _ in _ ↘ _ (type_scope) [in Mcltt.Core.Semantic.Readback.Definitions]
judg:Rne _ in _ ↘ _ (type_scope) [in Mcltt.Core.Semantic.Readback.Definitions]
judg:Rnf _ in _ ↘ _ (type_scope) [in Mcltt.Core.Semantic.Readback.Definitions]
judg:_ ⊢a _ ⊆ _ (type_scope) [in Mcltt.Algorithmic.Subtyping.Definitions]
judg:⊢anf _ ⊆ _ (type_scope) [in Mcltt.Algorithmic.Subtyping.Definitions]
judg:_ ⊩s _ : _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊩ _ : _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢s _ ® _ ∈ _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ : _ ® _ ∈ _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ ® _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊨s _ : _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨s _ ≈ _ : _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ : _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ⊆ _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ≈ _ : _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:DF _ ≈ _ ∈ _ ↘ _ [in Mcltt.Core.Semantic.PER.Definitions]
judg:DG _ ∈ _ ↘ _ ↘ _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:Dom _ ≈ _ ∈ _ [in Mcltt.Core.Semantic.PER.Definitions]
judg:EF _ ≈ _ ∈ _ ↘ _ [in Mcltt.Core.Semantic.PER.Definitions]
judg:EG _ ∈ _ ↘ _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:Exp _ ≈ _ ∈ _ [in Mcltt.Core.Semantic.PER.Definitions]
judg:rec _ ⟦return _ | zero -> _ | succ -> _ end⟧ _ ↘ _ [in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:$| _ & _ |↘ _ [in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:⊨ _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:⊨ _ ≈ _ [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
judg:⊩ _ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
judg:⟦ _ ⟧s _ ↘ _ [in Mcltt.Core.Semantic.Evaluation.Definitions]
judg:⟦ _ ⟧ _ ↘ _ [in Mcltt.Core.Semantic.Evaluation.Definitions]
_ [<=] _ [in Mcltt.Frontend.Elaborator]
_ <~> _ [in Mcltt.Core.Semantic.PER.Definitions]
_ ~> _ [in Mcltt.Core.Semantic.PER.Definitions]
env [in Mcltt.Core.Semantic.Domain]
glu_sub_pred_equivalence [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred_args [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_equivalence [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_args [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_equivalence [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_args [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
let*b _ := _ while _ in _ [in Mcltt.Extraction.PseudoMonadic]
let*b->o _ := _ while _ in _ [in Mcltt.Extraction.PseudoMonadic]
let*o _ := _ while _ in _ [in Mcltt.Extraction.PseudoMonadic]
let*o->b _ := _ while _ in _ [in Mcltt.Extraction.PseudoMonadic]
pureb _ [in Mcltt.Extraction.PseudoMonadic]
pureo _ [in Mcltt.Extraction.PseudoMonadic]
{{ _ }} [in Mcltt.Core.Base]
Module Index
A
Aut [in Mcltt.Frontend.Parser]Aut.Gram [in Mcltt.Frontend.Parser]
Aut.GramDefs [in Mcltt.Frontend.Parser]
C
Cst [in Mcltt.Core.Syntactic.Syntax]ctxsub_judg [in Mcltt.Core.Syntactic.CtxSub]
D
Domain_Notations [in Mcltt.Core.Semantic.Domain]G
Gram [in Mcltt.Frontend.Parser]M
MenhirLibParser [in Mcltt.Frontend.Parser]S
StrSet [in Mcltt.Frontend.Elaborator]StrSProp [in Mcltt.Frontend.Elaborator]
Syntax_Notations [in Mcltt.Core.Syntactic.Syntax]
Variable Index
G
GluingInduction.case_neut [in Mcltt.Core.Soundness.LogicalRelation.Definitions]GluingInduction.case_pi [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_nat [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_univ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.motive [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gluing.glu_univ_typ_rec [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gluing.i [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
P
Per_univ_elem_ind_def.case_ne [in Mcltt.Core.Semantic.PER.Definitions]Per_univ_elem_ind_def.case_Pi [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_N [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_U [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.motive [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_ne [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Pi [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_nat [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_U [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.motive [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.per_univ_rec [in Mcltt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.i [in Mcltt.Core.Semantic.PER.Definitions]
Library Index
B
BaseC
CompletenessConsequences
ContextCases
ContextCases
Core
CoreInversions
CoreLemmas
CoreTactics
CoreTactics
CoreTypeInversions
Corollaries
CtxEq
CtxSub
D
DefinitionDefinitions
Definitions
Definitions
Definitions
Definitions
Definitions
Definitions
Definitions
Domain
E
ElaboratorEntrypoint
Evaluation
Evaluation
ExpNoConfusion
F
FunctionCasesFunctionCases
FundamentalTheorem
FundamentalTheorem
I
InversionsL
LemmasLemmas
Lemmas
Lemmas
Lemmas
Lemmas
Lemmas
Lemmas
Lemmas
LibTactics
LogicalRelation
LogicalRelation
N
NatCasesNatCases
NbE
NbE
P
ParserPER
Presup
PseudoMonadic
R
ReadbackReadback
Realizability
Realizability
Rules
S
SoundnessSubstitutionCases
SubstitutionCases
Subtyping
SubtypingCases
SubtypingCases
Syntax
System
SystemOpt
T
TacticsTactics
Tactics
TermStructureCases
TermStructureCases
TypeCheck
Types
U
UniverseCasesUniverseCases
V
VariableCasesW
WeakeningLemma Index
A
adjust_exp_eq_level [in Mcltt.Core.Semantic.Consequences]alg_type_infer_pi_complete [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_typ_complete [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_complete [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_complete [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_conv [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_subtyp [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_pi_implies_alg_type_infer_pi [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_typ_implies_alg_type_infer_typ [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_normal [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_infer_sound [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_check_sound [in Mcltt.Algorithmic.Typing.Lemmas]
alg_type_sound [in Mcltt.Algorithmic.Typing.Lemmas]
alg_subtyping_sound [in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_complete [in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_trans [in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_refl [in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_trans [in Mcltt.Algorithmic.Subtyping.Lemmas]
alg_subtyping_nf_sound [in Mcltt.Algorithmic.Subtyping.Lemmas]
app_ctx_vlookup [in Mcltt.Core.Syntactic.Corollaries]
app_ctx_lookup [in Mcltt.Core.Syntactic.Corollaries]
C
complete [in Mcltt.Frontend.Parser]completeness [in Mcltt.Core.Completeness]
completeness_fundamental_ctx_eq [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_subtyp [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub_eq [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp_eq [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx_subtyp [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [in Mcltt.Core.Completeness.FundamentalTheorem]
completeness_ty [in Mcltt.Core.Completeness]
cons_glu_sub_pred_pi_helper [in Mcltt.Core.Soundness.FunctionCases]
cons_glu_sub_pred_q_nat_helper [in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_q_helper [in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_nat_helper [in Mcltt.Core.Soundness.NatCases]
cons_glu_sub_pred_helper [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_resp_wf_sub_eq [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
ctxeq_nbe_ty_eq' [in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_ty_eq [in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq' [in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq [in Mcltt.Core.Completeness.Consequences.Rules]
ctxeq_ctx_lookup [in Mcltt.Core.Syntactic.System.Lemmas]
ctxeq_subtyp [in Mcltt.Core.Syntactic.CtxEq]
ctxeq_sub_eq [in Mcltt.Core.Syntactic.CtxEq]
ctxeq_sub [in Mcltt.Core.Syntactic.CtxEq]
ctxeq_exp_eq [in Mcltt.Core.Syntactic.CtxEq]
ctxeq_exp [in Mcltt.Core.Syntactic.CtxEq]
ctxeq_weakening [in Mcltt.Core.Soundness.Weakening.Lemmas]
ctxsub_judg.ctxsub_subtyp [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_subtyp_helper [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq_helper [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_helper [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq_helper [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_helper [in Mcltt.Core.Syntactic.CtxSub]
ctxsub_weakening [in Mcltt.Core.Soundness.Weakening.Lemmas]
ctx_sub_ctx_lookup [in Mcltt.Core.Syntactic.System.Lemmas]
ctx_lookup_wf [in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp_right [in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp_left [in Mcltt.Core.Syntactic.System.Lemmas]
ctx_decomp [in Mcltt.Core.Syntactic.System.Lemmas]
ctx_eq_trans [in Mcltt.Core.Syntactic.CtxEq]
ctx_eq_sym [in Mcltt.Core.Syntactic.CtxEq]
ctx_eq_refl [in Mcltt.Core.Syntactic.CtxEq]
ctx_lookup_functional [in Mcltt.Core.Syntactic.Corollaries]
ctx_sub_refl [in Mcltt.Core.Syntactic.CtxSub]
D
domain_app_per [in Mcltt.Core.Semantic.PER.Lemmas]drop_env_extend_env_cancel [in Mcltt.Core.Semantic.Domain]
E
elaborator_gives_user_exp [in Mcltt.Frontend.Elaborator]eval_natrec_sub_rel [in Mcltt.Core.Completeness.NatCases]
eval_natrec_rel [in Mcltt.Core.Completeness.NatCases]
eval_natrec_neut [in Mcltt.Core.Completeness.NatCases]
eval_natrec_sub_neut [in Mcltt.Core.Completeness.NatCases]
eval_sub_impl_complete [in Mcltt.Extraction.Evaluation]
eval_app_impl_complete [in Mcltt.Extraction.Evaluation]
eval_natrec_impl_complete [in Mcltt.Extraction.Evaluation]
eval_exp_impl_complete [in Mcltt.Extraction.Evaluation]
eval_sub_order_sound [in Mcltt.Extraction.Evaluation]
eval_app_order_sound [in Mcltt.Extraction.Evaluation]
eval_natrec_order_sound [in Mcltt.Extraction.Evaluation]
eval_exp_order_sound [in Mcltt.Extraction.Evaluation]
exp_eq_typ_implies_eq_level [in Mcltt.Core.Completeness.Consequences.Types]
exp_eq_var_1_sub_q_sigma_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_nat_helper [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub_to_nat_sub [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat2 [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat1 [in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_nat [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_typ_helper [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_typ_sub_sub [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ2' [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ1 [in Mcltt.Core.Syntactic.System.Lemmas]
exp_sub_typ [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_trans_typ_max [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_refl [in Mcltt.Core.Syntactic.System.Lemmas]
exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 [in Mcltt.Core.Syntactic.Corollaries]
exp_sub_decompose_double_q_with_id_double_extend [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_var_sub_rhs_typ_gen [in Mcltt.Core.Syntactic.Corollaries]
exp_pi_eta_rhs_body [in Mcltt.Core.Syntactic.Corollaries]
exp_pi_sub_rhs [in Mcltt.Core.Syntactic.Corollaries]
exp_pi_sub_lhs [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_nat_beta_succ_rhs_typ_gen [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_sub_cong_typ2 [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_rhs_typ [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_lhs_typ_gen [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_natrec_cong_rhs_typ [in Mcltt.Core.Syntactic.Corollaries]
exp_succ_sub_rhs [in Mcltt.Core.Syntactic.Corollaries]
exp_succ_sub_lhs [in Mcltt.Core.Syntactic.Corollaries]
exp_zero_sub_lhs [in Mcltt.Core.Syntactic.Corollaries]
exp_nat_sub_lhs [in Mcltt.Core.Syntactic.Corollaries]
exp_typ_sub_lhs [in Mcltt.Core.Syntactic.Corollaries]
exp_eq_pi_inversion [in Mcltt.Core.Semantic.Consequences]
F
functional_alg_type_infer [in Mcltt.Algorithmic.Typing.Lemmas]functional_glu_univ_elem [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
functional_read_typ [in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read_ne [in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read_nf [in Mcltt.Core.Semantic.Readback.Lemmas]
functional_read [in Mcltt.Core.Semantic.Readback.Lemmas]
functional_ctx_lookup [in Mcltt.Core.Syntactic.System.Lemmas]
functional_nbe_ty [in Mcltt.Core.Semantic.NbE]
functional_nbe_of_typ [in Mcltt.Core.Semantic.NbE]
functional_nbe [in Mcltt.Core.Semantic.NbE]
functional_initial_env [in Mcltt.Core.Semantic.NbE]
functional_eval_sub [in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_app [in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_natrec [in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval_exp [in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_eval [in Mcltt.Core.Semantic.Evaluation.Lemmas]
functional_glu_ctx_env [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
G
glu_rel_ctx_extend [in Mcltt.Core.Soundness.ContextCases]glu_rel_ctx_empty [in Mcltt.Core.Soundness.ContextCases]
glu_rel_exp_app [in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_app_helper [in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_fn [in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_fn_helper [in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_of_pi [in Mcltt.Core.Soundness.FunctionCases]
glu_rel_exp_pi [in Mcltt.Core.Soundness.FunctionCases]
glu_univ_elem_exp_monotone [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_monotone [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion2 [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion1 [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_simple_constructor [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_core_univ' [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_exp_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_univ_lvl [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_typ [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_elem [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_univ [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_escape [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk' [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_ctx_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_ctx_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_typ_exp_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_exp_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_lvl [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_readback [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_exp_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_ctx_eq [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_escape [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_per_nat [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_rel_exp_natrec [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_helper [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_neut_helper [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_succ_helper [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_natrec_zero_helper [in Mcltt.Core.Soundness.NatCases]
glu_rel_sub_extend_nat [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_succ [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_zero [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_of_nat [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_clean_inversion2'' [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_sub_nat [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_nat [in Mcltt.Core.Soundness.NatCases]
glu_rel_exp_sub [in Mcltt.Core.Soundness.TermStructureCases]
glu_rel_exp_vlookup [in Mcltt.Core.Soundness.TermStructureCases]
glu_rel_exp_sub_typ [in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_clean_inversion2' [in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_typ [in Mcltt.Core.Soundness.UniverseCases]
glu_rel_exp_of_typ [in Mcltt.Core.Soundness.UniverseCases]
glu_rel_sub_wf_sub [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion3 [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion2 [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion1 [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_to_wf_exp [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion2 [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion1 [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_monotone [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_subtyp_sub_if [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_cons_clean_inversion [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_resp_per_ctx_helper [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_ctx_env [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_escape [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_wf_ctx [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_env [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_sub_eq [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_ctx_eq [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_conv [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_if [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_typ_escape [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_right [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_left [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_right [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_left [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_ge [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_right [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_left [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_ge [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity_ge [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_right [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_left [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_ge [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_iff [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_escape [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_elem_typ_escape [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq' [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq_ge [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_extend [in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_compose [in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_weaken [in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_id [in Mcltt.Core.Soundness.SubstitutionCases]
glu_rel_sub_conv [in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv [in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_sub_subtyp [in Mcltt.Core.Soundness.SubtypingCases]
glu_rel_exp_subtyp [in Mcltt.Core.Soundness.SubtypingCases]
I
idempotent_nbe_ty [in Mcltt.Core.Semantic.Consequences]initial_env_impl_complete [in Mcltt.Extraction.NbE]
initial_env_order_sound [in Mcltt.Extraction.NbE]
initial_env_glu_rel_exp [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
invert_compose_id [in Mcltt.Core.Syntactic.Corollaries]
invert_sub_id_typ [in Mcltt.Core.Syntactic.Corollaries]
invert_sub_id [in Mcltt.Core.Syntactic.Corollaries]
is_typ_constr_and_exp_eq_nat_implies_eq_nat [in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_typ_implies_eq_typ [in Mcltt.Core.Completeness.Consequences.Types]
L
lift_exp_eq_max_right [in Mcltt.Core.Syntactic.System.Lemmas]lift_exp_eq_max_left [in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_eq_ge [in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_max_right [in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_max_left [in Mcltt.Core.Syntactic.System.Lemmas]
lift_exp_ge [in Mcltt.Core.Syntactic.System.Lemmas]
lift_nbe_max_right [in Mcltt.Core.Semantic.NbE]
lift_nbe_max_left [in Mcltt.Core.Semantic.NbE]
lift_nbe_ge [in Mcltt.Core.Semantic.NbE]
lookup_bound [in Mcltt.Frontend.Elaborator]
lookup_known [in Mcltt.Frontend.Elaborator]
M
mk_glu_rel_exp_with_sub'' [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]mk_glu_rel_exp_with_sub' [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub'' [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub' [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
N
nbe_type_to_nbe_ty [in Mcltt.Core.Semantic.NbE]nbe_cumu [in Mcltt.Core.Semantic.NbE]
nbe_ty_impl_complete [in Mcltt.Extraction.NbE]
nbe_ty_order_sound [in Mcltt.Extraction.NbE]
nbe_impl_complete [in Mcltt.Extraction.NbE]
nbe_order_sound [in Mcltt.Extraction.NbE]
ne_eq_dec [in Mcltt.Core.Syntactic.Syntax]
nf_eq_dec [in Mcltt.Core.Syntactic.Syntax]
nf_of_pi [in Mcltt.Core.Semantic.Consequences]
P
per_ctx_then_per_env_initial_env [in Mcltt.Core.Semantic.Realizability]per_elem_then_per_top [in Mcltt.Core.Semantic.Realizability]
per_bot_then_per_elem [in Mcltt.Core.Semantic.Realizability]
per_univ_then_per_top_typ [in Mcltt.Core.Semantic.Realizability]
per_nat_then_per_top [in Mcltt.Core.Semantic.Realizability]
per_univ_elem_glu_univ_elem [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
per_univ_glu_univ_elem [in Mcltt.Core.Soundness.LogicalRelation.CoreLemmas]
PER_refl2 [in Mcltt.LibTactics]
PER_refl1 [in Mcltt.LibTactics]
per_univ_elem_core_univ' [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl2 [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl1 [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_subtyping [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_to_env [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_respects_length [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons_clean_inversion [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons' [in Mcltt.Core.Semantic.PER.Lemmas]
per_env_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_cross_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_left_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_env_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_env_right_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_right [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_left [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_transp [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_refl2 [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_refl1 [in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_subtyping_gen [in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_subtyping [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_to_univ_elem [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_right [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_left [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_ge [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi_clean_inversion [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi' [in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_trans' [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_cross_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_left_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_sym' [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_elem_right_irrel [in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_then_per_top [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_sym [in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_trans [in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_sym [in Mcltt.Core.Semantic.PER.Lemmas]
presup_subtyp_right [in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub_right [in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub_left [in Mcltt.Core.Syntactic.System.Definitions]
presup_ctx_sub [in Mcltt.Core.Syntactic.System.Definitions]
presup_rel_sub [in Mcltt.Core.Completeness.SubstitutionCases]
presup_exp_eq_ctx [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_right [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_left [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx [in Mcltt.Core.Syntactic.System.Lemmas]
presup_exp_ctx [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx_right [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx_left [in Mcltt.Core.Syntactic.System.Lemmas]
presup_sub_ctx [in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_right [in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_left [in Mcltt.Core.Syntactic.System.Lemmas]
presup_ctx_eq [in Mcltt.Core.Syntactic.System.Lemmas]
presup_typ_glu_rel_exp [in Mcltt.Core.Soundness.TermStructureCases]
presup_ctx_glu_rel_exp [in Mcltt.Core.Soundness.TermStructureCases]
presup_glu_rel_exp [in Mcltt.Core.Soundness.TermStructureCases]
presup_subtyp [in Mcltt.Core.Syntactic.Presup]
presup_sub_eq [in Mcltt.Core.Syntactic.Presup]
presup_exp_eq [in Mcltt.Core.Syntactic.Presup]
presup_exp [in Mcltt.Core.Syntactic.Presup]
presup_rel_exp [in Mcltt.Core.Completeness.TermStructureCases]
presup_right_glu_rel_sub [in Mcltt.Core.Soundness.SubstitutionCases]
presup_left_glu_rel_sub [in Mcltt.Core.Soundness.SubstitutionCases]
presup_glu_rel_sub [in Mcltt.Core.Soundness.SubstitutionCases]
prog_complete [in Mcltt.Frontend.Parser]
prog_correct [in Mcltt.Frontend.Parser]
R
read_typ_impl_complete [in Mcltt.Extraction.Readback]read_ne_impl_complete [in Mcltt.Extraction.Readback]
read_nf_impl_complete [in Mcltt.Extraction.Readback]
read_typ_order_sound [in Mcltt.Extraction.Readback]
read_ne_order_sound [in Mcltt.Extraction.Readback]
read_nf_order_sound [in Mcltt.Extraction.Readback]
realize_glu_elem_top [in Mcltt.Core.Soundness.Realizability]
realize_glu_elem_bot [in Mcltt.Core.Soundness.Realizability]
realize_glu_typ_top [in Mcltt.Core.Soundness.Realizability]
realize_glu_univ_elem_gen [in Mcltt.Core.Soundness.Realizability]
realize_per_univ_elem_gen [in Mcltt.Core.Semantic.Realizability]
rel_exp_nat_beta_succ [in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_beta_succ_rel_typ [in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_beta_zero [in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_sub [in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_sub_rel_typ [in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_cong [in Mcltt.Core.Completeness.NatCases]
rel_exp_natrec_cong_rel_typ [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_N [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_wkwk_succ_var1_inversion [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero_inversion [in Mcltt.Core.Completeness.NatCases]
rel_exp_succ_cong [in Mcltt.Core.Completeness.NatCases]
rel_exp_succ_sub [in Mcltt.Core.Completeness.NatCases]
rel_exp_zero_sub [in Mcltt.Core.Completeness.NatCases]
rel_exp_nat_sub [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_nat [in Mcltt.Core.Completeness.NatCases]
rel_exp_of_nat_inversion [in Mcltt.Core.Completeness.NatCases]
rel_typ_implies_rel_exp [in Mcltt.Core.Completeness.LogicalRelation.Lemmas]
rel_exp_implies_rel_typ [in Mcltt.Core.Completeness.LogicalRelation.Lemmas]
rel_sub_eq_subtyp [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_conv [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_trans [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_sym [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_p_extend [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend_compose [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_compose_assoc [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_left [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_right [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_extend_cong [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_compose_cong [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_weaken [in Mcltt.Core.Completeness.SubstitutionCases]
rel_sub_id [in Mcltt.Core.Completeness.SubstitutionCases]
rel_exp_cumu [in Mcltt.Core.Completeness.UniverseCases]
rel_exp_typ_sub [in Mcltt.Core.Completeness.UniverseCases]
rel_exp_of_typ [in Mcltt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion [in Mcltt.Core.Completeness.UniverseCases]
rel_ctx_sub_extend [in Mcltt.Core.Completeness.ContextCases]
rel_ctx_sub_empty [in Mcltt.Core.Completeness.ContextCases]
rel_ctx_extend' [in Mcltt.Core.Completeness.ContextCases]
rel_ctx_extend [in Mcltt.Core.Completeness.ContextCases]
rel_exp_pi_eta [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_beta [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_app_sub [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_app_cong [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_fn_sub [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_fn_cong [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_sub [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_cong [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_pi_core [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_of_pi [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_of_pi_inversion [in Mcltt.Core.Completeness.FunctionCases]
rel_exp_var_weaken [in Mcltt.Core.Completeness.VariableCases]
rel_exp_var_S_sub [in Mcltt.Core.Completeness.VariableCases]
rel_exp_var_0_sub [in Mcltt.Core.Completeness.VariableCases]
rel_exp_eq_subtyp [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_trans [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sym [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_conv [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_compose [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_id [in Mcltt.Core.Completeness.TermStructureCases]
rel_exp_sub_cong [in Mcltt.Core.Completeness.TermStructureCases]
S
safe [in Mcltt.Frontend.Parser]soundness [in Mcltt.Core.Soundness]
soundness_fundamental_sub [in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_exp [in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_ctx [in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [in Mcltt.Core.Soundness.FundamentalTheorem]
soundness_ty' [in Mcltt.Core.Soundness]
soundness_ty [in Mcltt.Core.Soundness]
soundness' [in Mcltt.Core.Soundness]
Subset_to_In [in Mcltt.Frontend.Elaborator]
subtyping_impl_complete [in Mcltt.Extraction.Subtyping]
subtyping_impl_complete' [in Mcltt.Extraction.Subtyping]
subtyping_order_sound [in Mcltt.Extraction.Subtyping]
subtyping_nf_impl_complete [in Mcltt.Extraction.Subtyping]
subtyp_pi [in Mcltt.Core.Completeness.SubtypingCases]
subtyp_univ [in Mcltt.Core.Completeness.SubtypingCases]
subtyp_trans [in Mcltt.Core.Completeness.SubtypingCases]
subtyp_refl [in Mcltt.Core.Completeness.SubtypingCases]
sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_p_q_q_sigma_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_id_extend [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_sigma_compose_weak_id_extend [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_compose_sigma [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_nat_compose_sigma [in Mcltt.Core.Syntactic.System.Lemmas]
sub_weak_compose_weak_extend_succ_var_1 [in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_extend_zero [in Mcltt.Core.Syntactic.System.Lemmas]
sub_q_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_q_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_q [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_id_extend [in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_extend [in Mcltt.Core.Syntactic.System.Lemmas]
sub_id_on_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_extend_nat [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_wk_var0_id [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_extend_typ [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_refl [in Mcltt.Core.Syntactic.System.Lemmas]
sub_eq_q_compose_nat [in Mcltt.Core.Syntactic.Corollaries]
sub_eq_q_compose [in Mcltt.Core.Syntactic.Corollaries]
sub_eq_p_q_sigma_compose_tau_extend [in Mcltt.Core.Syntactic.Corollaries]
sub_decompose_q_typ [in Mcltt.Core.Syntactic.Corollaries]
sub_decompose_q [in Mcltt.Core.Syntactic.Corollaries]
sub_q_eq [in Mcltt.Core.Syntactic.Corollaries]
sub_id_typ [in Mcltt.Core.Syntactic.Corollaries]
T
type_check_closed_complete [in Mcltt.Extraction.TypeCheck]type_infer_complete [in Mcltt.Extraction.TypeCheck]
type_check_complete' [in Mcltt.Extraction.TypeCheck]
type_check_order_soundness [in Mcltt.Extraction.TypeCheck]
type_infer_order_soundness [in Mcltt.Extraction.TypeCheck]
U
user_exp_to_type_infer_order [in Mcltt.Extraction.TypeCheck]user_exp_ne [in Mcltt.Frontend.Elaborator]
user_exp_nf [in Mcltt.Frontend.Elaborator]
V
valid_exp_zero [in Mcltt.Core.Completeness.NatCases]valid_exp_nat [in Mcltt.Core.Completeness.NatCases]
valid_exp_typ [in Mcltt.Core.Completeness.UniverseCases]
valid_ctx_empty [in Mcltt.Core.Completeness.ContextCases]
valid_exp_var [in Mcltt.Core.Completeness.VariableCases]
valid_lookup [in Mcltt.Core.Completeness.VariableCases]
var_glu_elem_bot [in Mcltt.Core.Soundness.Realizability]
var_weaken_gen [in Mcltt.Core.Soundness.Realizability]
var_arith [in Mcltt.Core.Soundness.Realizability]
var_per_elem [in Mcltt.Core.Semantic.Realizability]
var_per_bot [in Mcltt.Core.Semantic.PER.Lemmas]
var0_glu_elem [in Mcltt.Core.Soundness.Realizability]
vlookup_1_nat [in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_0_nat [in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_1_typ [in Mcltt.Core.Syntactic.System.Lemmas]
vlookup_0_typ [in Mcltt.Core.Syntactic.System.Lemmas]
W
weakening_wk [in Mcltt.Core.Soundness.Weakening.Lemmas]weakening_id [in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_compose [in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_conv [in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_resp_equiv [in Mcltt.Core.Soundness.Weakening.Lemmas]
weakening_escape [in Mcltt.Core.Soundness.Weakening.Lemmas]
well_scoped [in Mcltt.Frontend.Elaborator]
wf_sub_extend_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_compose_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_weaken_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_sub_id_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_exp_sub_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_vlookup_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_app_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_fn_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_natrec_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_succ_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_zero_inversion [in Mcltt.Core.Syntactic.CoreInversions]
wf_ctx_sub_ctx_lookup [in Mcltt.Core.Soundness.Realizability]
wf_sub_eq_subtyp' [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp' [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_subtyp' [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_subtyp' [in Mcltt.Core.Syntactic.System.Definitions]
wf_pi_inversion' [in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_pi_inversion [in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_nat_inversion [in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_typ_inversion [in Mcltt.Core.Syntactic.CoreTypeInversions]
wf_subtyp_univ_weaken [in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_sub [in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_ge [in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_refl [in Mcltt.Core.Syntactic.System.Lemmas]
wf_sub_eq_conv [in Mcltt.Core.Syntactic.System.Lemmas]
wf_exp_eq_cumu [in Mcltt.Core.Syntactic.System.Lemmas]
wf_exp_eq_conv [in Mcltt.Core.Syntactic.System.Lemmas]
wf_sub_conv [in Mcltt.Core.Syntactic.System.Lemmas]
wf_cumu [in Mcltt.Core.Syntactic.System.Lemmas]
wf_conv [in Mcltt.Core.Syntactic.System.Lemmas]
wf_ctx_sub_refl [in Mcltt.Core.Syntactic.System.Lemmas]
wf_subtyp_subst [in Mcltt.Core.Syntactic.Corollaries]
wf_subtyp_subst_eq [in Mcltt.Core.Syntactic.Corollaries]
wf_ctx_sub_length [in Mcltt.Core.Syntactic.Corollaries]
wf_subtyp_pi' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_eta' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_beta' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_sub' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_cong' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_sub' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_cong' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong_max [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_sub_max [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_succ' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_zero' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_sub' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_cong' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_sub' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_typ_sub' [in Mcltt.Core.Syntactic.SystemOpt]
wf_app' [in Mcltt.Core.Syntactic.SystemOpt]
wf_fn' [in Mcltt.Core.Syntactic.SystemOpt]
wf_pi_max [in Mcltt.Core.Syntactic.SystemOpt]
wf_natrec' [in Mcltt.Core.Syntactic.SystemOpt]
wf_nat' [in Mcltt.Core.Syntactic.SystemOpt]
wf_ctx_eq_extend' [in Mcltt.Core.Syntactic.SystemOpt]
wf_exp_eq_conv' [in Mcltt.Core.Syntactic.SystemOpt]
wf_conv' [in Mcltt.Core.Syntactic.SystemOpt]
wf_subtyp_refl' [in Mcltt.Core.Syntactic.SystemOpt]
wf_ctx_sub_trans [in Mcltt.Core.Syntactic.CtxSub]
Constructor Index
A
alg_subtyp_run [in Mcltt.Algorithmic.Subtyping.Definitions]AllGood [in Mcltt.Entrypoint]
ARROW [in Mcltt.Frontend.Parser]
asnf_pi [in Mcltt.Algorithmic.Subtyping.Definitions]
asnf_univ [in Mcltt.Algorithmic.Subtyping.Definitions]
asnf_refl [in Mcltt.Algorithmic.Subtyping.Definitions]
AT [in Mcltt.Frontend.Parser]
atc_ati [in Mcltt.Algorithmic.Typing.Definitions]
ati_vlookup [in Mcltt.Algorithmic.Typing.Definitions]
ati_app [in Mcltt.Algorithmic.Typing.Definitions]
ati_fn [in Mcltt.Algorithmic.Typing.Definitions]
ati_pi [in Mcltt.Algorithmic.Typing.Definitions]
ati_natrec [in Mcltt.Algorithmic.Typing.Definitions]
ati_succ [in Mcltt.Algorithmic.Typing.Definitions]
ati_zero [in Mcltt.Algorithmic.Typing.Definitions]
ati_nat [in Mcltt.Algorithmic.Typing.Definitions]
ati_typ [in Mcltt.Algorithmic.Typing.Definitions]
Aut.Init'0 [in Mcltt.Frontend.Parser]
Aut.Nis'1 [in Mcltt.Frontend.Parser]
Aut.Nis'10 [in Mcltt.Frontend.Parser]
Aut.Nis'11 [in Mcltt.Frontend.Parser]
Aut.Nis'12 [in Mcltt.Frontend.Parser]
Aut.Nis'13 [in Mcltt.Frontend.Parser]
Aut.Nis'14 [in Mcltt.Frontend.Parser]
Aut.Nis'15 [in Mcltt.Frontend.Parser]
Aut.Nis'16 [in Mcltt.Frontend.Parser]
Aut.Nis'17 [in Mcltt.Frontend.Parser]
Aut.Nis'18 [in Mcltt.Frontend.Parser]
Aut.Nis'19 [in Mcltt.Frontend.Parser]
Aut.Nis'2 [in Mcltt.Frontend.Parser]
Aut.Nis'20 [in Mcltt.Frontend.Parser]
Aut.Nis'21 [in Mcltt.Frontend.Parser]
Aut.Nis'22 [in Mcltt.Frontend.Parser]
Aut.Nis'23 [in Mcltt.Frontend.Parser]
Aut.Nis'24 [in Mcltt.Frontend.Parser]
Aut.Nis'25 [in Mcltt.Frontend.Parser]
Aut.Nis'26 [in Mcltt.Frontend.Parser]
Aut.Nis'27 [in Mcltt.Frontend.Parser]
Aut.Nis'28 [in Mcltt.Frontend.Parser]
Aut.Nis'29 [in Mcltt.Frontend.Parser]
Aut.Nis'3 [in Mcltt.Frontend.Parser]
Aut.Nis'30 [in Mcltt.Frontend.Parser]
Aut.Nis'31 [in Mcltt.Frontend.Parser]
Aut.Nis'32 [in Mcltt.Frontend.Parser]
Aut.Nis'33 [in Mcltt.Frontend.Parser]
Aut.Nis'34 [in Mcltt.Frontend.Parser]
Aut.Nis'35 [in Mcltt.Frontend.Parser]
Aut.Nis'36 [in Mcltt.Frontend.Parser]
Aut.Nis'37 [in Mcltt.Frontend.Parser]
Aut.Nis'38 [in Mcltt.Frontend.Parser]
Aut.Nis'39 [in Mcltt.Frontend.Parser]
Aut.Nis'4 [in Mcltt.Frontend.Parser]
Aut.Nis'40 [in Mcltt.Frontend.Parser]
Aut.Nis'41 [in Mcltt.Frontend.Parser]
Aut.Nis'42 [in Mcltt.Frontend.Parser]
Aut.Nis'43 [in Mcltt.Frontend.Parser]
Aut.Nis'44 [in Mcltt.Frontend.Parser]
Aut.Nis'45 [in Mcltt.Frontend.Parser]
Aut.Nis'46 [in Mcltt.Frontend.Parser]
Aut.Nis'48 [in Mcltt.Frontend.Parser]
Aut.Nis'49 [in Mcltt.Frontend.Parser]
Aut.Nis'5 [in Mcltt.Frontend.Parser]
Aut.Nis'50 [in Mcltt.Frontend.Parser]
Aut.Nis'51 [in Mcltt.Frontend.Parser]
Aut.Nis'6 [in Mcltt.Frontend.Parser]
Aut.Nis'7 [in Mcltt.Frontend.Parser]
Aut.Nis'8 [in Mcltt.Frontend.Parser]
Aut.Nis'9 [in Mcltt.Frontend.Parser]
a_extend [in Mcltt.Core.Syntactic.Syntax]
a_compose [in Mcltt.Core.Syntactic.Syntax]
a_weaken [in Mcltt.Core.Syntactic.Syntax]
a_id [in Mcltt.Core.Syntactic.Syntax]
a_sub [in Mcltt.Core.Syntactic.Syntax]
a_var [in Mcltt.Core.Syntactic.Syntax]
a_app [in Mcltt.Core.Syntactic.Syntax]
a_fn [in Mcltt.Core.Syntactic.Syntax]
a_pi [in Mcltt.Core.Syntactic.Syntax]
a_natrec [in Mcltt.Core.Syntactic.Syntax]
a_succ [in Mcltt.Core.Syntactic.Syntax]
a_zero [in Mcltt.Core.Syntactic.Syntax]
a_nat [in Mcltt.Core.Syntactic.Syntax]
a_typ [in Mcltt.Core.Syntactic.Syntax]
B
BAR [in Mcltt.Frontend.Parser]C
ca_natrec [in Mcltt.Frontend.Elaborator]ca_succ [in Mcltt.Frontend.Elaborator]
ca_type [in Mcltt.Frontend.Elaborator]
ca_zero [in Mcltt.Frontend.Elaborator]
ca_nat [in Mcltt.Frontend.Elaborator]
ca_app [in Mcltt.Frontend.Elaborator]
ca_pi [in Mcltt.Frontend.Elaborator]
ca_lam [in Mcltt.Frontend.Elaborator]
ca_var [in Mcltt.Frontend.Elaborator]
COLON [in Mcltt.Frontend.Parser]
COMMA [in Mcltt.Frontend.Parser]
Cst.app [in Mcltt.Core.Syntactic.Syntax]
Cst.fn [in Mcltt.Core.Syntactic.Syntax]
Cst.nat [in Mcltt.Core.Syntactic.Syntax]
Cst.natrec [in Mcltt.Core.Syntactic.Syntax]
Cst.pi [in Mcltt.Core.Syntactic.Syntax]
Cst.succ [in Mcltt.Core.Syntactic.Syntax]
Cst.typ [in Mcltt.Core.Syntactic.Syntax]
Cst.var [in Mcltt.Core.Syntactic.Syntax]
Cst.zero [in Mcltt.Core.Syntactic.Syntax]
D
DARROW [in Mcltt.Frontend.Parser]d_dom [in Mcltt.Core.Semantic.Domain]
d_natrec [in Mcltt.Core.Semantic.Domain]
d_app [in Mcltt.Core.Semantic.Domain]
d_var [in Mcltt.Core.Semantic.Domain]
d_neut [in Mcltt.Core.Semantic.Domain]
d_fn [in Mcltt.Core.Semantic.Domain]
d_succ [in Mcltt.Core.Semantic.Domain]
d_zero [in Mcltt.Core.Semantic.Domain]
d_univ [in Mcltt.Core.Semantic.Domain]
d_pi [in Mcltt.Core.Semantic.Domain]
d_nat [in Mcltt.Core.Semantic.Domain]
E
eao_neut [in Mcltt.Extraction.Evaluation]eao_fn [in Mcltt.Extraction.Evaluation]
eeo_sub [in Mcltt.Extraction.Evaluation]
eeo_app [in Mcltt.Extraction.Evaluation]
eeo_fn [in Mcltt.Extraction.Evaluation]
eeo_pi [in Mcltt.Extraction.Evaluation]
eeo_natrec [in Mcltt.Extraction.Evaluation]
eeo_succ [in Mcltt.Extraction.Evaluation]
eeo_zero [in Mcltt.Extraction.Evaluation]
eeo_nat [in Mcltt.Extraction.Evaluation]
eeo_var [in Mcltt.Extraction.Evaluation]
eeo_typ [in Mcltt.Extraction.Evaluation]
ElaborationFailure [in Mcltt.Entrypoint]
END [in Mcltt.Frontend.Parser]
eno_neut [in Mcltt.Extraction.Evaluation]
eno_succ [in Mcltt.Extraction.Evaluation]
eno_zero [in Mcltt.Extraction.Evaluation]
EOF [in Mcltt.Frontend.Parser]
eso_compose [in Mcltt.Extraction.Evaluation]
eso_extend [in Mcltt.Extraction.Evaluation]
eso_weaken [in Mcltt.Extraction.Evaluation]
eso_id [in Mcltt.Extraction.Evaluation]
eval_sub_compose [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_extend [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_weaken [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_id [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_neut [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_fn [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_neut [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_succ [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_zero [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_sub [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_app [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_fn [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_pi [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_natrec [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_succ [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_zero [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_nat [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_var [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_typ [in Mcltt.Core.Semantic.Evaluation.Definitions]
G
glu_ctx_env_cons [in Mcltt.Core.Soundness.LogicalRelation.Definitions]glu_ctx_env_nil [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top_make [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top_make [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot_make [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_neut [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_pi [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_nat [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_univ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_neut [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_succ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_zero [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gram.app_obj'nt [in Mcltt.Frontend.Parser]
Gram.ARROW't [in Mcltt.Frontend.Parser]
Gram.atomic_obj'nt [in Mcltt.Frontend.Parser]
Gram.AT't [in Mcltt.Frontend.Parser]
Gram.BAR't [in Mcltt.Frontend.Parser]
Gram.COLON't [in Mcltt.Frontend.Parser]
Gram.COMMA't [in Mcltt.Frontend.Parser]
Gram.DARROW't [in Mcltt.Frontend.Parser]
Gram.END't [in Mcltt.Frontend.Parser]
Gram.EOF't [in Mcltt.Frontend.Parser]
Gram.fnbinder'nt [in Mcltt.Frontend.Parser]
Gram.INT't [in Mcltt.Frontend.Parser]
Gram.LAMBDA't [in Mcltt.Frontend.Parser]
Gram.LPAREN't [in Mcltt.Frontend.Parser]
Gram.NAT't [in Mcltt.Frontend.Parser]
Gram.obj'nt [in Mcltt.Frontend.Parser]
Gram.params'nt [in Mcltt.Frontend.Parser]
Gram.param'nt [in Mcltt.Frontend.Parser]
Gram.PI't [in Mcltt.Frontend.Parser]
Gram.Prod'app_obj'0 [in Mcltt.Frontend.Parser]
Gram.Prod'app_obj'1 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'0 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'1 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'2 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'3 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'4 [in Mcltt.Frontend.Parser]
Gram.Prod'atomic_obj'5 [in Mcltt.Frontend.Parser]
Gram.Prod'fnbinder'0 [in Mcltt.Frontend.Parser]
Gram.Prod'fnbinder'1 [in Mcltt.Frontend.Parser]
Gram.Prod'obj'0 [in Mcltt.Frontend.Parser]
Gram.Prod'obj'1 [in Mcltt.Frontend.Parser]
Gram.Prod'obj'2 [in Mcltt.Frontend.Parser]
Gram.Prod'obj'3 [in Mcltt.Frontend.Parser]
Gram.Prod'params'0 [in Mcltt.Frontend.Parser]
Gram.Prod'params'1 [in Mcltt.Frontend.Parser]
Gram.Prod'param'0 [in Mcltt.Frontend.Parser]
Gram.Prod'prog'0 [in Mcltt.Frontend.Parser]
Gram.prog'nt [in Mcltt.Frontend.Parser]
Gram.REC't [in Mcltt.Frontend.Parser]
Gram.RETURN't [in Mcltt.Frontend.Parser]
Gram.RPAREN't [in Mcltt.Frontend.Parser]
Gram.SUCC't [in Mcltt.Frontend.Parser]
Gram.TYPE't [in Mcltt.Frontend.Parser]
Gram.VAR't [in Mcltt.Frontend.Parser]
Gram.ZERO't [in Mcltt.Frontend.Parser]
H
here [in Mcltt.Core.Syntactic.System.Definitions]I
ie_cons [in Mcltt.Extraction.NbE]ie_nil [in Mcltt.Extraction.NbE]
initial_env_cons [in Mcltt.Core.Semantic.NbE]
initial_env_nil [in Mcltt.Core.Semantic.NbE]
INT [in Mcltt.Frontend.Parser]
L
LAMBDA [in Mcltt.Frontend.Parser]LPAREN [in Mcltt.Frontend.Parser]
M
mk_glu_rel_sub_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]mk_glu_rel_exp_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_cons_glu_sub_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_typ_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_neut_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
mk_rel_sub [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_exp [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_mod_app [in Mcltt.Core.Semantic.PER.Definitions]
mk_rel_mod_eval [in Mcltt.Core.Semantic.PER.Definitions]
N
NAT [in Mcltt.Frontend.Parser]nat_is_typ_constr [in Mcltt.Core.Completeness.Consequences.Types]
nbe_ty_run [in Mcltt.Core.Semantic.NbE]
nbe_run [in Mcltt.Core.Semantic.NbE]
nbe_ty_order_run [in Mcltt.Extraction.NbE]
nbe_order_run [in Mcltt.Extraction.NbE]
ne_var [in Mcltt.Core.Syntactic.Syntax]
ne_app [in Mcltt.Core.Syntactic.Syntax]
ne_natrec [in Mcltt.Core.Syntactic.Syntax]
nf_neut [in Mcltt.Core.Syntactic.Syntax]
nf_fn [in Mcltt.Core.Syntactic.Syntax]
nf_pi [in Mcltt.Core.Syntactic.Syntax]
nf_succ [in Mcltt.Core.Syntactic.Syntax]
nf_zero [in Mcltt.Core.Syntactic.Syntax]
nf_nat [in Mcltt.Core.Syntactic.Syntax]
nf_typ [in Mcltt.Core.Syntactic.Syntax]
P
ParserFailure [in Mcltt.Entrypoint]ParserTimeout [in Mcltt.Entrypoint]
per_elem [in Mcltt.LibTactics]
per_ctx_subtyp_cons [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_nil [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_cons [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_nil [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_pi [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_univ [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_nat [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_neut [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_neut [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_pi [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_nat [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ [in Mcltt.Core.Semantic.PER.Definitions]
per_ne_neut [in Mcltt.Core.Semantic.PER.Definitions]
per_nat_neut [in Mcltt.Core.Semantic.PER.Definitions]
per_nat_succ [in Mcltt.Core.Semantic.PER.Definitions]
per_nat_zero [in Mcltt.Core.Semantic.PER.Definitions]
PI [in Mcltt.Frontend.Parser]
pi_is_typ_constr [in Mcltt.Core.Completeness.Consequences.Types]
R
read_typ_neut [in Mcltt.Core.Semantic.Readback.Definitions]read_typ_pi [in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_nat [in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_univ [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_natrec [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_app [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_var [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_neut [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_fn [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_nat_neut [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_succ [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_zero [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_type [in Mcltt.Core.Semantic.Readback.Definitions]
REC [in Mcltt.Frontend.Parser]
RETURN [in Mcltt.Frontend.Parser]
rne_natrec [in Mcltt.Extraction.Readback]
rne_app [in Mcltt.Extraction.Readback]
rne_var [in Mcltt.Extraction.Readback]
rnf_neut [in Mcltt.Extraction.Readback]
rnf_fn [in Mcltt.Extraction.Readback]
rnf_nat_neut [in Mcltt.Extraction.Readback]
rnf_succ [in Mcltt.Extraction.Readback]
rnf_zero [in Mcltt.Extraction.Readback]
rnf_type [in Mcltt.Extraction.Readback]
RPAREN [in Mcltt.Frontend.Parser]
rtyp_neut [in Mcltt.Extraction.Readback]
rtyp_pi [in Mcltt.Extraction.Readback]
rtyp_nat [in Mcltt.Extraction.Readback]
rtyp_univ [in Mcltt.Extraction.Readback]
S
subtyping_order_run [in Mcltt.Extraction.Subtyping]SUCC [in Mcltt.Frontend.Parser]
T
tc_ti [in Mcltt.Extraction.TypeCheck]there [in Mcltt.Core.Syntactic.System.Definitions]
ti_vlookup [in Mcltt.Extraction.TypeCheck]
ti_app [in Mcltt.Extraction.TypeCheck]
ti_fn [in Mcltt.Extraction.TypeCheck]
ti_pi [in Mcltt.Extraction.TypeCheck]
ti_natrec [in Mcltt.Extraction.TypeCheck]
ti_succ [in Mcltt.Extraction.TypeCheck]
ti_zero [in Mcltt.Extraction.TypeCheck]
ti_nat [in Mcltt.Extraction.TypeCheck]
ti_typ [in Mcltt.Extraction.TypeCheck]
TYPE [in Mcltt.Frontend.Parser]
TypeCheckingFailure [in Mcltt.Entrypoint]
typ_is_typ_constr [in Mcltt.Core.Completeness.Consequences.Types]
U
user_exp_vlookup [in Mcltt.Frontend.Elaborator]user_exp_app [in Mcltt.Frontend.Elaborator]
user_exp_fn [in Mcltt.Frontend.Elaborator]
user_exp_pi [in Mcltt.Frontend.Elaborator]
user_exp_natrec [in Mcltt.Frontend.Elaborator]
user_exp_succ [in Mcltt.Frontend.Elaborator]
user_exp_zero [in Mcltt.Frontend.Elaborator]
user_exp_nat [in Mcltt.Frontend.Elaborator]
user_exp_typ [in Mcltt.Frontend.Elaborator]
V
VAR [in Mcltt.Frontend.Parser]W
wf_ctx_eq_extend [in Mcltt.Core.Syntactic.System.Definitions]wf_ctx_eq_empty [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_pi [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_univ [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_trans [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_refl [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_trans [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_sym [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_p_extend [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_compose [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_assoc [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_left [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_right [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_weaken [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_id [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_trans [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sym [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_compose [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_id [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_weaken [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_S_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_0_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_var [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_eta [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_beta [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_succ [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_zero [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_cong [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_zero_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_typ_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_subtyp [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_extend [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_compose [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_weaken [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_id [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_subtyp [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_vlookup [in Mcltt.Core.Syntactic.System.Definitions]
wf_app [in Mcltt.Core.Syntactic.System.Definitions]
wf_fn [in Mcltt.Core.Syntactic.System.Definitions]
wf_pi [in Mcltt.Core.Syntactic.System.Definitions]
wf_natrec [in Mcltt.Core.Syntactic.System.Definitions]
wf_succ [in Mcltt.Core.Syntactic.System.Definitions]
wf_zero [in Mcltt.Core.Syntactic.System.Definitions]
wf_nat [in Mcltt.Core.Syntactic.System.Definitions]
wf_typ [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_extend [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_empty [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_extend [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_empty [in Mcltt.Core.Syntactic.System.Definitions]
wk_p [in Mcltt.Core.Soundness.Weakening.Definition]
wk_id [in Mcltt.Core.Soundness.Weakening.Definition]
Z
ZERO [in Mcltt.Frontend.Parser]Axiom Index
L
loc [in Mcltt.Frontend.Parser]Inductive Index
A
alg_type_infer [in Mcltt.Algorithmic.Typing.Definitions]alg_type_check [in Mcltt.Algorithmic.Typing.Definitions]
alg_subtyping [in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf [in Mcltt.Algorithmic.Subtyping.Definitions]
Aut.initstate' [in Mcltt.Frontend.Parser]
Aut.noninitstate' [in Mcltt.Frontend.Parser]
C
closed_at [in Mcltt.Frontend.Elaborator]cons_glu_sub_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Cst.obj [in Mcltt.Core.Syntactic.Syntax]
ctx_lookup [in Mcltt.Core.Syntactic.System.Definitions]
D
domain [in Mcltt.Core.Semantic.Domain]domain_nf [in Mcltt.Core.Semantic.Domain]
domain_ne [in Mcltt.Core.Semantic.Domain]
E
eval_sub_order [in Mcltt.Extraction.Evaluation]eval_app_order [in Mcltt.Extraction.Evaluation]
eval_natrec_order [in Mcltt.Extraction.Evaluation]
eval_exp_order [in Mcltt.Extraction.Evaluation]
eval_sub [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp [in Mcltt.Core.Semantic.Evaluation.Definitions]
exp [in Mcltt.Core.Syntactic.Syntax]
G
glu_rel_sub_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]glu_rel_exp_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_typ_with_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
Gram.nonterminal' [in Mcltt.Frontend.Parser]
Gram.production' [in Mcltt.Frontend.Parser]
Gram.terminal' [in Mcltt.Frontend.Parser]
I
initial_env [in Mcltt.Core.Semantic.NbE]initial_env_order [in Mcltt.Extraction.NbE]
is_typ_constr [in Mcltt.Core.Completeness.Consequences.Types]
M
main_result [in Mcltt.Entrypoint]N
nbe [in Mcltt.Core.Semantic.NbE]nbe_ty [in Mcltt.Core.Semantic.NbE]
nbe_ty_order [in Mcltt.Extraction.NbE]
nbe_order [in Mcltt.Extraction.NbE]
ne [in Mcltt.Core.Syntactic.Syntax]
neut_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
nf [in Mcltt.Core.Syntactic.Syntax]
P
PERElem [in Mcltt.LibTactics]per_ctx_subtyp [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core [in Mcltt.Core.Semantic.PER.Definitions]
per_ne [in Mcltt.Core.Semantic.PER.Definitions]
per_nat [in Mcltt.Core.Semantic.PER.Definitions]
pi_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
pi_glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
R
read_typ_order [in Mcltt.Extraction.Readback]read_ne_order [in Mcltt.Extraction.Readback]
read_nf_order [in Mcltt.Extraction.Readback]
read_typ [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf [in Mcltt.Core.Semantic.Readback.Definitions]
rel_sub [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_mod_app [in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval [in Mcltt.Core.Semantic.PER.Definitions]
S
sub [in Mcltt.Core.Syntactic.Syntax]subtyping_order [in Mcltt.Extraction.Subtyping]
T
token [in Mcltt.Frontend.Parser]type_infer_order [in Mcltt.Extraction.TypeCheck]
type_check_order [in Mcltt.Extraction.TypeCheck]
U
user_exp [in Mcltt.Frontend.Elaborator]W
weakening [in Mcltt.Core.Soundness.Weakening.Definition]wf_ctx_eq [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx [in Mcltt.Core.Syntactic.System.Definitions]
Projection Index
P
per_elem [in Mcltt.LibTactics]Section Index
C
completeness_fundamental [in Mcltt.Core.Completeness.FundamentalTheorem]F
functional_read [in Mcltt.Core.Semantic.Readback.Lemmas]functional_eval [in Mcltt.Core.Semantic.Evaluation.Lemmas]
G
Gluing [in Mcltt.Core.Soundness.LogicalRelation.Definitions]GluingInduction [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_cumulativity [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
I
InitialEnvImpl [in Mcltt.Extraction.NbE]L
lookup [in Mcltt.Extraction.TypeCheck]N
NbEDef [in Mcltt.Extraction.NbE]NbETyDef [in Mcltt.Extraction.NbE]
P
Per_univ_elem_ind_def [in Mcltt.Core.Semantic.PER.Definitions]Per_univ_elem_core_def [in Mcltt.Core.Semantic.PER.Definitions]
S
soundness_fundamental [in Mcltt.Core.Soundness.FundamentalTheorem]T
type_check_closed [in Mcltt.Extraction.TypeCheck]type_check [in Mcltt.Extraction.TypeCheck]
Instance Index
A
Aut.InitStateAlph [in Mcltt.Frontend.Parser]Aut.initstateNum [in Mcltt.Frontend.Parser]
Aut.NonInitStateAlph [in Mcltt.Frontend.Parser]
Aut.noninitstateNum [in Mcltt.Frontend.Parser]
G
Gram.NonTerminalAlph [in Mcltt.Frontend.Parser]Gram.nonterminalNum [in Mcltt.Frontend.Parser]
Gram.ProductionAlph [in Mcltt.Frontend.Parser]
Gram.productionNum [in Mcltt.Frontend.Parser]
Gram.TerminalAlph [in Mcltt.Frontend.Parser]
Gram.terminalNum [in Mcltt.Frontend.Parser]
P
PERProper [in Mcltt.LibTactics]per_ctx_subtyp_trans_ins [in Mcltt.Core.Semantic.PER.Lemmas]
per_env_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_ctx_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_subtyp_trans_ins [in Mcltt.Core.Semantic.PER.Lemmas]
per_elem_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_PER' [in Mcltt.Core.Semantic.PER.Lemmas]
per_univ_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_ne_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_nat_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_typ_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_top_PER [in Mcltt.Core.Semantic.PER.Lemmas]
per_bot_PER [in Mcltt.Core.Semantic.PER.Lemmas]
predicate_implication_equivalence [in Mcltt.LibTactics]
R
rel_sub_PER [in Mcltt.Core.Completeness.SubstitutionCases]rel_exp_PER [in Mcltt.Core.Completeness.TermStructureCases]
S
subtyp_Transitive [in Mcltt.Core.Completeness.SubtypingCases]W
wf_sub_eq_per_elem [in Mcltt.Core.Syntactic.System.Definitions]wf_exp_eq_per_elem [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_Transitive [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_Symmetric [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_PER [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_PER [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_PER [in Mcltt.Core.Syntactic.CtxEq]
wf_ctx_sub_trans_ins [in Mcltt.Core.Syntactic.CtxSub]
Abbreviation Index
C
ctx [in Mcltt.Core.Syntactic.Syntax]T
typ [in Mcltt.Core.Syntactic.Syntax]Definition Index
A
alg_type_infer_mut_ind [in Mcltt.Algorithmic.Typing.Definitions]alg_type_check_mut_ind [in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer_sind [in Mcltt.Algorithmic.Typing.Definitions]
alg_type_infer_ind [in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check_sind [in Mcltt.Algorithmic.Typing.Definitions]
alg_type_check_ind [in Mcltt.Algorithmic.Typing.Definitions]
alg_subtyping_sind [in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_ind [in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf_sind [in Mcltt.Algorithmic.Subtyping.Definitions]
alg_subtyping_nf_ind [in Mcltt.Algorithmic.Subtyping.Definitions]
Aut.action_table [in Mcltt.Frontend.Parser]
Aut.first_nterm [in Mcltt.Frontend.Parser]
Aut.goto_table [in Mcltt.Frontend.Parser]
Aut.initstate [in Mcltt.Frontend.Parser]
Aut.items_of_state [in Mcltt.Frontend.Parser]
Aut.items_of_state_51 [in Mcltt.Frontend.Parser]
Aut.items_of_state_50 [in Mcltt.Frontend.Parser]
Aut.items_of_state_49 [in Mcltt.Frontend.Parser]
Aut.items_of_state_48 [in Mcltt.Frontend.Parser]
Aut.items_of_state_46 [in Mcltt.Frontend.Parser]
Aut.items_of_state_45 [in Mcltt.Frontend.Parser]
Aut.items_of_state_44 [in Mcltt.Frontend.Parser]
Aut.items_of_state_43 [in Mcltt.Frontend.Parser]
Aut.items_of_state_42 [in Mcltt.Frontend.Parser]
Aut.items_of_state_41 [in Mcltt.Frontend.Parser]
Aut.items_of_state_40 [in Mcltt.Frontend.Parser]
Aut.items_of_state_39 [in Mcltt.Frontend.Parser]
Aut.items_of_state_38 [in Mcltt.Frontend.Parser]
Aut.items_of_state_37 [in Mcltt.Frontend.Parser]
Aut.items_of_state_36 [in Mcltt.Frontend.Parser]
Aut.items_of_state_35 [in Mcltt.Frontend.Parser]
Aut.items_of_state_34 [in Mcltt.Frontend.Parser]
Aut.items_of_state_33 [in Mcltt.Frontend.Parser]
Aut.items_of_state_32 [in Mcltt.Frontend.Parser]
Aut.items_of_state_31 [in Mcltt.Frontend.Parser]
Aut.items_of_state_30 [in Mcltt.Frontend.Parser]
Aut.items_of_state_29 [in Mcltt.Frontend.Parser]
Aut.items_of_state_28 [in Mcltt.Frontend.Parser]
Aut.items_of_state_27 [in Mcltt.Frontend.Parser]
Aut.items_of_state_26 [in Mcltt.Frontend.Parser]
Aut.items_of_state_25 [in Mcltt.Frontend.Parser]
Aut.items_of_state_24 [in Mcltt.Frontend.Parser]
Aut.items_of_state_23 [in Mcltt.Frontend.Parser]
Aut.items_of_state_22 [in Mcltt.Frontend.Parser]
Aut.items_of_state_21 [in Mcltt.Frontend.Parser]
Aut.items_of_state_20 [in Mcltt.Frontend.Parser]
Aut.items_of_state_19 [in Mcltt.Frontend.Parser]
Aut.items_of_state_18 [in Mcltt.Frontend.Parser]
Aut.items_of_state_17 [in Mcltt.Frontend.Parser]
Aut.items_of_state_16 [in Mcltt.Frontend.Parser]
Aut.items_of_state_15 [in Mcltt.Frontend.Parser]
Aut.items_of_state_14 [in Mcltt.Frontend.Parser]
Aut.items_of_state_13 [in Mcltt.Frontend.Parser]
Aut.items_of_state_12 [in Mcltt.Frontend.Parser]
Aut.items_of_state_11 [in Mcltt.Frontend.Parser]
Aut.items_of_state_10 [in Mcltt.Frontend.Parser]
Aut.items_of_state_9 [in Mcltt.Frontend.Parser]
Aut.items_of_state_8 [in Mcltt.Frontend.Parser]
Aut.items_of_state_7 [in Mcltt.Frontend.Parser]
Aut.items_of_state_6 [in Mcltt.Frontend.Parser]
Aut.items_of_state_5 [in Mcltt.Frontend.Parser]
Aut.items_of_state_4 [in Mcltt.Frontend.Parser]
Aut.items_of_state_3 [in Mcltt.Frontend.Parser]
Aut.items_of_state_2 [in Mcltt.Frontend.Parser]
Aut.items_of_state_1 [in Mcltt.Frontend.Parser]
Aut.items_of_state_0 [in Mcltt.Frontend.Parser]
Aut.last_symb_of_non_init_state [in Mcltt.Frontend.Parser]
Aut.lookahead_set_17 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_16 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_15 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_14 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_13 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_12 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_11 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_10 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_9 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_8 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_7 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_6 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_5 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_4 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_3 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_2 [in Mcltt.Frontend.Parser]
Aut.lookahead_set_1 [in Mcltt.Frontend.Parser]
Aut.noninitstate [in Mcltt.Frontend.Parser]
Aut.nullable_nterm [in Mcltt.Frontend.Parser]
Aut.N_of_state [in Mcltt.Frontend.Parser]
Aut.past_state_of_non_init_state [in Mcltt.Frontend.Parser]
Aut.past_symb_of_non_init_state [in Mcltt.Frontend.Parser]
Aut.start_nt [in Mcltt.Frontend.Parser]
Aut.state_set_37 [in Mcltt.Frontend.Parser]
Aut.state_set_36 [in Mcltt.Frontend.Parser]
Aut.state_set_35 [in Mcltt.Frontend.Parser]
Aut.state_set_34 [in Mcltt.Frontend.Parser]
Aut.state_set_33 [in Mcltt.Frontend.Parser]
Aut.state_set_32 [in Mcltt.Frontend.Parser]
Aut.state_set_31 [in Mcltt.Frontend.Parser]
Aut.state_set_30 [in Mcltt.Frontend.Parser]
Aut.state_set_29 [in Mcltt.Frontend.Parser]
Aut.state_set_28 [in Mcltt.Frontend.Parser]
Aut.state_set_27 [in Mcltt.Frontend.Parser]
Aut.state_set_26 [in Mcltt.Frontend.Parser]
Aut.state_set_25 [in Mcltt.Frontend.Parser]
Aut.state_set_24 [in Mcltt.Frontend.Parser]
Aut.state_set_23 [in Mcltt.Frontend.Parser]
Aut.state_set_22 [in Mcltt.Frontend.Parser]
Aut.state_set_21 [in Mcltt.Frontend.Parser]
Aut.state_set_20 [in Mcltt.Frontend.Parser]
Aut.state_set_19 [in Mcltt.Frontend.Parser]
Aut.state_set_18 [in Mcltt.Frontend.Parser]
Aut.state_set_17 [in Mcltt.Frontend.Parser]
Aut.state_set_16 [in Mcltt.Frontend.Parser]
Aut.state_set_15 [in Mcltt.Frontend.Parser]
Aut.state_set_14 [in Mcltt.Frontend.Parser]
Aut.state_set_13 [in Mcltt.Frontend.Parser]
Aut.state_set_12 [in Mcltt.Frontend.Parser]
Aut.state_set_11 [in Mcltt.Frontend.Parser]
Aut.state_set_10 [in Mcltt.Frontend.Parser]
Aut.state_set_9 [in Mcltt.Frontend.Parser]
Aut.state_set_8 [in Mcltt.Frontend.Parser]
Aut.state_set_7 [in Mcltt.Frontend.Parser]
Aut.state_set_6 [in Mcltt.Frontend.Parser]
Aut.state_set_5 [in Mcltt.Frontend.Parser]
Aut.state_set_4 [in Mcltt.Frontend.Parser]
Aut.state_set_3 [in Mcltt.Frontend.Parser]
Aut.state_set_2 [in Mcltt.Frontend.Parser]
Aut.state_set_1 [in Mcltt.Frontend.Parser]
C
closed_at_sind [in Mcltt.Frontend.Elaborator]closed_at_ind [in Mcltt.Frontend.Elaborator]
cst_variables [in Mcltt.Frontend.Elaborator]
Cst.obj_sind [in Mcltt.Core.Syntactic.Syntax]
Cst.obj_rec [in Mcltt.Core.Syntactic.Syntax]
Cst.obj_ind [in Mcltt.Core.Syntactic.Syntax]
Cst.obj_rect [in Mcltt.Core.Syntactic.Syntax]
ctx_lookup_sind [in Mcltt.Core.Syntactic.System.Definitions]
ctx_lookup_ind [in Mcltt.Core.Syntactic.System.Definitions]
D
domain_nf_sind [in Mcltt.Core.Semantic.Domain]domain_nf_rec [in Mcltt.Core.Semantic.Domain]
domain_nf_ind [in Mcltt.Core.Semantic.Domain]
domain_nf_rect [in Mcltt.Core.Semantic.Domain]
domain_ne_sind [in Mcltt.Core.Semantic.Domain]
domain_ne_rec [in Mcltt.Core.Semantic.Domain]
domain_ne_ind [in Mcltt.Core.Semantic.Domain]
domain_ne_rect [in Mcltt.Core.Semantic.Domain]
domain_sind [in Mcltt.Core.Semantic.Domain]
domain_rec [in Mcltt.Core.Semantic.Domain]
domain_ind [in Mcltt.Core.Semantic.Domain]
domain_rect [in Mcltt.Core.Semantic.Domain]
drop_env [in Mcltt.Core.Semantic.Domain]
E
elaborate [in Mcltt.Frontend.Elaborator]empty_env [in Mcltt.Core.Semantic.Domain]
eval_sub_impl [in Mcltt.Extraction.Evaluation]
eval_app_impl [in Mcltt.Extraction.Evaluation]
eval_natrec_impl [in Mcltt.Extraction.Evaluation]
eval_exp_impl [in Mcltt.Extraction.Evaluation]
eval_sub_order_sind [in Mcltt.Extraction.Evaluation]
eval_sub_order_ind [in Mcltt.Extraction.Evaluation]
eval_app_order_sind [in Mcltt.Extraction.Evaluation]
eval_app_order_ind [in Mcltt.Extraction.Evaluation]
eval_natrec_order_sind [in Mcltt.Extraction.Evaluation]
eval_natrec_order_ind [in Mcltt.Extraction.Evaluation]
eval_exp_order_sind [in Mcltt.Extraction.Evaluation]
eval_exp_order_ind [in Mcltt.Extraction.Evaluation]
eval_sub_mut_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_mut_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_mut_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_mut_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_sind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_sub_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_sind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_app_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_sind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_natrec_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_sind [in Mcltt.Core.Semantic.Evaluation.Definitions]
eval_exp_ind [in Mcltt.Core.Semantic.Evaluation.Definitions]
exp_to_num [in Mcltt.Core.Syntactic.Syntax]
exp_to_nat [in Mcltt.Core.Syntactic.Syntax]
exp_sind [in Mcltt.Core.Syntactic.Syntax]
exp_rec [in Mcltt.Core.Syntactic.Syntax]
exp_ind [in Mcltt.Core.Syntactic.Syntax]
exp_rect [in Mcltt.Core.Syntactic.Syntax]
extend_env [in Mcltt.Core.Semantic.Domain]
G
get_subterms_of_pi_nf [in Mcltt.Extraction.TypeCheck]get_level_of_type_nf [in Mcltt.Extraction.TypeCheck]
glu_rel_sub [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_ctx [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_sind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_ind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_ind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_typ [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_sind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_ind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_sind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_ind [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_clean_inversion2_result [in Mcltt.Core.Soundness.LogicalRelation.Lemmas]
Gram.nonterminal [in Mcltt.Frontend.Parser]
Gram.nonterminal_semantic_type [in Mcltt.Frontend.Parser]
Gram.production [in Mcltt.Frontend.Parser]
Gram.prod_action [in Mcltt.Frontend.Parser]
Gram.prod_rhs_rev [in Mcltt.Frontend.Parser]
Gram.prod_lhs [in Mcltt.Frontend.Parser]
Gram.prod_contents [in Mcltt.Frontend.Parser]
Gram.symbol_semantic_type [in Mcltt.Frontend.Parser]
Gram.terminal [in Mcltt.Frontend.Parser]
Gram.terminal_semantic_type [in Mcltt.Frontend.Parser]
Gram.token [in Mcltt.Frontend.Parser]
Gram.token_sem [in Mcltt.Frontend.Parser]
Gram.token_term [in Mcltt.Frontend.Parser]
I
initial_env_sind [in Mcltt.Core.Semantic.NbE]initial_env_ind [in Mcltt.Core.Semantic.NbE]
initial_env_impl [in Mcltt.Extraction.NbE]
initial_env_order_sind [in Mcltt.Extraction.NbE]
initial_env_order_ind [in Mcltt.Extraction.NbE]
inspect [in Mcltt.Entrypoint]
is_typ_constr_sind [in Mcltt.Core.Completeness.Consequences.Types]
is_typ_constr_ind [in Mcltt.Core.Completeness.Consequences.Types]
L
lookup [in Mcltt.Extraction.TypeCheck]lookup [in Mcltt.Frontend.Elaborator]
M
main [in Mcltt.Entrypoint]N
nat_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]nat_glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
nat_to_exp [in Mcltt.Core.Syntactic.Syntax]
nbe_ty_sind [in Mcltt.Core.Semantic.NbE]
nbe_ty_ind [in Mcltt.Core.Semantic.NbE]
nbe_sind [in Mcltt.Core.Semantic.NbE]
nbe_ind [in Mcltt.Core.Semantic.NbE]
nbe_ty_impl [in Mcltt.Extraction.NbE]
nbe_ty_order_sind [in Mcltt.Extraction.NbE]
nbe_ty_order_rec [in Mcltt.Extraction.NbE]
nbe_ty_order_ind [in Mcltt.Extraction.NbE]
nbe_ty_order_rect [in Mcltt.Extraction.NbE]
nbe_impl [in Mcltt.Extraction.NbE]
nbe_order_sind [in Mcltt.Extraction.NbE]
nbe_order_rec [in Mcltt.Extraction.NbE]
nbe_order_ind [in Mcltt.Extraction.NbE]
nbe_order_rect [in Mcltt.Extraction.NbE]
neut_glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
ne_to_exp [in Mcltt.Core.Syntactic.Syntax]
ne_sind [in Mcltt.Core.Syntactic.Syntax]
ne_rec [in Mcltt.Core.Syntactic.Syntax]
ne_ind [in Mcltt.Core.Syntactic.Syntax]
ne_rect [in Mcltt.Core.Syntactic.Syntax]
nf_to_exp [in Mcltt.Core.Syntactic.Syntax]
nf_sind [in Mcltt.Core.Syntactic.Syntax]
nf_rec [in Mcltt.Core.Syntactic.Syntax]
nf_ind [in Mcltt.Core.Syntactic.Syntax]
nf_rect [in Mcltt.Core.Syntactic.Syntax]
nil_glu_sub_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
not_univ_pi [in Mcltt.Algorithmic.Subtyping.Definitions]
num_to_exp [in Mcltt.Core.Syntactic.Syntax]
P
per_ctx_subtyp_sind [in Mcltt.Core.Semantic.PER.Definitions]per_ctx_subtyp_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_sind [in Mcltt.Core.Semantic.PER.Definitions]
per_ctx_env_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_sind [in Mcltt.Core.Semantic.PER.Definitions]
per_subtyp_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_ind' [in Mcltt.Core.Semantic.PER.Definitions]
per_univ [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_strong_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_sind [in Mcltt.Core.Semantic.PER.Definitions]
per_univ_elem_core_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_ne_sind [in Mcltt.Core.Semantic.PER.Definitions]
per_ne_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_nat_sind [in Mcltt.Core.Semantic.PER.Definitions]
per_nat_ind [in Mcltt.Core.Semantic.PER.Definitions]
per_top_typ [in Mcltt.Core.Semantic.PER.Definitions]
per_top [in Mcltt.Core.Semantic.PER.Definitions]
per_bot [in Mcltt.Core.Semantic.PER.Definitions]
prog [in Mcltt.Frontend.Parser]
Q
q [in Mcltt.Core.Syntactic.Syntax]R
read_typ_impl [in Mcltt.Extraction.Readback]read_ne_impl [in Mcltt.Extraction.Readback]
read_nf_impl [in Mcltt.Extraction.Readback]
read_typ_order_sind [in Mcltt.Extraction.Readback]
read_typ_order_ind [in Mcltt.Extraction.Readback]
read_ne_order_sind [in Mcltt.Extraction.Readback]
read_ne_order_ind [in Mcltt.Extraction.Readback]
read_nf_order_sind [in Mcltt.Extraction.Readback]
read_nf_order_ind [in Mcltt.Extraction.Readback]
read_typ_mut_ind [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_mut_ind [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_mut_ind [in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_sind [in Mcltt.Core.Semantic.Readback.Definitions]
read_typ_ind [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_sind [in Mcltt.Core.Semantic.Readback.Definitions]
read_ne_ind [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_sind [in Mcltt.Core.Semantic.Readback.Definitions]
read_nf_ind [in Mcltt.Core.Semantic.Readback.Definitions]
rel_sub_under_ctx [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_sind [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_ind [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_under_ctx [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_sind [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_ind [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
rel_typ [in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_app_sind [in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_app_ind [in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval_sind [in Mcltt.Core.Semantic.PER.Definitions]
rel_mod_eval_ind [in Mcltt.Core.Semantic.PER.Definitions]
S
subtyping_impl [in Mcltt.Extraction.Subtyping]subtyping_order_sind [in Mcltt.Extraction.Subtyping]
subtyping_order_rec [in Mcltt.Extraction.Subtyping]
subtyping_order_ind [in Mcltt.Extraction.Subtyping]
subtyping_order_rect [in Mcltt.Extraction.Subtyping]
subtyping_nf_impl [in Mcltt.Extraction.Subtyping]
subtyp_under_ctx [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
sub_sind [in Mcltt.Core.Syntactic.Syntax]
sub_rec [in Mcltt.Core.Syntactic.Syntax]
sub_ind [in Mcltt.Core.Syntactic.Syntax]
sub_rect [in Mcltt.Core.Syntactic.Syntax]
sumbool_sumor_failable_bind [in Mcltt.Extraction.PseudoMonadic]
sumbool_failable_bind [in Mcltt.Extraction.PseudoMonadic]
sumor_sumbool_failable_bind [in Mcltt.Extraction.PseudoMonadic]
sumor_failable_bind [in Mcltt.Extraction.PseudoMonadic]
T
test_elab2 [in Mcltt.Frontend.Elaborator]test_elab [in Mcltt.Frontend.Elaborator]
type_check_closed [in Mcltt.Extraction.TypeCheck]
type_infer [in Mcltt.Extraction.TypeCheck]
type_check [in Mcltt.Extraction.TypeCheck]
type_infer_order_sind [in Mcltt.Extraction.TypeCheck]
type_infer_order_ind [in Mcltt.Extraction.TypeCheck]
type_check_order_sind [in Mcltt.Extraction.TypeCheck]
type_check_order_ind [in Mcltt.Extraction.TypeCheck]
U
univ_glu_exp_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]univ_glu_exp_pred' [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_typ_pred [in Mcltt.Core.Soundness.LogicalRelation.Definitions]
user_exp_sind [in Mcltt.Frontend.Elaborator]
user_exp_ind [in Mcltt.Frontend.Elaborator]
V
valid_sub_under_ctx [in Mcltt.Core.Completeness.LogicalRelation.Definitions]valid_exp_under_ctx [in Mcltt.Core.Completeness.LogicalRelation.Definitions]
valid_ctx [in Mcltt.Core.Semantic.PER.Definitions]
version_check [in Mcltt.Frontend.Parser]
W
weakening_sind [in Mcltt.Core.Soundness.Weakening.Definition]weakening_ind [in Mcltt.Core.Soundness.Weakening.Definition]
wf_ctx_eq_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_eq_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind' [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind' [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind' [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_subtyp_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_eq_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_eq_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_sub_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_exp_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sub_ind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_sind [in Mcltt.Core.Syntactic.System.Definitions]
wf_ctx_ind [in Mcltt.Core.Syntactic.System.Definitions]
_
__mark__ [in Mcltt.LibTactics]Record Index
P
PERElem [in Mcltt.LibTactics]| 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 | (1707 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 | (115 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 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 | (19 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 | (79 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 | (590 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 | (393 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (79 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (15 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (366 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |