| 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 | (466 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 | (328 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 | (1 entry) |
| File 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 | (31 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 | (74 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 | (7 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 | (22 entries) |
Global Index
A
A:114 [binder, in PCF.PCF]A:117 [binder, in PCF.PCF]
A:122 [binder, in PCF.PCF]
A:130 [binder, in PCF.PCF]
A:135 [binder, in PCF.PCF]
A:139 [binder, in PCF.PCF]
A:143 [binder, in PCF.PCF]
A:150 [binder, in PCF.PCF]
A:154 [binder, in PCF.PCF]
A:157 [binder, in PCF.PCF]
A:160 [binder, in PCF.PCF]
A:192 [binder, in PCF.PCF]
A:195 [binder, in PCF.PCF]
A:204 [binder, in PCF.PCF]
A:210 [binder, in PCF.PCF]
A:35 [binder, in PCF.CBN]
A:39 [binder, in PCF.CBV]
B
bigCBN [inductive, in PCF.CBN]bigCBN_bool [lemma, in PCF.CBN]
bigCBN_reduces_to_value [lemma, in PCF.CBN]
bigCBN_minus [constructor, in PCF.CBN]
bigCBN_mul [constructor, in PCF.CBN]
bigCBN_leq [constructor, in PCF.CBN]
bigCBN_ite_false [constructor, in PCF.CBN]
bigCBN_ite_true [constructor, in PCF.CBN]
bigCBN_fix [constructor, in PCF.CBN]
bigCBN_case_inr [constructor, in PCF.CBN]
bigCBN_case_inl [constructor, in PCF.CBN]
bigCBN_snd [constructor, in PCF.CBN]
bigCBN_fst [constructor, in PCF.CBN]
bigCBN_app [constructor, in PCF.CBN]
bigCBN_value [constructor, in PCF.CBN]
bigCBV [inductive, in PCF.CBV]
bigCBV_refl_bool [lemma, in PCF.CBV]
bigCBV_reduces_to_value [lemma, in PCF.CBV]
bigCBV_minus [constructor, in PCF.CBV]
bigCBV_mul [constructor, in PCF.CBV]
bigCBV_leq [constructor, in PCF.CBV]
bigCBV_ite_false [constructor, in PCF.CBV]
bigCBV_ite_true [constructor, in PCF.CBV]
bigCBV_fix [constructor, in PCF.CBV]
bigCBV_case_inr [constructor, in PCF.CBV]
bigCBV_case_inl [constructor, in PCF.CBV]
bigCBV_snd [constructor, in PCF.CBV]
bigCBV_fst [constructor, in PCF.CBV]
bigCBV_pair [constructor, in PCF.CBV]
bigCBV_app [constructor, in PCF.CBV]
bigCBV_value [constructor, in PCF.CBV]
b':25 [binder, in PCF.CBN]
b':28 [binder, in PCF.CBV]
b':30 [binder, in PCF.CBN]
b':33 [binder, in PCF.CBV]
B:119 [binder, in PCF.PCF]
B:123 [binder, in PCF.PCF]
B:132 [binder, in PCF.PCF]
B:136 [binder, in PCF.PCF]
B:140 [binder, in PCF.PCF]
b:142 [binder, in PCF.PCF]
B:144 [binder, in PCF.PCF]
B:151 [binder, in PCF.PCF]
B:155 [binder, in PCF.PCF]
b:172 [binder, in PCF.PCF]
b:190 [binder, in PCF.PCF]
B:213 [binder, in PCF.PCF]
b:24 [binder, in PCF.CBN]
b:27 [binder, in PCF.CBV]
b:29 [binder, in PCF.CBN]
b:32 [binder, in PCF.CBV]
b:37 [binder, in PCF.CBN]
B:40 [binder, in PCF.CBV]
b:41 [binder, in PCF.CBN]
b:42 [binder, in PCF.CBV]
b:46 [binder, in PCF.CBV]
b:62 [binder, in PCF.CBN]
b:67 [binder, in PCF.CBV]
b:68 [binder, in PCF.CBV]
b:74 [binder, in PCF.PCF]
b:76 [binder, in PCF.PCF]
b:80 [binder, in PCF.PCF]
b:83 [binder, in PCF.PCF]
C
CBN [file]CBV [file]
cempty [definition, in PCF.PCF]
clift [definition, in PCF.PCF]
clift_cupdate [lemma, in PCF.PCF]
context [definition, in PCF.PCF]
cupdate [definition, in PCF.PCF]
cupdate_clift_free [lemma, in PCF.PCF]
cupdate_clift_bound [lemma, in PCF.PCF]
c1:173 [binder, in PCF.PCF]
c2:176 [binder, in PCF.PCF]
c:115 [binder, in PCF.PCF]
c:116 [binder, in PCF.PCF]
c:12 [binder, in PCF.PCF]
c:120 [binder, in PCF.PCF]
c:125 [binder, in PCF.PCF]
c:126 [binder, in PCF.PCF]
c:128 [binder, in PCF.PCF]
c:133 [binder, in PCF.PCF]
c:137 [binder, in PCF.PCF]
c:141 [binder, in PCF.PCF]
C:146 [binder, in PCF.PCF]
c:148 [binder, in PCF.PCF]
c:152 [binder, in PCF.PCF]
c:156 [binder, in PCF.PCF]
c:158 [binder, in PCF.PCF]
c:162 [binder, in PCF.PCF]
c:165 [binder, in PCF.PCF]
c:168 [binder, in PCF.PCF]
c:17 [binder, in PCF.PCF]
c:171 [binder, in PCF.PCF]
c:179 [binder, in PCF.PCF]
c:184 [binder, in PCF.PCF]
c:189 [binder, in PCF.PCF]
c:194 [binder, in PCF.PCF]
c:197 [binder, in PCF.PCF]
c:20 [binder, in PCF.PCF]
c:203 [binder, in PCF.PCF]
c:208 [binder, in PCF.PCF]
c:211 [binder, in PCF.PCF]
C:215 [binder, in PCF.PCF]
c:3 [binder, in PCF.PCF]
c:8 [binder, in PCF.PCF]
D
deriv_ex_2 [definition, in PCF.PCF]F
fac [definition, in PCF.CBV]fixer:71 [binder, in PCF.CBV]
form [inductive, in PCF.PCF]
f_deriv_ex_1 [definition, in PCF.PCF]
f_deriv_ite [lemma, in PCF.PCF]
f_deriv_lift [lemma, in PCF.PCF]
f_deriv_cupdate [lemma, in PCF.PCF]
f_deriv_weakening [lemma, in PCF.PCF]
f_deriv_bool [lemma, in PCF.PCF]
f_deriv_minus [constructor, in PCF.PCF]
f_deriv_mul [constructor, in PCF.PCF]
f_deriv_leq [constructor, in PCF.PCF]
f_deriv_eq [constructor, in PCF.PCF]
f_deriv_fix [constructor, in PCF.PCF]
f_deriv_inr [constructor, in PCF.PCF]
f_deriv_inl [constructor, in PCF.PCF]
f_deriv_case [constructor, in PCF.PCF]
f_deriv_snd [constructor, in PCF.PCF]
f_deriv_fst [constructor, in PCF.PCF]
f_deriv_pair [constructor, in PCF.PCF]
f_deriv_nat [constructor, in PCF.PCF]
f_deriv_star [constructor, in PCF.PCF]
f_deriv_app [constructor, in PCF.PCF]
f_deriv_abs [constructor, in PCF.PCF]
f_deriv_var [constructor, in PCF.PCF]
f_deriv [inductive, in PCF.PCF]
f_ite [definition, in PCF.PCF]
f_bool [definition, in PCF.PCF]
f_minus [constructor, in PCF.PCF]
f_mul [constructor, in PCF.PCF]
f_leq [constructor, in PCF.PCF]
f_eq [constructor, in PCF.PCF]
f_fix [constructor, in PCF.PCF]
f_inr [constructor, in PCF.PCF]
f_inl [constructor, in PCF.PCF]
f_case [constructor, in PCF.PCF]
f_snd [constructor, in PCF.PCF]
f_fst [constructor, in PCF.PCF]
f_pair [constructor, in PCF.PCF]
f_nat [constructor, in PCF.PCF]
f_star [constructor, in PCF.PCF]
f_app [constructor, in PCF.PCF]
f_abs [constructor, in PCF.PCF]
f_var [constructor, in PCF.PCF]
f1:106 [binder, in PCF.PCF]
f1:198 [binder, in PCF.PCF]
f1:84 [binder, in PCF.PCF]
f1:87 [binder, in PCF.PCF]
f1:97 [binder, in PCF.PCF]
f2:107 [binder, in PCF.PCF]
f2:199 [binder, in PCF.PCF]
f2:85 [binder, in PCF.PCF]
f2:88 [binder, in PCF.PCF]
f2:98 [binder, in PCF.PCF]
f3:108 [binder, in PCF.PCF]
f3:86 [binder, in PCF.PCF]
f3:89 [binder, in PCF.PCF]
f3:99 [binder, in PCF.PCF]
f:100 [binder, in PCF.PCF]
f:174 [binder, in PCF.PCF]
f:180 [binder, in PCF.PCF]
f:185 [binder, in PCF.PCF]
f:196 [binder, in PCF.PCF]
f:200 [binder, in PCF.PCF]
f:202 [binder, in PCF.PCF]
f:27 [binder, in PCF.PCF]
f:33 [binder, in PCF.PCF]
f:34 [binder, in PCF.CBN]
f:35 [binder, in PCF.PCF]
f:37 [binder, in PCF.CBV]
f:39 [binder, in PCF.PCF]
f:41 [binder, in PCF.PCF]
f:43 [binder, in PCF.PCF]
f:49 [binder, in PCF.PCF]
f:51 [binder, in PCF.PCF]
f:55 [binder, in PCF.PCF]
f:59 [binder, in PCF.PCF]
f:62 [binder, in PCF.PCF]
f:65 [binder, in PCF.PCF]
f:69 [binder, in PCF.PCF]
f:91 [binder, in PCF.PCF]
G
g:38 [binder, in PCF.CBV]g:70 [binder, in PCF.CBV]
I
is_term [definition, in PCF.PCF]is_closed [definition, in PCF.PCF]
i1:53 [binder, in PCF.PCF]
i2:54 [binder, in PCF.PCF]
i:11 [binder, in PCF.PCF]
i:16 [binder, in PCF.PCF]
i:188 [binder, in PCF.PCF]
i:22 [binder, in PCF.PCF]
i:45 [binder, in PCF.PCF]
i:58 [binder, in PCF.PCF]
i:67 [binder, in PCF.PCF]
i:7 [binder, in PCF.PCF]
i:79 [binder, in PCF.PCF]
i:94 [binder, in PCF.PCF]
i:96 [binder, in PCF.PCF]
K
k1:56 [binder, in PCF.PCF]k1:92 [binder, in PCF.PCF]
k2:57 [binder, in PCF.PCF]
k2:93 [binder, in PCF.PCF]
k:10 [binder, in PCF.PCF]
k:101 [binder, in PCF.PCF]
k:15 [binder, in PCF.PCF]
k:187 [binder, in PCF.PCF]
k:21 [binder, in PCF.PCF]
k:44 [binder, in PCF.PCF]
k:50 [binder, in PCF.PCF]
k:52 [binder, in PCF.PCF]
k:6 [binder, in PCF.PCF]
k:60 [binder, in PCF.PCF]
k:63 [binder, in PCF.PCF]
k:66 [binder, in PCF.PCF]
k:78 [binder, in PCF.PCF]
k:95 [binder, in PCF.PCF]
L
lift [definition, in PCF.PCF]lift_f_ite [lemma, in PCF.PCF]
lift_f_ite_helper [lemma, in PCF.PCF]
lift_f_bool [lemma, in PCF.PCF]
lift_comp [lemma, in PCF.PCF]
lift_additive [lemma, in PCF.PCF]
lift_k_0 [definition, in PCF.PCF]
M
MaybeMonad [module, in PCF.PCF]MaybeMonad.bind [lemma, in PCF.PCF]
MaybeMonad.f_do [definition, in PCF.PCF]
MaybeMonad.f_return [definition, in PCF.PCF]
MaybeMonad.M [definition, in PCF.PCF]
MaybeMonad.ret [lemma, in PCF.PCF]
m:47 [binder, in PCF.CBN]
m:52 [binder, in PCF.CBV]
m:52 [binder, in PCF.CBN]
m:57 [binder, in PCF.CBV]
m:57 [binder, in PCF.CBN]
m:62 [binder, in PCF.CBV]
m:69 [binder, in PCF.CBV]
N
negative_occ_lift [lemma, in PCF.PCF]n':104 [binder, in PCF.PCF]
n':105 [binder, in PCF.PCF]
n1:45 [binder, in PCF.CBN]
n1:50 [binder, in PCF.CBV]
n1:50 [binder, in PCF.CBN]
n1:55 [binder, in PCF.CBV]
n1:55 [binder, in PCF.CBN]
n1:60 [binder, in PCF.CBV]
n2:46 [binder, in PCF.CBN]
n2:51 [binder, in PCF.CBV]
n2:51 [binder, in PCF.CBN]
n2:56 [binder, in PCF.CBV]
n2:56 [binder, in PCF.CBN]
n2:61 [binder, in PCF.CBV]
n:127 [binder, in PCF.PCF]
n:4 [binder, in PCF.CBV]
n:4 [binder, in PCF.CBN]
n:73 [binder, in PCF.CBV]
n:76 [binder, in PCF.CBV]
O
occ [definition, in PCF.PCF]occ_f_ite [lemma, in PCF.PCF]
occ_f_bool [lemma, in PCF.PCF]
occ_lift_reverse_k_1 [lemma, in PCF.PCF]
occ_lift_k_1 [lemma, in PCF.PCF]
occ_occ' [lemma, in PCF.PCF]
occ_list [definition, in PCF.PCF]
occ' [definition, in PCF.PCF]
occ'_occ [lemma, in PCF.PCF]
P
PCF [file]pcf_fac_reduces_to_fac [lemma, in PCF.CBV]
pcf_fac_type [lemma, in PCF.CBV]
pcf_fac [definition, in PCF.CBV]
p':13 [binder, in PCF.CBV]
p':13 [binder, in PCF.CBN]
p:12 [binder, in PCF.CBV]
p:12 [binder, in PCF.CBN]
p:145 [binder, in PCF.PCF]
p:17 [binder, in PCF.CBV]
p:17 [binder, in PCF.CBN]
p:206 [binder, in PCF.PCF]
p:21 [binder, in PCF.CBV]
p:21 [binder, in PCF.CBN]
p:212 [binder, in PCF.PCF]
p:24 [binder, in PCF.CBV]
p:26 [binder, in PCF.CBN]
p:29 [binder, in PCF.CBV]
p:31 [binder, in PCF.CBN]
p:34 [binder, in PCF.CBV]
p:38 [binder, in PCF.CBN]
p:42 [binder, in PCF.CBN]
p:43 [binder, in PCF.CBV]
p:47 [binder, in PCF.CBV]
p:48 [binder, in PCF.CBN]
p:53 [binder, in PCF.CBV]
p:53 [binder, in PCF.CBN]
p:58 [binder, in PCF.CBV]
p:58 [binder, in PCF.CBN]
p:60 [binder, in PCF.CBN]
p:63 [binder, in PCF.CBV]
p:65 [binder, in PCF.CBV]
Q
q':15 [binder, in PCF.CBV]q:14 [binder, in PCF.CBV]
q:14 [binder, in PCF.CBN]
q:147 [binder, in PCF.PCF]
q:18 [binder, in PCF.CBN]
q:19 [binder, in PCF.CBV]
q:207 [binder, in PCF.PCF]
q:214 [binder, in PCF.PCF]
q:22 [binder, in PCF.CBN]
q:28 [binder, in PCF.CBN]
q:31 [binder, in PCF.CBV]
q:33 [binder, in PCF.CBN]
q:36 [binder, in PCF.CBV]
q:40 [binder, in PCF.CBN]
q:44 [binder, in PCF.CBN]
q:45 [binder, in PCF.CBV]
q:49 [binder, in PCF.CBV]
q:49 [binder, in PCF.CBN]
q:54 [binder, in PCF.CBV]
q:54 [binder, in PCF.CBN]
q:59 [binder, in PCF.CBV]
q:59 [binder, in PCF.CBN]
q:64 [binder, in PCF.CBV]
R
r1:18 [binder, in PCF.CBV]r1:22 [binder, in PCF.CBV]
r1:25 [binder, in PCF.CBV]
r2:20 [binder, in PCF.CBV]
r2:23 [binder, in PCF.CBV]
r2:26 [binder, in PCF.CBV]
r:15 [binder, in PCF.CBN]
r:16 [binder, in PCF.CBV]
r:19 [binder, in PCF.CBN]
r:23 [binder, in PCF.CBN]
r:27 [binder, in PCF.CBN]
r:30 [binder, in PCF.CBV]
r:32 [binder, in PCF.CBN]
r:35 [binder, in PCF.CBV]
r:36 [binder, in PCF.CBN]
r:39 [binder, in PCF.CBN]
r:41 [binder, in PCF.CBV]
r:43 [binder, in PCF.CBN]
r:44 [binder, in PCF.CBV]
r:48 [binder, in PCF.CBV]
S
subst [definition, in PCF.PCF]subst_f_ite [lemma, in PCF.PCF]
subst_f_ite_helper [lemma, in PCF.PCF]
subst_f_bool [lemma, in PCF.PCF]
s:103 [binder, in PCF.PCF]
s:110 [binder, in PCF.PCF]
s:121 [binder, in PCF.PCF]
s:131 [binder, in PCF.PCF]
s:159 [binder, in PCF.PCF]
s:164 [binder, in PCF.PCF]
s:167 [binder, in PCF.PCF]
s:170 [binder, in PCF.PCF]
s:191 [binder, in PCF.PCF]
s:6 [binder, in PCF.CBV]
s:6 [binder, in PCF.CBN]
s:71 [binder, in PCF.PCF]
s:82 [binder, in PCF.PCF]
T
type [inductive, in PCF.PCF]ty_bool [definition, in PCF.PCF]
ty_sum [constructor, in PCF.PCF]
ty_prod [constructor, in PCF.PCF]
ty_nat [constructor, in PCF.PCF]
ty_unit [constructor, in PCF.PCF]
ty_func [constructor, in PCF.PCF]
ty:201 [binder, in PCF.PCF]
ty:205 [binder, in PCF.PCF]
ty:5 [binder, in PCF.PCF]
ty:72 [binder, in PCF.CBV]
T1:175 [binder, in PCF.PCF]
T1:178 [binder, in PCF.PCF]
T1:181 [binder, in PCF.PCF]
T2:183 [binder, in PCF.PCF]
t:118 [binder, in PCF.PCF]
t:124 [binder, in PCF.PCF]
t:129 [binder, in PCF.PCF]
T:13 [binder, in PCF.PCF]
t:134 [binder, in PCF.PCF]
t:138 [binder, in PCF.PCF]
t:149 [binder, in PCF.PCF]
t:153 [binder, in PCF.PCF]
t:16 [binder, in PCF.CBN]
t:161 [binder, in PCF.PCF]
t:163 [binder, in PCF.PCF]
t:166 [binder, in PCF.PCF]
t:169 [binder, in PCF.PCF]
T:18 [binder, in PCF.PCF]
T:186 [binder, in PCF.PCF]
t:193 [binder, in PCF.PCF]
t:20 [binder, in PCF.CBN]
t:209 [binder, in PCF.PCF]
T:23 [binder, in PCF.PCF]
t:3 [binder, in PCF.CBV]
t:3 [binder, in PCF.CBN]
t:46 [binder, in PCF.PCF]
t:5 [binder, in PCF.CBV]
t:5 [binder, in PCF.CBN]
t:7 [binder, in PCF.CBV]
t:7 [binder, in PCF.CBN]
t:8 [binder, in PCF.CBV]
t:8 [binder, in PCF.CBN]
V
value [inductive, in PCF.CBV]value [inductive, in PCF.CBN]
v_inr [constructor, in PCF.CBV]
v_inl [constructor, in PCF.CBV]
v_pair [constructor, in PCF.CBV]
v_nat [constructor, in PCF.CBV]
v_star [constructor, in PCF.CBV]
v_abs [constructor, in PCF.CBV]
v_inr [constructor, in PCF.CBN]
v_inl [constructor, in PCF.CBN]
v_pair [constructor, in PCF.CBN]
v_nat [constructor, in PCF.CBN]
v_star [constructor, in PCF.CBN]
v_abs [constructor, in PCF.CBN]
v:11 [binder, in PCF.CBV]
v:11 [binder, in PCF.CBN]
v:182 [binder, in PCF.PCF]
v:61 [binder, in PCF.CBN]
v:66 [binder, in PCF.CBV]
X
x:102 [binder, in PCF.PCF]x:109 [binder, in PCF.PCF]
x:113 [binder, in PCF.PCF]
x:14 [binder, in PCF.PCF]
x:177 [binder, in PCF.PCF]
x:19 [binder, in PCF.PCF]
x:24 [binder, in PCF.PCF]
x:30 [binder, in PCF.PCF]
x:31 [binder, in PCF.PCF]
x:32 [binder, in PCF.PCF]
x:34 [binder, in PCF.PCF]
x:36 [binder, in PCF.PCF]
x:4 [binder, in PCF.PCF]
x:40 [binder, in PCF.PCF]
x:42 [binder, in PCF.PCF]
x:61 [binder, in PCF.PCF]
x:64 [binder, in PCF.PCF]
x:68 [binder, in PCF.PCF]
x:70 [binder, in PCF.PCF]
x:77 [binder, in PCF.PCF]
x:81 [binder, in PCF.PCF]
x:9 [binder, in PCF.PCF]
x:90 [binder, in PCF.PCF]
Binder Index
A
A:114 [in PCF.PCF]A:117 [in PCF.PCF]
A:122 [in PCF.PCF]
A:130 [in PCF.PCF]
A:135 [in PCF.PCF]
A:139 [in PCF.PCF]
A:143 [in PCF.PCF]
A:150 [in PCF.PCF]
A:154 [in PCF.PCF]
A:157 [in PCF.PCF]
A:160 [in PCF.PCF]
A:192 [in PCF.PCF]
A:195 [in PCF.PCF]
A:204 [in PCF.PCF]
A:210 [in PCF.PCF]
A:35 [in PCF.CBN]
A:39 [in PCF.CBV]
B
b':25 [in PCF.CBN]b':28 [in PCF.CBV]
b':30 [in PCF.CBN]
b':33 [in PCF.CBV]
B:119 [in PCF.PCF]
B:123 [in PCF.PCF]
B:132 [in PCF.PCF]
B:136 [in PCF.PCF]
B:140 [in PCF.PCF]
b:142 [in PCF.PCF]
B:144 [in PCF.PCF]
B:151 [in PCF.PCF]
B:155 [in PCF.PCF]
b:172 [in PCF.PCF]
b:190 [in PCF.PCF]
B:213 [in PCF.PCF]
b:24 [in PCF.CBN]
b:27 [in PCF.CBV]
b:29 [in PCF.CBN]
b:32 [in PCF.CBV]
b:37 [in PCF.CBN]
B:40 [in PCF.CBV]
b:41 [in PCF.CBN]
b:42 [in PCF.CBV]
b:46 [in PCF.CBV]
b:62 [in PCF.CBN]
b:67 [in PCF.CBV]
b:68 [in PCF.CBV]
b:74 [in PCF.PCF]
b:76 [in PCF.PCF]
b:80 [in PCF.PCF]
b:83 [in PCF.PCF]
C
c1:173 [in PCF.PCF]c2:176 [in PCF.PCF]
c:115 [in PCF.PCF]
c:116 [in PCF.PCF]
c:12 [in PCF.PCF]
c:120 [in PCF.PCF]
c:125 [in PCF.PCF]
c:126 [in PCF.PCF]
c:128 [in PCF.PCF]
c:133 [in PCF.PCF]
c:137 [in PCF.PCF]
c:141 [in PCF.PCF]
C:146 [in PCF.PCF]
c:148 [in PCF.PCF]
c:152 [in PCF.PCF]
c:156 [in PCF.PCF]
c:158 [in PCF.PCF]
c:162 [in PCF.PCF]
c:165 [in PCF.PCF]
c:168 [in PCF.PCF]
c:17 [in PCF.PCF]
c:171 [in PCF.PCF]
c:179 [in PCF.PCF]
c:184 [in PCF.PCF]
c:189 [in PCF.PCF]
c:194 [in PCF.PCF]
c:197 [in PCF.PCF]
c:20 [in PCF.PCF]
c:203 [in PCF.PCF]
c:208 [in PCF.PCF]
c:211 [in PCF.PCF]
C:215 [in PCF.PCF]
c:3 [in PCF.PCF]
c:8 [in PCF.PCF]
F
fixer:71 [in PCF.CBV]f1:106 [in PCF.PCF]
f1:198 [in PCF.PCF]
f1:84 [in PCF.PCF]
f1:87 [in PCF.PCF]
f1:97 [in PCF.PCF]
f2:107 [in PCF.PCF]
f2:199 [in PCF.PCF]
f2:85 [in PCF.PCF]
f2:88 [in PCF.PCF]
f2:98 [in PCF.PCF]
f3:108 [in PCF.PCF]
f3:86 [in PCF.PCF]
f3:89 [in PCF.PCF]
f3:99 [in PCF.PCF]
f:100 [in PCF.PCF]
f:174 [in PCF.PCF]
f:180 [in PCF.PCF]
f:185 [in PCF.PCF]
f:196 [in PCF.PCF]
f:200 [in PCF.PCF]
f:202 [in PCF.PCF]
f:27 [in PCF.PCF]
f:33 [in PCF.PCF]
f:34 [in PCF.CBN]
f:35 [in PCF.PCF]
f:37 [in PCF.CBV]
f:39 [in PCF.PCF]
f:41 [in PCF.PCF]
f:43 [in PCF.PCF]
f:49 [in PCF.PCF]
f:51 [in PCF.PCF]
f:55 [in PCF.PCF]
f:59 [in PCF.PCF]
f:62 [in PCF.PCF]
f:65 [in PCF.PCF]
f:69 [in PCF.PCF]
f:91 [in PCF.PCF]
G
g:38 [in PCF.CBV]g:70 [in PCF.CBV]
I
i1:53 [in PCF.PCF]i2:54 [in PCF.PCF]
i:11 [in PCF.PCF]
i:16 [in PCF.PCF]
i:188 [in PCF.PCF]
i:22 [in PCF.PCF]
i:45 [in PCF.PCF]
i:58 [in PCF.PCF]
i:67 [in PCF.PCF]
i:7 [in PCF.PCF]
i:79 [in PCF.PCF]
i:94 [in PCF.PCF]
i:96 [in PCF.PCF]
K
k1:56 [in PCF.PCF]k1:92 [in PCF.PCF]
k2:57 [in PCF.PCF]
k2:93 [in PCF.PCF]
k:10 [in PCF.PCF]
k:101 [in PCF.PCF]
k:15 [in PCF.PCF]
k:187 [in PCF.PCF]
k:21 [in PCF.PCF]
k:44 [in PCF.PCF]
k:50 [in PCF.PCF]
k:52 [in PCF.PCF]
k:6 [in PCF.PCF]
k:60 [in PCF.PCF]
k:63 [in PCF.PCF]
k:66 [in PCF.PCF]
k:78 [in PCF.PCF]
k:95 [in PCF.PCF]
M
m:47 [in PCF.CBN]m:52 [in PCF.CBV]
m:52 [in PCF.CBN]
m:57 [in PCF.CBV]
m:57 [in PCF.CBN]
m:62 [in PCF.CBV]
m:69 [in PCF.CBV]
N
n':104 [in PCF.PCF]n':105 [in PCF.PCF]
n1:45 [in PCF.CBN]
n1:50 [in PCF.CBV]
n1:50 [in PCF.CBN]
n1:55 [in PCF.CBV]
n1:55 [in PCF.CBN]
n1:60 [in PCF.CBV]
n2:46 [in PCF.CBN]
n2:51 [in PCF.CBV]
n2:51 [in PCF.CBN]
n2:56 [in PCF.CBV]
n2:56 [in PCF.CBN]
n2:61 [in PCF.CBV]
n:127 [in PCF.PCF]
n:4 [in PCF.CBV]
n:4 [in PCF.CBN]
n:73 [in PCF.CBV]
n:76 [in PCF.CBV]
P
p':13 [in PCF.CBV]p':13 [in PCF.CBN]
p:12 [in PCF.CBV]
p:12 [in PCF.CBN]
p:145 [in PCF.PCF]
p:17 [in PCF.CBV]
p:17 [in PCF.CBN]
p:206 [in PCF.PCF]
p:21 [in PCF.CBV]
p:21 [in PCF.CBN]
p:212 [in PCF.PCF]
p:24 [in PCF.CBV]
p:26 [in PCF.CBN]
p:29 [in PCF.CBV]
p:31 [in PCF.CBN]
p:34 [in PCF.CBV]
p:38 [in PCF.CBN]
p:42 [in PCF.CBN]
p:43 [in PCF.CBV]
p:47 [in PCF.CBV]
p:48 [in PCF.CBN]
p:53 [in PCF.CBV]
p:53 [in PCF.CBN]
p:58 [in PCF.CBV]
p:58 [in PCF.CBN]
p:60 [in PCF.CBN]
p:63 [in PCF.CBV]
p:65 [in PCF.CBV]
Q
q':15 [in PCF.CBV]q:14 [in PCF.CBV]
q:14 [in PCF.CBN]
q:147 [in PCF.PCF]
q:18 [in PCF.CBN]
q:19 [in PCF.CBV]
q:207 [in PCF.PCF]
q:214 [in PCF.PCF]
q:22 [in PCF.CBN]
q:28 [in PCF.CBN]
q:31 [in PCF.CBV]
q:33 [in PCF.CBN]
q:36 [in PCF.CBV]
q:40 [in PCF.CBN]
q:44 [in PCF.CBN]
q:45 [in PCF.CBV]
q:49 [in PCF.CBV]
q:49 [in PCF.CBN]
q:54 [in PCF.CBV]
q:54 [in PCF.CBN]
q:59 [in PCF.CBV]
q:59 [in PCF.CBN]
q:64 [in PCF.CBV]
R
r1:18 [in PCF.CBV]r1:22 [in PCF.CBV]
r1:25 [in PCF.CBV]
r2:20 [in PCF.CBV]
r2:23 [in PCF.CBV]
r2:26 [in PCF.CBV]
r:15 [in PCF.CBN]
r:16 [in PCF.CBV]
r:19 [in PCF.CBN]
r:23 [in PCF.CBN]
r:27 [in PCF.CBN]
r:30 [in PCF.CBV]
r:32 [in PCF.CBN]
r:35 [in PCF.CBV]
r:36 [in PCF.CBN]
r:39 [in PCF.CBN]
r:41 [in PCF.CBV]
r:43 [in PCF.CBN]
r:44 [in PCF.CBV]
r:48 [in PCF.CBV]
S
s:103 [in PCF.PCF]s:110 [in PCF.PCF]
s:121 [in PCF.PCF]
s:131 [in PCF.PCF]
s:159 [in PCF.PCF]
s:164 [in PCF.PCF]
s:167 [in PCF.PCF]
s:170 [in PCF.PCF]
s:191 [in PCF.PCF]
s:6 [in PCF.CBV]
s:6 [in PCF.CBN]
s:71 [in PCF.PCF]
s:82 [in PCF.PCF]
T
ty:201 [in PCF.PCF]ty:205 [in PCF.PCF]
ty:5 [in PCF.PCF]
ty:72 [in PCF.CBV]
T1:175 [in PCF.PCF]
T1:178 [in PCF.PCF]
T1:181 [in PCF.PCF]
T2:183 [in PCF.PCF]
t:118 [in PCF.PCF]
t:124 [in PCF.PCF]
t:129 [in PCF.PCF]
T:13 [in PCF.PCF]
t:134 [in PCF.PCF]
t:138 [in PCF.PCF]
t:149 [in PCF.PCF]
t:153 [in PCF.PCF]
t:16 [in PCF.CBN]
t:161 [in PCF.PCF]
t:163 [in PCF.PCF]
t:166 [in PCF.PCF]
t:169 [in PCF.PCF]
T:18 [in PCF.PCF]
T:186 [in PCF.PCF]
t:193 [in PCF.PCF]
t:20 [in PCF.CBN]
t:209 [in PCF.PCF]
T:23 [in PCF.PCF]
t:3 [in PCF.CBV]
t:3 [in PCF.CBN]
t:46 [in PCF.PCF]
t:5 [in PCF.CBV]
t:5 [in PCF.CBN]
t:7 [in PCF.CBV]
t:7 [in PCF.CBN]
t:8 [in PCF.CBV]
t:8 [in PCF.CBN]
V
v:11 [in PCF.CBV]v:11 [in PCF.CBN]
v:182 [in PCF.PCF]
v:61 [in PCF.CBN]
v:66 [in PCF.CBV]
X
x:102 [in PCF.PCF]x:109 [in PCF.PCF]
x:113 [in PCF.PCF]
x:14 [in PCF.PCF]
x:177 [in PCF.PCF]
x:19 [in PCF.PCF]
x:24 [in PCF.PCF]
x:30 [in PCF.PCF]
x:31 [in PCF.PCF]
x:32 [in PCF.PCF]
x:34 [in PCF.PCF]
x:36 [in PCF.PCF]
x:4 [in PCF.PCF]
x:40 [in PCF.PCF]
x:42 [in PCF.PCF]
x:61 [in PCF.PCF]
x:64 [in PCF.PCF]
x:68 [in PCF.PCF]
x:70 [in PCF.PCF]
x:77 [in PCF.PCF]
x:81 [in PCF.PCF]
x:9 [in PCF.PCF]
x:90 [in PCF.PCF]
Module Index
M
MaybeMonad [in PCF.PCF]File Index
C
CBNCBV
P
PCFLemma Index
B
bigCBN_bool [in PCF.CBN]bigCBN_reduces_to_value [in PCF.CBN]
bigCBV_refl_bool [in PCF.CBV]
bigCBV_reduces_to_value [in PCF.CBV]
C
clift_cupdate [in PCF.PCF]cupdate_clift_free [in PCF.PCF]
cupdate_clift_bound [in PCF.PCF]
F
f_deriv_ite [in PCF.PCF]f_deriv_lift [in PCF.PCF]
f_deriv_cupdate [in PCF.PCF]
f_deriv_weakening [in PCF.PCF]
f_deriv_bool [in PCF.PCF]
L
lift_f_ite [in PCF.PCF]lift_f_ite_helper [in PCF.PCF]
lift_f_bool [in PCF.PCF]
lift_comp [in PCF.PCF]
lift_additive [in PCF.PCF]
M
MaybeMonad.bind [in PCF.PCF]MaybeMonad.ret [in PCF.PCF]
N
negative_occ_lift [in PCF.PCF]O
occ_f_ite [in PCF.PCF]occ_f_bool [in PCF.PCF]
occ_lift_reverse_k_1 [in PCF.PCF]
occ_lift_k_1 [in PCF.PCF]
occ_occ' [in PCF.PCF]
occ'_occ [in PCF.PCF]
P
pcf_fac_reduces_to_fac [in PCF.CBV]pcf_fac_type [in PCF.CBV]
S
subst_f_ite [in PCF.PCF]subst_f_ite_helper [in PCF.PCF]
subst_f_bool [in PCF.PCF]
Constructor Index
B
bigCBN_minus [in PCF.CBN]bigCBN_mul [in PCF.CBN]
bigCBN_leq [in PCF.CBN]
bigCBN_ite_false [in PCF.CBN]
bigCBN_ite_true [in PCF.CBN]
bigCBN_fix [in PCF.CBN]
bigCBN_case_inr [in PCF.CBN]
bigCBN_case_inl [in PCF.CBN]
bigCBN_snd [in PCF.CBN]
bigCBN_fst [in PCF.CBN]
bigCBN_app [in PCF.CBN]
bigCBN_value [in PCF.CBN]
bigCBV_minus [in PCF.CBV]
bigCBV_mul [in PCF.CBV]
bigCBV_leq [in PCF.CBV]
bigCBV_ite_false [in PCF.CBV]
bigCBV_ite_true [in PCF.CBV]
bigCBV_fix [in PCF.CBV]
bigCBV_case_inr [in PCF.CBV]
bigCBV_case_inl [in PCF.CBV]
bigCBV_snd [in PCF.CBV]
bigCBV_fst [in PCF.CBV]
bigCBV_pair [in PCF.CBV]
bigCBV_app [in PCF.CBV]
bigCBV_value [in PCF.CBV]
F
f_deriv_minus [in PCF.PCF]f_deriv_mul [in PCF.PCF]
f_deriv_leq [in PCF.PCF]
f_deriv_eq [in PCF.PCF]
f_deriv_fix [in PCF.PCF]
f_deriv_inr [in PCF.PCF]
f_deriv_inl [in PCF.PCF]
f_deriv_case [in PCF.PCF]
f_deriv_snd [in PCF.PCF]
f_deriv_fst [in PCF.PCF]
f_deriv_pair [in PCF.PCF]
f_deriv_nat [in PCF.PCF]
f_deriv_star [in PCF.PCF]
f_deriv_app [in PCF.PCF]
f_deriv_abs [in PCF.PCF]
f_deriv_var [in PCF.PCF]
f_minus [in PCF.PCF]
f_mul [in PCF.PCF]
f_leq [in PCF.PCF]
f_eq [in PCF.PCF]
f_fix [in PCF.PCF]
f_inr [in PCF.PCF]
f_inl [in PCF.PCF]
f_case [in PCF.PCF]
f_snd [in PCF.PCF]
f_fst [in PCF.PCF]
f_pair [in PCF.PCF]
f_nat [in PCF.PCF]
f_star [in PCF.PCF]
f_app [in PCF.PCF]
f_abs [in PCF.PCF]
f_var [in PCF.PCF]
T
ty_sum [in PCF.PCF]ty_prod [in PCF.PCF]
ty_nat [in PCF.PCF]
ty_unit [in PCF.PCF]
ty_func [in PCF.PCF]
V
v_inr [in PCF.CBV]v_inl [in PCF.CBV]
v_pair [in PCF.CBV]
v_nat [in PCF.CBV]
v_star [in PCF.CBV]
v_abs [in PCF.CBV]
v_inr [in PCF.CBN]
v_inl [in PCF.CBN]
v_pair [in PCF.CBN]
v_nat [in PCF.CBN]
v_star [in PCF.CBN]
v_abs [in PCF.CBN]
Inductive Index
B
bigCBN [in PCF.CBN]bigCBV [in PCF.CBV]
F
form [in PCF.PCF]f_deriv [in PCF.PCF]
T
type [in PCF.PCF]V
value [in PCF.CBV]value [in PCF.CBN]
Definition Index
C
cempty [in PCF.PCF]clift [in PCF.PCF]
context [in PCF.PCF]
cupdate [in PCF.PCF]
D
deriv_ex_2 [in PCF.PCF]F
fac [in PCF.CBV]f_deriv_ex_1 [in PCF.PCF]
f_ite [in PCF.PCF]
f_bool [in PCF.PCF]
I
is_term [in PCF.PCF]is_closed [in PCF.PCF]
L
lift [in PCF.PCF]lift_k_0 [in PCF.PCF]
M
MaybeMonad.f_do [in PCF.PCF]MaybeMonad.f_return [in PCF.PCF]
MaybeMonad.M [in PCF.PCF]
O
occ [in PCF.PCF]occ_list [in PCF.PCF]
occ' [in PCF.PCF]
P
pcf_fac [in PCF.CBV]S
subst [in PCF.PCF]T
ty_bool [in PCF.PCF]| 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 | (466 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 | (328 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 | (1 entry) |
| File 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 | (31 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 | (74 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 | (7 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 | (22 entries) |
This page has been generated by coqdoc