| 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 | (524 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 | (368 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 | (3 entries) |
| 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 | (7 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 | (86 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:117 [binder, in PCF.Terms]A:12 [binder, in PCF.Terms]
A:20 [binder, in PCF.Terms]
A:25 [binder, in PCF.Terms]
A:29 [binder, in PCF.Terms]
A:33 [binder, in PCF.Terms]
A:35 [binder, in PCF.CBN]
A:39 [binder, in PCF.CBV]
A:4 [binder, in PCF.Terms]
A:40 [binder, in PCF.Terms]
A:44 [binder, in PCF.Terms]
A:47 [binder, in PCF.Terms]
A:50 [binder, in PCF.Terms]
A:7 [binder, in PCF.Terms]
A:72 [binder, in PCF.Terms]
A:94 [binder, in PCF.Terms]
A:97 [binder, in PCF.Terms]
B
bigCBN [inductive, in PCF.CBN]bigCBN_bool [lemma, in PCF.CBN]
bigCBN_reduces_to_value [lemma, in PCF.CBN]
bigCBN_div [constructor, in PCF.CBN]
bigCBN_mul [constructor, in PCF.CBN]
bigCBN_sub [constructor, in PCF.CBN]
bigCBN_add [constructor, in PCF.CBN]
bigCBN_lt [constructor, in PCF.CBN]
bigCBN_le [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_div [constructor, in PCF.CBV]
bigCBV_mul [constructor, in PCF.CBV]
bigCBV_sub [constructor, in PCF.CBV]
bigCBV_add [constructor, in PCF.CBV]
bigCBV_lt [constructor, in PCF.CBV]
bigCBV_le [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:107 [binder, in PCF.Terms]
B:120 [binder, in PCF.Terms]
B:13 [binder, in PCF.Terms]
B:22 [binder, in PCF.Terms]
b:24 [binder, in PCF.CBN]
B:26 [binder, in PCF.Terms]
b:27 [binder, in PCF.CBV]
b:29 [binder, in PCF.CBN]
B:30 [binder, in PCF.Terms]
b:32 [binder, in PCF.CBV]
b:32 [binder, in PCF.Terms]
B:34 [binder, in PCF.Terms]
b:37 [binder, in PCF.CBN]
B:40 [binder, in PCF.CBV]
b:41 [binder, in PCF.CBN]
B:41 [binder, in PCF.Terms]
b:42 [binder, in PCF.CBV]
B:45 [binder, in PCF.Terms]
b:46 [binder, in PCF.CBV]
b:50 [binder, in PCF.Formulas]
b:52 [binder, in PCF.Formulas]
b:56 [binder, in PCF.Formulas]
b:59 [binder, in PCF.Formulas]
b:77 [binder, in PCF.CBN]
b:82 [binder, in PCF.CBV]
B:9 [binder, in PCF.Terms]
b:90 [binder, in PCF.Terms]
b:92 [binder, in PCF.Terms]
C
CBN [file]CBV [file]
cempty [definition, in PCF.Contexts]
clift [definition, in PCF.Contexts]
clift_cupdate [lemma, in PCF.Contexts]
context [definition, in PCF.Contexts]
Contexts [file]
cupdate [definition, in PCF.Contexts]
cupdate_clift_free [lemma, in PCF.Contexts]
cupdate_clift_bound [lemma, in PCF.Contexts]
c1:73 [binder, in PCF.Terms]
c2:76 [binder, in PCF.Terms]
c:1 [binder, in PCF.Contexts]
c:10 [binder, in PCF.Terms]
c:11 [binder, in PCF.Contexts]
c:115 [binder, in PCF.Terms]
c:118 [binder, in PCF.Terms]
C:122 [binder, in PCF.Terms]
c:15 [binder, in PCF.Terms]
c:16 [binder, in PCF.Terms]
c:16 [binder, in PCF.Contexts]
c:18 [binder, in PCF.Terms]
c:19 [binder, in PCF.Contexts]
c:23 [binder, in PCF.Terms]
c:27 [binder, in PCF.Terms]
c:31 [binder, in PCF.Terms]
C:36 [binder, in PCF.Terms]
c:38 [binder, in PCF.Terms]
c:42 [binder, in PCF.Terms]
c:46 [binder, in PCF.Terms]
c:48 [binder, in PCF.Terms]
c:5 [binder, in PCF.Terms]
c:52 [binder, in PCF.Terms]
c:55 [binder, in PCF.Terms]
c:58 [binder, in PCF.Terms]
c:6 [binder, in PCF.Terms]
c:61 [binder, in PCF.Terms]
c:64 [binder, in PCF.Terms]
c:67 [binder, in PCF.Terms]
c:7 [binder, in PCF.Contexts]
c:71 [binder, in PCF.Terms]
c:79 [binder, in PCF.Terms]
c:84 [binder, in PCF.Terms]
c:89 [binder, in PCF.Terms]
c:91 [binder, in PCF.Terms]
c:96 [binder, in PCF.Terms]
c:99 [binder, in PCF.Terms]
D
deriv_ex_2 [definition, in PCF.Terms]F
Faculty [module, in PCF.CBV]Faculty [module, in PCF.Terms]
Faculty.fac [definition, in PCF.Terms]
Faculty.pcf_fac_reduces_to_fac [lemma, in PCF.CBV]
Faculty.pcf_fac_type [lemma, in PCF.Terms]
Faculty.pcf_fac [definition, in PCF.Terms]
fixer:110 [binder, in PCF.Terms]
form [inductive, in PCF.Formulas]
Formulas [file]
f_deriv_ex_1 [definition, in PCF.Terms]
f_deriv_ite [lemma, in PCF.Terms]
f_deriv_bool [lemma, in PCF.Terms]
f_deriv_lift [lemma, in PCF.Terms]
f_deriv_cupdate [lemma, in PCF.Terms]
f_deriv_weakening [lemma, in PCF.Terms]
f_deriv_div [constructor, in PCF.Terms]
f_deriv_mul [constructor, in PCF.Terms]
f_deriv_sub [constructor, in PCF.Terms]
f_deriv_add [constructor, in PCF.Terms]
f_deriv_lt [constructor, in PCF.Terms]
f_deriv_le [constructor, in PCF.Terms]
f_deriv_eq [constructor, in PCF.Terms]
f_deriv_fix [constructor, in PCF.Terms]
f_deriv_inr [constructor, in PCF.Terms]
f_deriv_inl [constructor, in PCF.Terms]
f_deriv_case [constructor, in PCF.Terms]
f_deriv_snd [constructor, in PCF.Terms]
f_deriv_fst [constructor, in PCF.Terms]
f_deriv_pair [constructor, in PCF.Terms]
f_deriv_nat [constructor, in PCF.Terms]
f_deriv_star [constructor, in PCF.Terms]
f_deriv_app [constructor, in PCF.Terms]
f_deriv_abs [constructor, in PCF.Terms]
f_deriv_var [constructor, in PCF.Terms]
f_deriv [inductive, in PCF.Terms]
f_ite [definition, in PCF.Formulas]
f_bool [definition, in PCF.Formulas]
f_div [constructor, in PCF.Formulas]
f_mul [constructor, in PCF.Formulas]
f_sub [constructor, in PCF.Formulas]
f_add [constructor, in PCF.Formulas]
f_lt [constructor, in PCF.Formulas]
f_le [constructor, in PCF.Formulas]
f_eq [constructor, in PCF.Formulas]
f_fix [constructor, in PCF.Formulas]
f_inr [constructor, in PCF.Formulas]
f_inl [constructor, in PCF.Formulas]
f_case [constructor, in PCF.Formulas]
f_snd [constructor, in PCF.Formulas]
f_fst [constructor, in PCF.Formulas]
f_pair [constructor, in PCF.Formulas]
f_nat [constructor, in PCF.Formulas]
f_star [constructor, in PCF.Formulas]
f_app [constructor, in PCF.Formulas]
f_abs [constructor, in PCF.Formulas]
f_var [constructor, in PCF.Formulas]
f1:100 [binder, in PCF.Terms]
f1:60 [binder, in PCF.Formulas]
f1:63 [binder, in PCF.Formulas]
f1:73 [binder, in PCF.Formulas]
f1:82 [binder, in PCF.Formulas]
f2:101 [binder, in PCF.Terms]
f2:61 [binder, in PCF.Formulas]
f2:64 [binder, in PCF.Formulas]
f2:74 [binder, in PCF.Formulas]
f2:83 [binder, in PCF.Formulas]
f3:62 [binder, in PCF.Formulas]
f3:65 [binder, in PCF.Formulas]
f3:75 [binder, in PCF.Formulas]
f3:84 [binder, in PCF.Formulas]
f:102 [binder, in PCF.Terms]
f:11 [binder, in PCF.Formulas]
f:15 [binder, in PCF.Formulas]
f:17 [binder, in PCF.Formulas]
f:19 [binder, in PCF.Formulas]
f:25 [binder, in PCF.Formulas]
f:27 [binder, in PCF.Formulas]
f:3 [binder, in PCF.Formulas]
f:31 [binder, in PCF.Formulas]
f:34 [binder, in PCF.CBN]
f:35 [binder, in PCF.Formulas]
f:37 [binder, in PCF.CBV]
f:38 [binder, in PCF.Formulas]
f:41 [binder, in PCF.Formulas]
f:45 [binder, in PCF.Formulas]
f:67 [binder, in PCF.Formulas]
f:70 [binder, in PCF.Terms]
f:74 [binder, in PCF.Terms]
f:76 [binder, in PCF.Formulas]
f:80 [binder, in PCF.Terms]
f:85 [binder, in PCF.Terms]
f:9 [binder, in PCF.Formulas]
f:98 [binder, in PCF.Terms]
G
g:109 [binder, in PCF.Terms]g:38 [binder, in PCF.CBV]
I
is_term [definition, in PCF.Terms]is_closed [definition, in PCF.Formulas]
i1:29 [binder, in PCF.Formulas]
i2:30 [binder, in PCF.Formulas]
i:10 [binder, in PCF.Contexts]
i:15 [binder, in PCF.Contexts]
i:21 [binder, in PCF.Contexts]
i:21 [binder, in PCF.Formulas]
i:34 [binder, in PCF.Formulas]
i:43 [binder, in PCF.Formulas]
i:55 [binder, in PCF.Formulas]
i:6 [binder, in PCF.Contexts]
i:70 [binder, in PCF.Formulas]
i:72 [binder, in PCF.Formulas]
i:88 [binder, in PCF.Terms]
K
k1:32 [binder, in PCF.Formulas]k1:68 [binder, in PCF.Formulas]
k2:33 [binder, in PCF.Formulas]
k2:69 [binder, in PCF.Formulas]
k:14 [binder, in PCF.Contexts]
k:20 [binder, in PCF.Contexts]
k:20 [binder, in PCF.Formulas]
k:26 [binder, in PCF.Formulas]
k:28 [binder, in PCF.Formulas]
k:36 [binder, in PCF.Formulas]
k:39 [binder, in PCF.Formulas]
k:42 [binder, in PCF.Formulas]
k:5 [binder, in PCF.Contexts]
k:54 [binder, in PCF.Formulas]
k:71 [binder, in PCF.Formulas]
k:77 [binder, in PCF.Formulas]
k:87 [binder, in PCF.Terms]
k:9 [binder, in PCF.Contexts]
L
lift [definition, in PCF.Formulas]lift_f_ite [lemma, in PCF.Formulas]
lift_f_ite_helper [lemma, in PCF.Formulas]
lift_f_bool [lemma, in PCF.Formulas]
lift_comp [lemma, in PCF.Formulas]
lift_additive [lemma, in PCF.Formulas]
lift_k_0 [definition, in PCF.Formulas]
M
MaybeMonad [module, in PCF.Terms]MaybeMonad.bind [lemma, in PCF.Terms]
MaybeMonad.f_do [definition, in PCF.Terms]
MaybeMonad.f_return [definition, in PCF.Terms]
MaybeMonad.M [definition, in PCF.Terms]
MaybeMonad.ret [lemma, in PCF.Terms]
m:108 [binder, in PCF.Terms]
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:62 [binder, in PCF.CBN]
m:67 [binder, in PCF.CBV]
m:67 [binder, in PCF.CBN]
m:72 [binder, in PCF.CBV]
m:72 [binder, in PCF.CBN]
m:77 [binder, in PCF.CBV]
N
negative_occ_lift [lemma, in PCF.Formulas]n':80 [binder, in PCF.Formulas]
n':81 [binder, in PCF.Formulas]
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]
n1:60 [binder, in PCF.CBN]
n1:65 [binder, in PCF.CBV]
n1:65 [binder, in PCF.CBN]
n1:70 [binder, in PCF.CBV]
n1:70 [binder, in PCF.CBN]
n1:75 [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]
n2:61 [binder, in PCF.CBN]
n2:66 [binder, in PCF.CBV]
n2:66 [binder, in PCF.CBN]
n2:71 [binder, in PCF.CBV]
n2:71 [binder, in PCF.CBN]
n2:76 [binder, in PCF.CBV]
n:104 [binder, in PCF.Terms]
n:17 [binder, in PCF.Terms]
n:4 [binder, in PCF.CBV]
n:4 [binder, in PCF.CBN]
n:4 [binder, in PCF.Contexts]
n:83 [binder, in PCF.CBV]
O
occ [definition, in PCF.Formulas]occ_f_ite [lemma, in PCF.Formulas]
occ_f_bool [lemma, in PCF.Formulas]
occ_lift_reverse_k_1 [lemma, in PCF.Formulas]
occ_lift_k_1 [lemma, in PCF.Formulas]
occ_occ' [lemma, in PCF.Formulas]
occ_list [definition, in PCF.Formulas]
occ' [definition, in PCF.Formulas]
occ'_occ [lemma, in PCF.Formulas]
P
p':13 [binder, in PCF.CBV]p':13 [binder, in PCF.CBN]
p:113 [binder, in PCF.Terms]
p:119 [binder, in PCF.Terms]
p:12 [binder, in PCF.CBV]
p:12 [binder, in PCF.CBN]
p:17 [binder, in PCF.CBV]
p:17 [binder, in PCF.CBN]
p:21 [binder, in PCF.CBV]
p:21 [binder, in PCF.CBN]
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:35 [binder, in PCF.Terms]
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:63 [binder, in PCF.CBV]
p:63 [binder, in PCF.CBN]
p:68 [binder, in PCF.CBV]
p:68 [binder, in PCF.CBN]
p:73 [binder, in PCF.CBV]
p:73 [binder, in PCF.CBN]
p:75 [binder, in PCF.CBN]
p:78 [binder, in PCF.CBV]
p:80 [binder, in PCF.CBV]
Q
q':15 [binder, in PCF.CBV]q:114 [binder, in PCF.Terms]
q:121 [binder, in PCF.Terms]
q:14 [binder, in PCF.CBV]
q:14 [binder, in PCF.CBN]
q:18 [binder, in PCF.CBN]
q:19 [binder, in PCF.CBV]
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:37 [binder, in PCF.Terms]
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]
q:64 [binder, in PCF.CBN]
q:69 [binder, in PCF.CBV]
q:69 [binder, in PCF.CBN]
q:74 [binder, in PCF.CBV]
q:74 [binder, in PCF.CBN]
q:79 [binder, in PCF.CBV]
R
Requirements [file]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.Formulas]subst_f_ite [lemma, in PCF.Formulas]
subst_f_ite_helper [lemma, in PCF.Formulas]
subst_f_bool [lemma, in PCF.Formulas]
s:11 [binder, in PCF.Terms]
s:21 [binder, in PCF.Terms]
s:47 [binder, in PCF.Formulas]
s:49 [binder, in PCF.Terms]
s:54 [binder, in PCF.Terms]
s:57 [binder, in PCF.Terms]
s:58 [binder, in PCF.Formulas]
s:6 [binder, in PCF.CBV]
s:6 [binder, in PCF.CBN]
s:60 [binder, in PCF.Terms]
s:63 [binder, in PCF.Terms]
s:66 [binder, in PCF.Terms]
s:69 [binder, in PCF.Terms]
s:79 [binder, in PCF.Formulas]
s:86 [binder, in PCF.Formulas]
s:93 [binder, in PCF.Terms]
T
Terms [file]type [inductive, in PCF.Types]
Types [file]
ty_bool [definition, in PCF.Types]
ty_sum [constructor, in PCF.Types]
ty_prod [constructor, in PCF.Types]
ty_nat [constructor, in PCF.Types]
ty_unit [constructor, in PCF.Types]
ty_func [constructor, in PCF.Types]
ty:103 [binder, in PCF.Terms]
ty:111 [binder, in PCF.Terms]
ty:112 [binder, in PCF.Terms]
ty:3 [binder, in PCF.Contexts]
T1:75 [binder, in PCF.Terms]
T1:78 [binder, in PCF.Terms]
T1:81 [binder, in PCF.Terms]
T2:83 [binder, in PCF.Terms]
t:116 [binder, in PCF.Terms]
T:12 [binder, in PCF.Contexts]
t:14 [binder, in PCF.Terms]
t:16 [binder, in PCF.CBN]
T:17 [binder, in PCF.Contexts]
t:19 [binder, in PCF.Terms]
t:20 [binder, in PCF.CBN]
T:22 [binder, in PCF.Contexts]
t:22 [binder, in PCF.Formulas]
t:24 [binder, in PCF.Terms]
t:28 [binder, in PCF.Terms]
t:3 [binder, in PCF.CBV]
t:3 [binder, in PCF.CBN]
t:39 [binder, in PCF.Terms]
t:43 [binder, in PCF.Terms]
t:5 [binder, in PCF.CBV]
t:5 [binder, in PCF.CBN]
t:51 [binder, in PCF.Terms]
t:53 [binder, in PCF.Terms]
t:56 [binder, in PCF.Terms]
t:59 [binder, in PCF.Terms]
t:62 [binder, in PCF.Terms]
t:65 [binder, in PCF.Terms]
t:68 [binder, in PCF.Terms]
t:7 [binder, in PCF.CBV]
t:7 [binder, in PCF.CBN]
t:8 [binder, in PCF.CBV]
t:8 [binder, in PCF.CBN]
t:8 [binder, in PCF.Terms]
T:86 [binder, in PCF.Terms]
t:95 [binder, in PCF.Terms]
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:76 [binder, in PCF.CBN]
v:81 [binder, in PCF.CBV]
v:82 [binder, in PCF.Terms]
X
x:10 [binder, in PCF.Formulas]x:12 [binder, in PCF.Formulas]
x:13 [binder, in PCF.Contexts]
x:16 [binder, in PCF.Formulas]
x:18 [binder, in PCF.Contexts]
x:18 [binder, in PCF.Formulas]
x:2 [binder, in PCF.Contexts]
x:23 [binder, in PCF.Contexts]
x:3 [binder, in PCF.Terms]
x:37 [binder, in PCF.Formulas]
x:40 [binder, in PCF.Formulas]
x:44 [binder, in PCF.Formulas]
x:46 [binder, in PCF.Formulas]
x:53 [binder, in PCF.Formulas]
x:57 [binder, in PCF.Formulas]
x:6 [binder, in PCF.Formulas]
x:66 [binder, in PCF.Formulas]
x:7 [binder, in PCF.Formulas]
x:77 [binder, in PCF.Terms]
x:78 [binder, in PCF.Formulas]
x:8 [binder, in PCF.Contexts]
x:8 [binder, in PCF.Formulas]
x:85 [binder, in PCF.Formulas]
Binder Index
A
A:117 [in PCF.Terms]A:12 [in PCF.Terms]
A:20 [in PCF.Terms]
A:25 [in PCF.Terms]
A:29 [in PCF.Terms]
A:33 [in PCF.Terms]
A:35 [in PCF.CBN]
A:39 [in PCF.CBV]
A:4 [in PCF.Terms]
A:40 [in PCF.Terms]
A:44 [in PCF.Terms]
A:47 [in PCF.Terms]
A:50 [in PCF.Terms]
A:7 [in PCF.Terms]
A:72 [in PCF.Terms]
A:94 [in PCF.Terms]
A:97 [in PCF.Terms]
B
b':25 [in PCF.CBN]b':28 [in PCF.CBV]
b':30 [in PCF.CBN]
b':33 [in PCF.CBV]
b:107 [in PCF.Terms]
B:120 [in PCF.Terms]
B:13 [in PCF.Terms]
B:22 [in PCF.Terms]
b:24 [in PCF.CBN]
B:26 [in PCF.Terms]
b:27 [in PCF.CBV]
b:29 [in PCF.CBN]
B:30 [in PCF.Terms]
b:32 [in PCF.CBV]
b:32 [in PCF.Terms]
B:34 [in PCF.Terms]
b:37 [in PCF.CBN]
B:40 [in PCF.CBV]
b:41 [in PCF.CBN]
B:41 [in PCF.Terms]
b:42 [in PCF.CBV]
B:45 [in PCF.Terms]
b:46 [in PCF.CBV]
b:50 [in PCF.Formulas]
b:52 [in PCF.Formulas]
b:56 [in PCF.Formulas]
b:59 [in PCF.Formulas]
b:77 [in PCF.CBN]
b:82 [in PCF.CBV]
B:9 [in PCF.Terms]
b:90 [in PCF.Terms]
b:92 [in PCF.Terms]
C
c1:73 [in PCF.Terms]c2:76 [in PCF.Terms]
c:1 [in PCF.Contexts]
c:10 [in PCF.Terms]
c:11 [in PCF.Contexts]
c:115 [in PCF.Terms]
c:118 [in PCF.Terms]
C:122 [in PCF.Terms]
c:15 [in PCF.Terms]
c:16 [in PCF.Terms]
c:16 [in PCF.Contexts]
c:18 [in PCF.Terms]
c:19 [in PCF.Contexts]
c:23 [in PCF.Terms]
c:27 [in PCF.Terms]
c:31 [in PCF.Terms]
C:36 [in PCF.Terms]
c:38 [in PCF.Terms]
c:42 [in PCF.Terms]
c:46 [in PCF.Terms]
c:48 [in PCF.Terms]
c:5 [in PCF.Terms]
c:52 [in PCF.Terms]
c:55 [in PCF.Terms]
c:58 [in PCF.Terms]
c:6 [in PCF.Terms]
c:61 [in PCF.Terms]
c:64 [in PCF.Terms]
c:67 [in PCF.Terms]
c:7 [in PCF.Contexts]
c:71 [in PCF.Terms]
c:79 [in PCF.Terms]
c:84 [in PCF.Terms]
c:89 [in PCF.Terms]
c:91 [in PCF.Terms]
c:96 [in PCF.Terms]
c:99 [in PCF.Terms]
F
fixer:110 [in PCF.Terms]f1:100 [in PCF.Terms]
f1:60 [in PCF.Formulas]
f1:63 [in PCF.Formulas]
f1:73 [in PCF.Formulas]
f1:82 [in PCF.Formulas]
f2:101 [in PCF.Terms]
f2:61 [in PCF.Formulas]
f2:64 [in PCF.Formulas]
f2:74 [in PCF.Formulas]
f2:83 [in PCF.Formulas]
f3:62 [in PCF.Formulas]
f3:65 [in PCF.Formulas]
f3:75 [in PCF.Formulas]
f3:84 [in PCF.Formulas]
f:102 [in PCF.Terms]
f:11 [in PCF.Formulas]
f:15 [in PCF.Formulas]
f:17 [in PCF.Formulas]
f:19 [in PCF.Formulas]
f:25 [in PCF.Formulas]
f:27 [in PCF.Formulas]
f:3 [in PCF.Formulas]
f:31 [in PCF.Formulas]
f:34 [in PCF.CBN]
f:35 [in PCF.Formulas]
f:37 [in PCF.CBV]
f:38 [in PCF.Formulas]
f:41 [in PCF.Formulas]
f:45 [in PCF.Formulas]
f:67 [in PCF.Formulas]
f:70 [in PCF.Terms]
f:74 [in PCF.Terms]
f:76 [in PCF.Formulas]
f:80 [in PCF.Terms]
f:85 [in PCF.Terms]
f:9 [in PCF.Formulas]
f:98 [in PCF.Terms]
G
g:109 [in PCF.Terms]g:38 [in PCF.CBV]
I
i1:29 [in PCF.Formulas]i2:30 [in PCF.Formulas]
i:10 [in PCF.Contexts]
i:15 [in PCF.Contexts]
i:21 [in PCF.Contexts]
i:21 [in PCF.Formulas]
i:34 [in PCF.Formulas]
i:43 [in PCF.Formulas]
i:55 [in PCF.Formulas]
i:6 [in PCF.Contexts]
i:70 [in PCF.Formulas]
i:72 [in PCF.Formulas]
i:88 [in PCF.Terms]
K
k1:32 [in PCF.Formulas]k1:68 [in PCF.Formulas]
k2:33 [in PCF.Formulas]
k2:69 [in PCF.Formulas]
k:14 [in PCF.Contexts]
k:20 [in PCF.Contexts]
k:20 [in PCF.Formulas]
k:26 [in PCF.Formulas]
k:28 [in PCF.Formulas]
k:36 [in PCF.Formulas]
k:39 [in PCF.Formulas]
k:42 [in PCF.Formulas]
k:5 [in PCF.Contexts]
k:54 [in PCF.Formulas]
k:71 [in PCF.Formulas]
k:77 [in PCF.Formulas]
k:87 [in PCF.Terms]
k:9 [in PCF.Contexts]
M
m:108 [in PCF.Terms]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:62 [in PCF.CBN]
m:67 [in PCF.CBV]
m:67 [in PCF.CBN]
m:72 [in PCF.CBV]
m:72 [in PCF.CBN]
m:77 [in PCF.CBV]
N
n':80 [in PCF.Formulas]n':81 [in PCF.Formulas]
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]
n1:60 [in PCF.CBN]
n1:65 [in PCF.CBV]
n1:65 [in PCF.CBN]
n1:70 [in PCF.CBV]
n1:70 [in PCF.CBN]
n1:75 [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]
n2:61 [in PCF.CBN]
n2:66 [in PCF.CBV]
n2:66 [in PCF.CBN]
n2:71 [in PCF.CBV]
n2:71 [in PCF.CBN]
n2:76 [in PCF.CBV]
n:104 [in PCF.Terms]
n:17 [in PCF.Terms]
n:4 [in PCF.CBV]
n:4 [in PCF.CBN]
n:4 [in PCF.Contexts]
n:83 [in PCF.CBV]
P
p':13 [in PCF.CBV]p':13 [in PCF.CBN]
p:113 [in PCF.Terms]
p:119 [in PCF.Terms]
p:12 [in PCF.CBV]
p:12 [in PCF.CBN]
p:17 [in PCF.CBV]
p:17 [in PCF.CBN]
p:21 [in PCF.CBV]
p:21 [in PCF.CBN]
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:35 [in PCF.Terms]
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:63 [in PCF.CBV]
p:63 [in PCF.CBN]
p:68 [in PCF.CBV]
p:68 [in PCF.CBN]
p:73 [in PCF.CBV]
p:73 [in PCF.CBN]
p:75 [in PCF.CBN]
p:78 [in PCF.CBV]
p:80 [in PCF.CBV]
Q
q':15 [in PCF.CBV]q:114 [in PCF.Terms]
q:121 [in PCF.Terms]
q:14 [in PCF.CBV]
q:14 [in PCF.CBN]
q:18 [in PCF.CBN]
q:19 [in PCF.CBV]
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:37 [in PCF.Terms]
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]
q:64 [in PCF.CBN]
q:69 [in PCF.CBV]
q:69 [in PCF.CBN]
q:74 [in PCF.CBV]
q:74 [in PCF.CBN]
q:79 [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:11 [in PCF.Terms]s:21 [in PCF.Terms]
s:47 [in PCF.Formulas]
s:49 [in PCF.Terms]
s:54 [in PCF.Terms]
s:57 [in PCF.Terms]
s:58 [in PCF.Formulas]
s:6 [in PCF.CBV]
s:6 [in PCF.CBN]
s:60 [in PCF.Terms]
s:63 [in PCF.Terms]
s:66 [in PCF.Terms]
s:69 [in PCF.Terms]
s:79 [in PCF.Formulas]
s:86 [in PCF.Formulas]
s:93 [in PCF.Terms]
T
ty:103 [in PCF.Terms]ty:111 [in PCF.Terms]
ty:112 [in PCF.Terms]
ty:3 [in PCF.Contexts]
T1:75 [in PCF.Terms]
T1:78 [in PCF.Terms]
T1:81 [in PCF.Terms]
T2:83 [in PCF.Terms]
t:116 [in PCF.Terms]
T:12 [in PCF.Contexts]
t:14 [in PCF.Terms]
t:16 [in PCF.CBN]
T:17 [in PCF.Contexts]
t:19 [in PCF.Terms]
t:20 [in PCF.CBN]
T:22 [in PCF.Contexts]
t:22 [in PCF.Formulas]
t:24 [in PCF.Terms]
t:28 [in PCF.Terms]
t:3 [in PCF.CBV]
t:3 [in PCF.CBN]
t:39 [in PCF.Terms]
t:43 [in PCF.Terms]
t:5 [in PCF.CBV]
t:5 [in PCF.CBN]
t:51 [in PCF.Terms]
t:53 [in PCF.Terms]
t:56 [in PCF.Terms]
t:59 [in PCF.Terms]
t:62 [in PCF.Terms]
t:65 [in PCF.Terms]
t:68 [in PCF.Terms]
t:7 [in PCF.CBV]
t:7 [in PCF.CBN]
t:8 [in PCF.CBV]
t:8 [in PCF.CBN]
t:8 [in PCF.Terms]
T:86 [in PCF.Terms]
t:95 [in PCF.Terms]
V
v:11 [in PCF.CBV]v:11 [in PCF.CBN]
v:76 [in PCF.CBN]
v:81 [in PCF.CBV]
v:82 [in PCF.Terms]
X
x:10 [in PCF.Formulas]x:12 [in PCF.Formulas]
x:13 [in PCF.Contexts]
x:16 [in PCF.Formulas]
x:18 [in PCF.Contexts]
x:18 [in PCF.Formulas]
x:2 [in PCF.Contexts]
x:23 [in PCF.Contexts]
x:3 [in PCF.Terms]
x:37 [in PCF.Formulas]
x:40 [in PCF.Formulas]
x:44 [in PCF.Formulas]
x:46 [in PCF.Formulas]
x:53 [in PCF.Formulas]
x:57 [in PCF.Formulas]
x:6 [in PCF.Formulas]
x:66 [in PCF.Formulas]
x:7 [in PCF.Formulas]
x:77 [in PCF.Terms]
x:78 [in PCF.Formulas]
x:8 [in PCF.Contexts]
x:8 [in PCF.Formulas]
x:85 [in PCF.Formulas]
Module Index
F
Faculty [in PCF.CBV]Faculty [in PCF.Terms]
M
MaybeMonad [in PCF.Terms]File Index
C
CBNCBV
Contexts
F
FormulasR
RequirementsT
TermsTypes
Lemma 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.Contexts]cupdate_clift_free [in PCF.Contexts]
cupdate_clift_bound [in PCF.Contexts]
F
Faculty.pcf_fac_reduces_to_fac [in PCF.CBV]Faculty.pcf_fac_type [in PCF.Terms]
f_deriv_ite [in PCF.Terms]
f_deriv_bool [in PCF.Terms]
f_deriv_lift [in PCF.Terms]
f_deriv_cupdate [in PCF.Terms]
f_deriv_weakening [in PCF.Terms]
L
lift_f_ite [in PCF.Formulas]lift_f_ite_helper [in PCF.Formulas]
lift_f_bool [in PCF.Formulas]
lift_comp [in PCF.Formulas]
lift_additive [in PCF.Formulas]
M
MaybeMonad.bind [in PCF.Terms]MaybeMonad.ret [in PCF.Terms]
N
negative_occ_lift [in PCF.Formulas]O
occ_f_ite [in PCF.Formulas]occ_f_bool [in PCF.Formulas]
occ_lift_reverse_k_1 [in PCF.Formulas]
occ_lift_k_1 [in PCF.Formulas]
occ_occ' [in PCF.Formulas]
occ'_occ [in PCF.Formulas]
S
subst_f_ite [in PCF.Formulas]subst_f_ite_helper [in PCF.Formulas]
subst_f_bool [in PCF.Formulas]
Constructor Index
B
bigCBN_div [in PCF.CBN]bigCBN_mul [in PCF.CBN]
bigCBN_sub [in PCF.CBN]
bigCBN_add [in PCF.CBN]
bigCBN_lt [in PCF.CBN]
bigCBN_le [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_div [in PCF.CBV]
bigCBV_mul [in PCF.CBV]
bigCBV_sub [in PCF.CBV]
bigCBV_add [in PCF.CBV]
bigCBV_lt [in PCF.CBV]
bigCBV_le [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_div [in PCF.Terms]f_deriv_mul [in PCF.Terms]
f_deriv_sub [in PCF.Terms]
f_deriv_add [in PCF.Terms]
f_deriv_lt [in PCF.Terms]
f_deriv_le [in PCF.Terms]
f_deriv_eq [in PCF.Terms]
f_deriv_fix [in PCF.Terms]
f_deriv_inr [in PCF.Terms]
f_deriv_inl [in PCF.Terms]
f_deriv_case [in PCF.Terms]
f_deriv_snd [in PCF.Terms]
f_deriv_fst [in PCF.Terms]
f_deriv_pair [in PCF.Terms]
f_deriv_nat [in PCF.Terms]
f_deriv_star [in PCF.Terms]
f_deriv_app [in PCF.Terms]
f_deriv_abs [in PCF.Terms]
f_deriv_var [in PCF.Terms]
f_div [in PCF.Formulas]
f_mul [in PCF.Formulas]
f_sub [in PCF.Formulas]
f_add [in PCF.Formulas]
f_lt [in PCF.Formulas]
f_le [in PCF.Formulas]
f_eq [in PCF.Formulas]
f_fix [in PCF.Formulas]
f_inr [in PCF.Formulas]
f_inl [in PCF.Formulas]
f_case [in PCF.Formulas]
f_snd [in PCF.Formulas]
f_fst [in PCF.Formulas]
f_pair [in PCF.Formulas]
f_nat [in PCF.Formulas]
f_star [in PCF.Formulas]
f_app [in PCF.Formulas]
f_abs [in PCF.Formulas]
f_var [in PCF.Formulas]
T
ty_sum [in PCF.Types]ty_prod [in PCF.Types]
ty_nat [in PCF.Types]
ty_unit [in PCF.Types]
ty_func [in PCF.Types]
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.Formulas]f_deriv [in PCF.Terms]
T
type [in PCF.Types]V
value [in PCF.CBV]value [in PCF.CBN]
Definition Index
C
cempty [in PCF.Contexts]clift [in PCF.Contexts]
context [in PCF.Contexts]
cupdate [in PCF.Contexts]
D
deriv_ex_2 [in PCF.Terms]F
Faculty.fac [in PCF.Terms]Faculty.pcf_fac [in PCF.Terms]
f_deriv_ex_1 [in PCF.Terms]
f_ite [in PCF.Formulas]
f_bool [in PCF.Formulas]
I
is_term [in PCF.Terms]is_closed [in PCF.Formulas]
L
lift [in PCF.Formulas]lift_k_0 [in PCF.Formulas]
M
MaybeMonad.f_do [in PCF.Terms]MaybeMonad.f_return [in PCF.Terms]
MaybeMonad.M [in PCF.Terms]
O
occ [in PCF.Formulas]occ_list [in PCF.Formulas]
occ' [in PCF.Formulas]
S
subst [in PCF.Formulas]T
ty_bool [in PCF.Types]| 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 | (524 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 | (368 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 | (3 entries) |
| 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 | (7 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 | (86 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