| 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 | (318 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 | (22 entries) |
| Binder 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 | (208 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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 | (44 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 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 | (10 entries) |
Global Index
A
abs_arrow [lemma, in LambdaProj.Proofs]A:1 [binder, in LambdaProj.Infrastructure]
A:12 [binder, in LambdaProj.Infrastructure]
A:17 [binder, in LambdaProj.Infrastructure]
A:2 [binder, in LambdaProj.Infrastructure]
A:22 [binder, in LambdaProj.Infrastructure]
A:28 [binder, in LambdaProj.Infrastructure]
A:3 [binder, in LambdaProj.Infrastructure]
A:33 [binder, in LambdaProj.Infrastructure]
A:8 [binder, in LambdaProj.Infrastructure]
C
canonical_forms_of_arrow_types [lemma, in LambdaProj.Proofs]D
Definitions [library]E
empty [definition, in LambdaProj.Infrastructure]environment [definition, in LambdaProj.Definitions]
G
Gamma':48 [binder, in LambdaProj.Proofs]Gamma:104 [binder, in LambdaProj.Definitions]
Gamma:107 [binder, in LambdaProj.Definitions]
Gamma:114 [binder, in LambdaProj.Definitions]
Gamma:117 [binder, in LambdaProj.Definitions]
Gamma:122 [binder, in LambdaProj.Definitions]
Gamma:126 [binder, in LambdaProj.Definitions]
Gamma:127 [binder, in LambdaProj.Definitions]
Gamma:26 [binder, in LambdaProj.Proofs]
Gamma:37 [binder, in LambdaProj.Proofs]
Gamma:47 [binder, in LambdaProj.Proofs]
Gamma:51 [binder, in LambdaProj.Proofs]
Gamma:54 [binder, in LambdaProj.Proofs]
Gamma:6 [binder, in LambdaProj.Proofs]
H
has_type [inductive, in LambdaProj.Definitions]I
inclusion [definition, in LambdaProj.Infrastructure]inclusion_update [lemma, in LambdaProj.Infrastructure]
Infrastructure [library]
L
lookup_field_in_value [lemma, in LambdaProj.Proofs]l1:97 [binder, in LambdaProj.Definitions]
l2:98 [binder, in LambdaProj.Definitions]
l:1 [binder, in LambdaProj.Proofs]
l:118 [binder, in LambdaProj.Definitions]
l:12 [binder, in LambdaProj.Definitions]
l:128 [binder, in LambdaProj.Definitions]
l:13 [binder, in LambdaProj.Proofs]
l:18 [binder, in LambdaProj.Proofs]
l:19 [binder, in LambdaProj.Definitions]
l:32 [binder, in LambdaProj.Definitions]
l:35 [binder, in LambdaProj.Definitions]
l:39 [binder, in LambdaProj.Definitions]
l:57 [binder, in LambdaProj.Definitions]
l:59 [binder, in LambdaProj.Definitions]
l:61 [binder, in LambdaProj.Definitions]
l:65 [binder, in LambdaProj.Definitions]
l:7 [binder, in LambdaProj.Definitions]
l:89 [binder, in LambdaProj.Definitions]
l:92 [binder, in LambdaProj.Definitions]
M
multistep [inductive, in LambdaProj.Definitions]Multi_step [constructor, in LambdaProj.Definitions]
Multi_refl [constructor, in LambdaProj.Definitions]
m':30 [binder, in LambdaProj.Infrastructure]
m':35 [binder, in LambdaProj.Infrastructure]
m:13 [binder, in LambdaProj.Infrastructure]
m:18 [binder, in LambdaProj.Infrastructure]
m:23 [binder, in LambdaProj.Infrastructure]
m:29 [binder, in LambdaProj.Infrastructure]
m:34 [binder, in LambdaProj.Infrastructure]
m:4 [binder, in LambdaProj.Infrastructure]
m:9 [binder, in LambdaProj.Infrastructure]
N
normal_form [definition, in LambdaProj.Definitions]P
partial_map [definition, in LambdaProj.Infrastructure]preservation [lemma, in LambdaProj.Proofs]
progress [lemma, in LambdaProj.Proofs]
Proofs [library]
R
rcd_types_match [lemma, in LambdaProj.Proofs]record_tm [inductive, in LambdaProj.Definitions]
record_ty [inductive, in LambdaProj.Definitions]
rtcons [constructor, in LambdaProj.Definitions]
RTcons [constructor, in LambdaProj.Definitions]
rtnil [constructor, in LambdaProj.Definitions]
RTnil [constructor, in LambdaProj.Definitions]
R':11 [binder, in LambdaProj.Proofs]
R:12 [binder, in LambdaProj.Proofs]
R:120 [binder, in LambdaProj.Definitions]
r:16 [binder, in LambdaProj.Proofs]
R:17 [binder, in LambdaProj.Proofs]
R:2 [binder, in LambdaProj.Proofs]
R:81 [binder, in LambdaProj.Definitions]
S
Sr:94 [binder, in LambdaProj.Definitions]step [inductive, in LambdaProj.Definitions]
step_preserves_record_tm [lemma, in LambdaProj.Proofs]
stuck [definition, in LambdaProj.Definitions]
ST_Rcd_Tail [constructor, in LambdaProj.Definitions]
ST_Rcd_Head [constructor, in LambdaProj.Definitions]
ST_ProjRcd [constructor, in LambdaProj.Definitions]
ST_Proj1 [constructor, in LambdaProj.Definitions]
ST_App2 [constructor, in LambdaProj.Definitions]
ST_App1 [constructor, in LambdaProj.Definitions]
ST_AppAbs [constructor, in LambdaProj.Definitions]
subst [definition, in LambdaProj.Definitions]
substitution_preserves_typing [lemma, in LambdaProj.Proofs]
subtype [inductive, in LambdaProj.Definitions]
sub_inversion_arrow [lemma, in LambdaProj.Proofs]
S_RcdPerm [constructor, in LambdaProj.Definitions]
S_RcdDepth [constructor, in LambdaProj.Definitions]
S_RcdWidth [constructor, in LambdaProj.Definitions]
S_Arrow [constructor, in LambdaProj.Definitions]
S_Top [constructor, in LambdaProj.Definitions]
S_Trans [constructor, in LambdaProj.Definitions]
S_Refl [constructor, in LambdaProj.Definitions]
S1:24 [binder, in LambdaProj.Proofs]
S1:28 [binder, in LambdaProj.Proofs]
S1:33 [binder, in LambdaProj.Proofs]
S1:42 [binder, in LambdaProj.Proofs]
S1:85 [binder, in LambdaProj.Definitions]
S2:25 [binder, in LambdaProj.Proofs]
S2:31 [binder, in LambdaProj.Proofs]
s2:34 [binder, in LambdaProj.Proofs]
s2:43 [binder, in LambdaProj.Proofs]
S2:86 [binder, in LambdaProj.Definitions]
S:124 [binder, in LambdaProj.Definitions]
S:21 [binder, in LambdaProj.Proofs]
s:23 [binder, in LambdaProj.Definitions]
s:38 [binder, in LambdaProj.Proofs]
S:4 [binder, in LambdaProj.Proofs]
S:82 [binder, in LambdaProj.Definitions]
S:84 [binder, in LambdaProj.Definitions]
S:93 [binder, in LambdaProj.Definitions]
T
tlookup [definition, in LambdaProj.Definitions]Tlookup [definition, in LambdaProj.Definitions]
tm [inductive, in LambdaProj.Definitions]
tm_rcons [constructor, in LambdaProj.Definitions]
tm_rnil [constructor, in LambdaProj.Definitions]
tm_rproj [constructor, in LambdaProj.Definitions]
tm_abs [constructor, in LambdaProj.Definitions]
tm_app [constructor, in LambdaProj.Definitions]
tm_var [constructor, in LambdaProj.Definitions]
tr':10 [binder, in LambdaProj.Proofs]
tr':68 [binder, in LambdaProj.Definitions]
Tr:101 [binder, in LambdaProj.Definitions]
tr:131 [binder, in LambdaProj.Definitions]
Tr:132 [binder, in LambdaProj.Definitions]
tr:14 [binder, in LambdaProj.Definitions]
Tr:21 [binder, in LambdaProj.Definitions]
Tr:36 [binder, in LambdaProj.Definitions]
tr:40 [binder, in LambdaProj.Definitions]
tr:58 [binder, in LambdaProj.Definitions]
tr:64 [binder, in LambdaProj.Definitions]
tr:67 [binder, in LambdaProj.Definitions]
tr:9 [binder, in LambdaProj.Proofs]
Tr:9 [binder, in LambdaProj.Definitions]
Tr:91 [binder, in LambdaProj.Definitions]
Tr:96 [binder, in LambdaProj.Definitions]
ty [inductive, in LambdaProj.Definitions]
type_soundness [lemma, in LambdaProj.Proofs]
typing_inversion_abs [lemma, in LambdaProj.Proofs]
Ty_RCons [constructor, in LambdaProj.Definitions]
Ty_RNil [constructor, in LambdaProj.Definitions]
Ty_Arrow [constructor, in LambdaProj.Definitions]
Ty_Top [constructor, in LambdaProj.Definitions]
T_RCons [constructor, in LambdaProj.Definitions]
T_RNil [constructor, in LambdaProj.Definitions]
T_Sub [constructor, in LambdaProj.Definitions]
T_Proj [constructor, in LambdaProj.Definitions]
T_App [constructor, in LambdaProj.Definitions]
T_Abs [constructor, in LambdaProj.Definitions]
T_Var [constructor, in LambdaProj.Definitions]
T':15 [binder, in LambdaProj.Proofs]
t':46 [binder, in LambdaProj.Proofs]
t':61 [binder, in LambdaProj.Proofs]
t':63 [binder, in LambdaProj.Definitions]
t':64 [binder, in LambdaProj.Proofs]
t':76 [binder, in LambdaProj.Definitions]
t1':50 [binder, in LambdaProj.Definitions]
t1':56 [binder, in LambdaProj.Definitions]
T11:109 [binder, in LambdaProj.Definitions]
T12:110 [binder, in LambdaProj.Definitions]
t12:111 [binder, in LambdaProj.Definitions]
T1:112 [binder, in LambdaProj.Definitions]
t1:115 [binder, in LambdaProj.Definitions]
T1:17 [binder, in LambdaProj.Definitions]
T1:22 [binder, in LambdaProj.Proofs]
T1:35 [binder, in LambdaProj.Proofs]
T1:39 [binder, in LambdaProj.Proofs]
t1:47 [binder, in LambdaProj.Definitions]
t1:49 [binder, in LambdaProj.Definitions]
t1:55 [binder, in LambdaProj.Definitions]
t1:72 [binder, in LambdaProj.Definitions]
T1:87 [binder, in LambdaProj.Definitions]
T1:99 [binder, in LambdaProj.Definitions]
t2':54 [binder, in LambdaProj.Definitions]
T2:100 [binder, in LambdaProj.Definitions]
T2:113 [binder, in LambdaProj.Definitions]
t2:116 [binder, in LambdaProj.Definitions]
T2:18 [binder, in LambdaProj.Definitions]
T2:23 [binder, in LambdaProj.Proofs]
t2:29 [binder, in LambdaProj.Proofs]
T2:36 [binder, in LambdaProj.Proofs]
T2:40 [binder, in LambdaProj.Proofs]
T2:46 [binder, in LambdaProj.Definitions]
t2:51 [binder, in LambdaProj.Definitions]
t2:53 [binder, in LambdaProj.Definitions]
t2:73 [binder, in LambdaProj.Definitions]
T2:88 [binder, in LambdaProj.Definitions]
t3:74 [binder, in LambdaProj.Definitions]
T:106 [binder, in LambdaProj.Definitions]
t:119 [binder, in LambdaProj.Definitions]
T:121 [binder, in LambdaProj.Definitions]
t:123 [binder, in LambdaProj.Definitions]
T:125 [binder, in LambdaProj.Definitions]
t:129 [binder, in LambdaProj.Definitions]
t:13 [binder, in LambdaProj.Definitions]
T:130 [binder, in LambdaProj.Definitions]
T:14 [binder, in LambdaProj.Proofs]
T:19 [binder, in LambdaProj.Proofs]
T:20 [binder, in LambdaProj.Definitions]
t:24 [binder, in LambdaProj.Definitions]
T:3 [binder, in LambdaProj.Proofs]
T:30 [binder, in LambdaProj.Proofs]
T:30 [binder, in LambdaProj.Definitions]
t:31 [binder, in LambdaProj.Definitions]
t:44 [binder, in LambdaProj.Proofs]
T:45 [binder, in LambdaProj.Proofs]
t:49 [binder, in LambdaProj.Proofs]
T:5 [binder, in LambdaProj.Proofs]
T:50 [binder, in LambdaProj.Proofs]
t:52 [binder, in LambdaProj.Proofs]
T:53 [binder, in LambdaProj.Proofs]
t:57 [binder, in LambdaProj.Proofs]
T:59 [binder, in LambdaProj.Proofs]
t:60 [binder, in LambdaProj.Proofs]
T:62 [binder, in LambdaProj.Proofs]
t:62 [binder, in LambdaProj.Definitions]
t:63 [binder, in LambdaProj.Proofs]
T:65 [binder, in LambdaProj.Proofs]
t:7 [binder, in LambdaProj.Proofs]
t:71 [binder, in LambdaProj.Definitions]
t:75 [binder, in LambdaProj.Definitions]
t:77 [binder, in LambdaProj.Definitions]
T:8 [binder, in LambdaProj.Proofs]
T:8 [binder, in LambdaProj.Definitions]
T:80 [binder, in LambdaProj.Definitions]
T:83 [binder, in LambdaProj.Definitions]
T:90 [binder, in LambdaProj.Definitions]
T:95 [binder, in LambdaProj.Definitions]
U
update [definition, in LambdaProj.Infrastructure]update_permute [lemma, in LambdaProj.Infrastructure]
update_shadow [lemma, in LambdaProj.Infrastructure]
update_neq [lemma, in LambdaProj.Infrastructure]
update_eq [lemma, in LambdaProj.Infrastructure]
U:56 [binder, in LambdaProj.Proofs]
V
value [inductive, in LambdaProj.Definitions]vr:34 [binder, in LambdaProj.Definitions]
vx:37 [binder, in LambdaProj.Infrastructure]
v_rcons [constructor, in LambdaProj.Definitions]
v_rnil [constructor, in LambdaProj.Definitions]
v_abs [constructor, in LambdaProj.Definitions]
v1:20 [binder, in LambdaProj.Infrastructure]
v1:26 [binder, in LambdaProj.Infrastructure]
v1:52 [binder, in LambdaProj.Definitions]
v2:21 [binder, in LambdaProj.Infrastructure]
v2:27 [binder, in LambdaProj.Infrastructure]
v2:48 [binder, in LambdaProj.Definitions]
v:11 [binder, in LambdaProj.Infrastructure]
v:16 [binder, in LambdaProj.Infrastructure]
v:20 [binder, in LambdaProj.Proofs]
v:32 [binder, in LambdaProj.Infrastructure]
v:33 [binder, in LambdaProj.Definitions]
v:58 [binder, in LambdaProj.Proofs]
v:6 [binder, in LambdaProj.Infrastructure]
v:60 [binder, in LambdaProj.Definitions]
v:66 [binder, in LambdaProj.Definitions]
W
weakening [lemma, in LambdaProj.Proofs]weakening_empty [lemma, in LambdaProj.Proofs]
well_formed_ty [inductive, in LambdaProj.Definitions]
wfArrow [constructor, in LambdaProj.Definitions]
wfRCons [constructor, in LambdaProj.Definitions]
wfRNil [constructor, in LambdaProj.Definitions]
wfTop [constructor, in LambdaProj.Definitions]
wf_has_type [lemma, in LambdaProj.Proofs]
wf_subtype [lemma, in LambdaProj.Proofs]
wf_rcd_lookup [lemma, in LambdaProj.Proofs]
X
x':7 [binder, in LambdaProj.Infrastructure]x1:14 [binder, in LambdaProj.Infrastructure]
x1:24 [binder, in LambdaProj.Infrastructure]
x2:15 [binder, in LambdaProj.Infrastructure]
x2:25 [binder, in LambdaProj.Infrastructure]
x:10 [binder, in LambdaProj.Infrastructure]
x:105 [binder, in LambdaProj.Definitions]
x:108 [binder, in LambdaProj.Definitions]
x:19 [binder, in LambdaProj.Infrastructure]
x:22 [binder, in LambdaProj.Definitions]
x:27 [binder, in LambdaProj.Proofs]
x:29 [binder, in LambdaProj.Definitions]
x:31 [binder, in LambdaProj.Infrastructure]
x:32 [binder, in LambdaProj.Proofs]
x:36 [binder, in LambdaProj.Infrastructure]
x:41 [binder, in LambdaProj.Proofs]
x:45 [binder, in LambdaProj.Definitions]
x:5 [binder, in LambdaProj.Infrastructure]
x:55 [binder, in LambdaProj.Proofs]
other
stlc_ty:_ : _ :: _ [notation, in LambdaProj.Definitions]stlc_ty:nil [notation, in LambdaProj.Definitions]
stlc_ty:_ -> _ [notation, in LambdaProj.Definitions]
stlc_ty:Top [notation, in LambdaProj.Definitions]
stlc_ty:_ [notation, in LambdaProj.Definitions]
stlc_ty:( _ ) [notation, in LambdaProj.Definitions]
stlc:_ [notation, in LambdaProj.Definitions]
stlc:_ [ _ := _ ] [notation, in LambdaProj.Definitions]
stlc:_ = _ :: _ [notation, in LambdaProj.Definitions]
stlc:_ --> _ [notation, in LambdaProj.Definitions]
stlc:_ _ [notation, in LambdaProj.Definitions]
stlc:nil [notation, in LambdaProj.Definitions]
stlc:( _ ) [notation, in LambdaProj.Definitions]
stlc:\ _ : _ , _ [notation, in LambdaProj.Definitions]
_ |-> _ [notation, in LambdaProj.Infrastructure]
_ |-> _ ; _ [notation, in LambdaProj.Infrastructure]
_ |- _ : _ [notation, in LambdaProj.Definitions]
_ <: _ [notation, in LambdaProj.Definitions]
_ -->* _ [notation, in LambdaProj.Definitions]
_ --> _ [notation, in LambdaProj.Definitions]
<{ _ }> [notation, in LambdaProj.Definitions]
<{{ _ }}> [notation, in LambdaProj.Definitions]
Notation Index
other
stlc_ty:_ : _ :: _ [in LambdaProj.Definitions]stlc_ty:nil [in LambdaProj.Definitions]
stlc_ty:_ -> _ [in LambdaProj.Definitions]
stlc_ty:Top [in LambdaProj.Definitions]
stlc_ty:_ [in LambdaProj.Definitions]
stlc_ty:( _ ) [in LambdaProj.Definitions]
stlc:_ [in LambdaProj.Definitions]
stlc:_ [ _ := _ ] [in LambdaProj.Definitions]
stlc:_ = _ :: _ [in LambdaProj.Definitions]
stlc:_ --> _ [in LambdaProj.Definitions]
stlc:_ _ [in LambdaProj.Definitions]
stlc:nil [in LambdaProj.Definitions]
stlc:( _ ) [in LambdaProj.Definitions]
stlc:\ _ : _ , _ [in LambdaProj.Definitions]
_ |-> _ [in LambdaProj.Infrastructure]
_ |-> _ ; _ [in LambdaProj.Infrastructure]
_ |- _ : _ [in LambdaProj.Definitions]
_ <: _ [in LambdaProj.Definitions]
_ -->* _ [in LambdaProj.Definitions]
_ --> _ [in LambdaProj.Definitions]
<{ _ }> [in LambdaProj.Definitions]
<{{ _ }}> [in LambdaProj.Definitions]
Binder Index
A
A:1 [in LambdaProj.Infrastructure]A:12 [in LambdaProj.Infrastructure]
A:17 [in LambdaProj.Infrastructure]
A:2 [in LambdaProj.Infrastructure]
A:22 [in LambdaProj.Infrastructure]
A:28 [in LambdaProj.Infrastructure]
A:3 [in LambdaProj.Infrastructure]
A:33 [in LambdaProj.Infrastructure]
A:8 [in LambdaProj.Infrastructure]
G
Gamma':48 [in LambdaProj.Proofs]Gamma:104 [in LambdaProj.Definitions]
Gamma:107 [in LambdaProj.Definitions]
Gamma:114 [in LambdaProj.Definitions]
Gamma:117 [in LambdaProj.Definitions]
Gamma:122 [in LambdaProj.Definitions]
Gamma:126 [in LambdaProj.Definitions]
Gamma:127 [in LambdaProj.Definitions]
Gamma:26 [in LambdaProj.Proofs]
Gamma:37 [in LambdaProj.Proofs]
Gamma:47 [in LambdaProj.Proofs]
Gamma:51 [in LambdaProj.Proofs]
Gamma:54 [in LambdaProj.Proofs]
Gamma:6 [in LambdaProj.Proofs]
L
l1:97 [in LambdaProj.Definitions]l2:98 [in LambdaProj.Definitions]
l:1 [in LambdaProj.Proofs]
l:118 [in LambdaProj.Definitions]
l:12 [in LambdaProj.Definitions]
l:128 [in LambdaProj.Definitions]
l:13 [in LambdaProj.Proofs]
l:18 [in LambdaProj.Proofs]
l:19 [in LambdaProj.Definitions]
l:32 [in LambdaProj.Definitions]
l:35 [in LambdaProj.Definitions]
l:39 [in LambdaProj.Definitions]
l:57 [in LambdaProj.Definitions]
l:59 [in LambdaProj.Definitions]
l:61 [in LambdaProj.Definitions]
l:65 [in LambdaProj.Definitions]
l:7 [in LambdaProj.Definitions]
l:89 [in LambdaProj.Definitions]
l:92 [in LambdaProj.Definitions]
M
m':30 [in LambdaProj.Infrastructure]m':35 [in LambdaProj.Infrastructure]
m:13 [in LambdaProj.Infrastructure]
m:18 [in LambdaProj.Infrastructure]
m:23 [in LambdaProj.Infrastructure]
m:29 [in LambdaProj.Infrastructure]
m:34 [in LambdaProj.Infrastructure]
m:4 [in LambdaProj.Infrastructure]
m:9 [in LambdaProj.Infrastructure]
R
R':11 [in LambdaProj.Proofs]R:12 [in LambdaProj.Proofs]
R:120 [in LambdaProj.Definitions]
r:16 [in LambdaProj.Proofs]
R:17 [in LambdaProj.Proofs]
R:2 [in LambdaProj.Proofs]
R:81 [in LambdaProj.Definitions]
S
Sr:94 [in LambdaProj.Definitions]S1:24 [in LambdaProj.Proofs]
S1:28 [in LambdaProj.Proofs]
S1:33 [in LambdaProj.Proofs]
S1:42 [in LambdaProj.Proofs]
S1:85 [in LambdaProj.Definitions]
S2:25 [in LambdaProj.Proofs]
S2:31 [in LambdaProj.Proofs]
s2:34 [in LambdaProj.Proofs]
s2:43 [in LambdaProj.Proofs]
S2:86 [in LambdaProj.Definitions]
S:124 [in LambdaProj.Definitions]
S:21 [in LambdaProj.Proofs]
s:23 [in LambdaProj.Definitions]
s:38 [in LambdaProj.Proofs]
S:4 [in LambdaProj.Proofs]
S:82 [in LambdaProj.Definitions]
S:84 [in LambdaProj.Definitions]
S:93 [in LambdaProj.Definitions]
T
tr':10 [in LambdaProj.Proofs]tr':68 [in LambdaProj.Definitions]
Tr:101 [in LambdaProj.Definitions]
tr:131 [in LambdaProj.Definitions]
Tr:132 [in LambdaProj.Definitions]
tr:14 [in LambdaProj.Definitions]
Tr:21 [in LambdaProj.Definitions]
Tr:36 [in LambdaProj.Definitions]
tr:40 [in LambdaProj.Definitions]
tr:58 [in LambdaProj.Definitions]
tr:64 [in LambdaProj.Definitions]
tr:67 [in LambdaProj.Definitions]
tr:9 [in LambdaProj.Proofs]
Tr:9 [in LambdaProj.Definitions]
Tr:91 [in LambdaProj.Definitions]
Tr:96 [in LambdaProj.Definitions]
T':15 [in LambdaProj.Proofs]
t':46 [in LambdaProj.Proofs]
t':61 [in LambdaProj.Proofs]
t':63 [in LambdaProj.Definitions]
t':64 [in LambdaProj.Proofs]
t':76 [in LambdaProj.Definitions]
t1':50 [in LambdaProj.Definitions]
t1':56 [in LambdaProj.Definitions]
T11:109 [in LambdaProj.Definitions]
T12:110 [in LambdaProj.Definitions]
t12:111 [in LambdaProj.Definitions]
T1:112 [in LambdaProj.Definitions]
t1:115 [in LambdaProj.Definitions]
T1:17 [in LambdaProj.Definitions]
T1:22 [in LambdaProj.Proofs]
T1:35 [in LambdaProj.Proofs]
T1:39 [in LambdaProj.Proofs]
t1:47 [in LambdaProj.Definitions]
t1:49 [in LambdaProj.Definitions]
t1:55 [in LambdaProj.Definitions]
t1:72 [in LambdaProj.Definitions]
T1:87 [in LambdaProj.Definitions]
T1:99 [in LambdaProj.Definitions]
t2':54 [in LambdaProj.Definitions]
T2:100 [in LambdaProj.Definitions]
T2:113 [in LambdaProj.Definitions]
t2:116 [in LambdaProj.Definitions]
T2:18 [in LambdaProj.Definitions]
T2:23 [in LambdaProj.Proofs]
t2:29 [in LambdaProj.Proofs]
T2:36 [in LambdaProj.Proofs]
T2:40 [in LambdaProj.Proofs]
T2:46 [in LambdaProj.Definitions]
t2:51 [in LambdaProj.Definitions]
t2:53 [in LambdaProj.Definitions]
t2:73 [in LambdaProj.Definitions]
T2:88 [in LambdaProj.Definitions]
t3:74 [in LambdaProj.Definitions]
T:106 [in LambdaProj.Definitions]
t:119 [in LambdaProj.Definitions]
T:121 [in LambdaProj.Definitions]
t:123 [in LambdaProj.Definitions]
T:125 [in LambdaProj.Definitions]
t:129 [in LambdaProj.Definitions]
t:13 [in LambdaProj.Definitions]
T:130 [in LambdaProj.Definitions]
T:14 [in LambdaProj.Proofs]
T:19 [in LambdaProj.Proofs]
T:20 [in LambdaProj.Definitions]
t:24 [in LambdaProj.Definitions]
T:3 [in LambdaProj.Proofs]
T:30 [in LambdaProj.Proofs]
T:30 [in LambdaProj.Definitions]
t:31 [in LambdaProj.Definitions]
t:44 [in LambdaProj.Proofs]
T:45 [in LambdaProj.Proofs]
t:49 [in LambdaProj.Proofs]
T:5 [in LambdaProj.Proofs]
T:50 [in LambdaProj.Proofs]
t:52 [in LambdaProj.Proofs]
T:53 [in LambdaProj.Proofs]
t:57 [in LambdaProj.Proofs]
T:59 [in LambdaProj.Proofs]
t:60 [in LambdaProj.Proofs]
T:62 [in LambdaProj.Proofs]
t:62 [in LambdaProj.Definitions]
t:63 [in LambdaProj.Proofs]
T:65 [in LambdaProj.Proofs]
t:7 [in LambdaProj.Proofs]
t:71 [in LambdaProj.Definitions]
t:75 [in LambdaProj.Definitions]
t:77 [in LambdaProj.Definitions]
T:8 [in LambdaProj.Proofs]
T:8 [in LambdaProj.Definitions]
T:80 [in LambdaProj.Definitions]
T:83 [in LambdaProj.Definitions]
T:90 [in LambdaProj.Definitions]
T:95 [in LambdaProj.Definitions]
U
U:56 [in LambdaProj.Proofs]V
vr:34 [in LambdaProj.Definitions]vx:37 [in LambdaProj.Infrastructure]
v1:20 [in LambdaProj.Infrastructure]
v1:26 [in LambdaProj.Infrastructure]
v1:52 [in LambdaProj.Definitions]
v2:21 [in LambdaProj.Infrastructure]
v2:27 [in LambdaProj.Infrastructure]
v2:48 [in LambdaProj.Definitions]
v:11 [in LambdaProj.Infrastructure]
v:16 [in LambdaProj.Infrastructure]
v:20 [in LambdaProj.Proofs]
v:32 [in LambdaProj.Infrastructure]
v:33 [in LambdaProj.Definitions]
v:58 [in LambdaProj.Proofs]
v:6 [in LambdaProj.Infrastructure]
v:60 [in LambdaProj.Definitions]
v:66 [in LambdaProj.Definitions]
X
x':7 [in LambdaProj.Infrastructure]x1:14 [in LambdaProj.Infrastructure]
x1:24 [in LambdaProj.Infrastructure]
x2:15 [in LambdaProj.Infrastructure]
x2:25 [in LambdaProj.Infrastructure]
x:10 [in LambdaProj.Infrastructure]
x:105 [in LambdaProj.Definitions]
x:108 [in LambdaProj.Definitions]
x:19 [in LambdaProj.Infrastructure]
x:22 [in LambdaProj.Definitions]
x:27 [in LambdaProj.Proofs]
x:29 [in LambdaProj.Definitions]
x:31 [in LambdaProj.Infrastructure]
x:32 [in LambdaProj.Proofs]
x:36 [in LambdaProj.Infrastructure]
x:41 [in LambdaProj.Proofs]
x:45 [in LambdaProj.Definitions]
x:5 [in LambdaProj.Infrastructure]
x:55 [in LambdaProj.Proofs]
Library Index
D
DefinitionsI
InfrastructureP
ProofsLemma Index
A
abs_arrow [in LambdaProj.Proofs]C
canonical_forms_of_arrow_types [in LambdaProj.Proofs]I
inclusion_update [in LambdaProj.Infrastructure]L
lookup_field_in_value [in LambdaProj.Proofs]P
preservation [in LambdaProj.Proofs]progress [in LambdaProj.Proofs]
R
rcd_types_match [in LambdaProj.Proofs]S
step_preserves_record_tm [in LambdaProj.Proofs]substitution_preserves_typing [in LambdaProj.Proofs]
sub_inversion_arrow [in LambdaProj.Proofs]
T
type_soundness [in LambdaProj.Proofs]typing_inversion_abs [in LambdaProj.Proofs]
U
update_permute [in LambdaProj.Infrastructure]update_shadow [in LambdaProj.Infrastructure]
update_neq [in LambdaProj.Infrastructure]
update_eq [in LambdaProj.Infrastructure]
W
weakening [in LambdaProj.Proofs]weakening_empty [in LambdaProj.Proofs]
wf_has_type [in LambdaProj.Proofs]
wf_subtype [in LambdaProj.Proofs]
wf_rcd_lookup [in LambdaProj.Proofs]
Constructor Index
M
Multi_step [in LambdaProj.Definitions]Multi_refl [in LambdaProj.Definitions]
R
rtcons [in LambdaProj.Definitions]RTcons [in LambdaProj.Definitions]
rtnil [in LambdaProj.Definitions]
RTnil [in LambdaProj.Definitions]
S
ST_Rcd_Tail [in LambdaProj.Definitions]ST_Rcd_Head [in LambdaProj.Definitions]
ST_ProjRcd [in LambdaProj.Definitions]
ST_Proj1 [in LambdaProj.Definitions]
ST_App2 [in LambdaProj.Definitions]
ST_App1 [in LambdaProj.Definitions]
ST_AppAbs [in LambdaProj.Definitions]
S_RcdPerm [in LambdaProj.Definitions]
S_RcdDepth [in LambdaProj.Definitions]
S_RcdWidth [in LambdaProj.Definitions]
S_Arrow [in LambdaProj.Definitions]
S_Top [in LambdaProj.Definitions]
S_Trans [in LambdaProj.Definitions]
S_Refl [in LambdaProj.Definitions]
T
tm_rcons [in LambdaProj.Definitions]tm_rnil [in LambdaProj.Definitions]
tm_rproj [in LambdaProj.Definitions]
tm_abs [in LambdaProj.Definitions]
tm_app [in LambdaProj.Definitions]
tm_var [in LambdaProj.Definitions]
Ty_RCons [in LambdaProj.Definitions]
Ty_RNil [in LambdaProj.Definitions]
Ty_Arrow [in LambdaProj.Definitions]
Ty_Top [in LambdaProj.Definitions]
T_RCons [in LambdaProj.Definitions]
T_RNil [in LambdaProj.Definitions]
T_Sub [in LambdaProj.Definitions]
T_Proj [in LambdaProj.Definitions]
T_App [in LambdaProj.Definitions]
T_Abs [in LambdaProj.Definitions]
T_Var [in LambdaProj.Definitions]
V
v_rcons [in LambdaProj.Definitions]v_rnil [in LambdaProj.Definitions]
v_abs [in LambdaProj.Definitions]
W
wfArrow [in LambdaProj.Definitions]wfRCons [in LambdaProj.Definitions]
wfRNil [in LambdaProj.Definitions]
wfTop [in LambdaProj.Definitions]
Inductive Index
H
has_type [in LambdaProj.Definitions]M
multistep [in LambdaProj.Definitions]R
record_tm [in LambdaProj.Definitions]record_ty [in LambdaProj.Definitions]
S
step [in LambdaProj.Definitions]subtype [in LambdaProj.Definitions]
T
tm [in LambdaProj.Definitions]ty [in LambdaProj.Definitions]
V
value [in LambdaProj.Definitions]W
well_formed_ty [in LambdaProj.Definitions]Definition Index
E
empty [in LambdaProj.Infrastructure]environment [in LambdaProj.Definitions]
I
inclusion [in LambdaProj.Infrastructure]N
normal_form [in LambdaProj.Definitions]P
partial_map [in LambdaProj.Infrastructure]S
stuck [in LambdaProj.Definitions]subst [in LambdaProj.Definitions]
T
tlookup [in LambdaProj.Definitions]Tlookup [in LambdaProj.Definitions]
U
update [in LambdaProj.Infrastructure]| 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 | (318 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 | (22 entries) |
| Binder 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 | (208 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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 | (44 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 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 | (10 entries) |