| 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 | (357 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 | (237 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 | (4 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 | (89 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 | (16 entries) |
Global Index
A
A:106 [binder, in PCF.PCF]A:112 [binder, in PCF.PCF]
A:32 [binder, in PCF.PCF]
A:37 [binder, in PCF.PCF]
A:42 [binder, in PCF.PCF]
A:46 [binder, in PCF.PCF]
A:48 [binder, in PCF.CBN]
A:50 [binder, in PCF.PCF]
A:52 [binder, in PCF.CBV]
A:54 [binder, in PCF.PCF]
A:58 [binder, in PCF.PCF]
A:64 [binder, in PCF.PCF]
A:69 [binder, in PCF.PCF]
A:78 [binder, in PCF.PCF]
A:83 [binder, in PCF.PCF]
A:86 [binder, in PCF.PCF]
A:97 [binder, in PCF.PCF]
B
bigCBN [inductive, in PCF.CBN]bigCBN_minus [constructor, in PCF.CBN]
bigCBN_mul [constructor, in PCF.CBN]
bigCBN_leq [constructor, in PCF.CBN]
bigCBN_fix [constructor, in PCF.CBN]
bigCBN_ite_false [constructor, in PCF.CBN]
bigCBN_ite_true [constructor, in PCF.CBN]
bigCBN_sum_case_inr [constructor, in PCF.CBN]
bigCBN_sum_case_inl [constructor, in PCF.CBN]
bigCBN_pair_snd [constructor, in PCF.CBN]
bigCBN_pair_fst [constructor, in PCF.CBN]
bigCBN_beta [constructor, in PCF.CBN]
bigCBN_abs_refl [constructor, in PCF.CBN]
bigCBN_refl_pair [constructor, in PCF.CBN]
bigCBN_refl_star [constructor, in PCF.CBN]
bigCBN_refl_bool [constructor, in PCF.CBN]
bigCBN_refl_nat [constructor, in PCF.CBN]
bigCBV [inductive, in PCF.CBV]
bigCBV_minus [constructor, in PCF.CBV]
bigCBV_mul [constructor, in PCF.CBV]
bigCBV_leq [constructor, in PCF.CBV]
bigCBV_fix [constructor, in PCF.CBV]
bigCBV_ite_false [constructor, in PCF.CBV]
bigCBV_ite_true [constructor, in PCF.CBV]
bigCBV_sum_case_inr [constructor, in PCF.CBV]
bigCBV_sum_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_beta [constructor, in PCF.CBV]
bigCBV_refl_abs [constructor, in PCF.CBV]
bigCBV_refl_pair [constructor, in PCF.CBV]
bigCBV_refl_star [constructor, in PCF.CBV]
bigCBV_refl_bool [constructor, in PCF.CBV]
bigCBV_refl_nat [constructor, in PCF.CBV]
b':30 [binder, in PCF.CBN]
b':33 [binder, in PCF.CBV]
b':35 [binder, in PCF.CBN]
b':38 [binder, in PCF.CBV]
B:115 [binder, in PCF.PCF]
b:13 [binder, in PCF.CBV]
b:13 [binder, in PCF.CBN]
b:29 [binder, in PCF.CBN]
b:3 [binder, in PCF.CBV]
b:3 [binder, in PCF.CBN]
b:32 [binder, in PCF.CBV]
b:34 [binder, in PCF.CBN]
b:37 [binder, in PCF.CBV]
B:39 [binder, in PCF.PCF]
b:39 [binder, in PCF.CBN]
b:42 [binder, in PCF.CBV]
B:43 [binder, in PCF.PCF]
b:43 [binder, in PCF.CBN]
b:46 [binder, in PCF.CBV]
B:47 [binder, in PCF.PCF]
B:51 [binder, in PCF.PCF]
B:53 [binder, in PCF.CBV]
B:55 [binder, in PCF.PCF]
b:57 [binder, in PCF.PCF]
B:59 [binder, in PCF.PCF]
B:66 [binder, in PCF.PCF]
B:70 [binder, in PCF.PCF]
b:70 [binder, in PCF.CBV]
b:75 [binder, in PCF.PCF]
b:81 [binder, in PCF.PCF]
C
CBN [file]CBV [file]
cempty [definition, in PCF.PCF]
clift [definition, in PCF.PCF]
context [definition, in PCF.PCF]
cupdate [definition, in PCF.PCF]
c:105 [binder, in PCF.PCF]
c:110 [binder, in PCF.PCF]
c:113 [binder, in PCF.PCF]
C:117 [binder, in PCF.PCF]
c:22 [binder, in PCF.PCF]
c:3 [binder, in PCF.PCF]
c:33 [binder, in PCF.PCF]
c:34 [binder, in PCF.PCF]
c:35 [binder, in PCF.PCF]
c:40 [binder, in PCF.PCF]
c:44 [binder, in PCF.PCF]
c:48 [binder, in PCF.PCF]
c:52 [binder, in PCF.PCF]
c:56 [binder, in PCF.PCF]
C:61 [binder, in PCF.PCF]
c:63 [binder, in PCF.PCF]
c:67 [binder, in PCF.PCF]
c:72 [binder, in PCF.PCF]
c:74 [binder, in PCF.PCF]
c:76 [binder, in PCF.PCF]
c:80 [binder, in PCF.PCF]
c:85 [binder, in PCF.PCF]
c:87 [binder, in PCF.PCF]
c:90 [binder, in PCF.PCF]
c:93 [binder, in PCF.PCF]
c:96 [binder, in PCF.PCF]
c:99 [binder, in PCF.PCF]
D
deriv_ex_2 [definition, in PCF.PCF]F
fac [definition, in PCF.CBV]fixer:73 [binder, in PCF.CBV]
form [inductive, in PCF.PCF]
f_deriv_ex_1 [definition, 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_fix [constructor, in PCF.PCF]
f_deriv_ite [constructor, in PCF.PCF]
f_deriv_eq [constructor, in PCF.PCF]
f_deriv_bool [constructor, in PCF.PCF]
f_deriv_nat [constructor, in PCF.PCF]
f_deriv_app [constructor, in PCF.PCF]
f_deriv_abs [constructor, in PCF.PCF]
f_deriv_case [constructor, in PCF.PCF]
f_deriv_inr [constructor, in PCF.PCF]
f_deriv_inl [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_star [constructor, in PCF.PCF]
f_deriv_var [constructor, in PCF.PCF]
f_deriv [inductive, in PCF.PCF]
f_minus [constructor, in PCF.PCF]
f_mul [constructor, in PCF.PCF]
f_leq [constructor, in PCF.PCF]
f_fix [constructor, in PCF.PCF]
f_ite [constructor, in PCF.PCF]
f_eq [constructor, in PCF.PCF]
f_app [constructor, in PCF.PCF]
f_abs [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_star [constructor, in PCF.PCF]
f_bool [constructor, in PCF.PCF]
f_nat [constructor, in PCF.PCF]
f_var [constructor, in PCF.PCF]
f1:100 [binder, in PCF.PCF]
f2:101 [binder, in PCF.PCF]
f:102 [binder, in PCF.PCF]
f:104 [binder, in PCF.PCF]
f:14 [binder, in PCF.PCF]
f:24 [binder, in PCF.PCF]
f:47 [binder, in PCF.CBN]
f:50 [binder, in PCF.CBV]
f:8 [binder, in PCF.PCF]
f:98 [binder, in PCF.PCF]
G
g:51 [binder, in PCF.CBV]g:72 [binder, in PCF.CBV]
I
is_term [definition, in PCF.PCF]is_closed [definition, in PCF.PCF]
i:16 [binder, in PCF.PCF]
i:21 [binder, in PCF.PCF]
K
k:15 [binder, in PCF.PCF]k:20 [binder, in PCF.PCF]
L
lift [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: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:71 [binder, in PCF.CBV]
N
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]
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]
n:12 [binder, in PCF.CBV]
n:12 [binder, in PCF.CBN]
n:4 [binder, in PCF.CBV]
n:4 [binder, in PCF.CBN]
n:73 [binder, in PCF.PCF]
n:75 [binder, in PCF.CBV]
n:78 [binder, in PCF.CBV]
O
occ [definition, 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':18 [binder, in PCF.CBV]
p':18 [binder, in PCF.CBN]
p:108 [binder, in PCF.PCF]
p:114 [binder, in PCF.PCF]
p:16 [binder, in PCF.CBV]
p:16 [binder, in PCF.CBN]
p:17 [binder, in PCF.CBV]
p:17 [binder, in PCF.CBN]
p:22 [binder, in PCF.CBV]
p:22 [binder, in PCF.CBN]
p:26 [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:36 [binder, in PCF.CBN]
p:39 [binder, in PCF.CBV]
p:40 [binder, in PCF.CBN]
p:43 [binder, in PCF.CBV]
p:44 [binder, in PCF.CBN]
p:47 [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.PCF]
p:63 [binder, in PCF.CBV]
p:63 [binder, in PCF.CBN]
p:68 [binder, in PCF.CBV]
Q
q':20 [binder, in PCF.CBV]q:109 [binder, in PCF.PCF]
q:116 [binder, in PCF.PCF]
q:19 [binder, in PCF.CBV]
q:19 [binder, in PCF.CBN]
q:23 [binder, in PCF.CBN]
q:24 [binder, in PCF.CBV]
q:27 [binder, in PCF.CBN]
q:33 [binder, in PCF.CBN]
q:36 [binder, in PCF.CBV]
q:38 [binder, in PCF.CBN]
q:41 [binder, in PCF.CBV]
q:42 [binder, in PCF.CBN]
q:45 [binder, in PCF.CBV]
q:46 [binder, in PCF.CBN]
q:49 [binder, in PCF.CBV]
q:54 [binder, in PCF.CBN]
q:59 [binder, in PCF.CBV]
q:59 [binder, in PCF.CBN]
q:62 [binder, in PCF.PCF]
q:64 [binder, in PCF.CBV]
q:64 [binder, in PCF.CBN]
q:69 [binder, in PCF.CBV]
R
r1:23 [binder, in PCF.CBV]r1:27 [binder, in PCF.CBV]
r1:30 [binder, in PCF.CBV]
r2:25 [binder, in PCF.CBV]
r2:28 [binder, in PCF.CBV]
r2:31 [binder, in PCF.CBV]
r:20 [binder, in PCF.CBN]
r:21 [binder, in PCF.CBV]
r:24 [binder, in PCF.CBN]
r:28 [binder, in PCF.CBN]
r:32 [binder, in PCF.CBN]
r:35 [binder, in PCF.CBV]
r:37 [binder, in PCF.CBN]
r:40 [binder, in PCF.CBV]
r:41 [binder, in PCF.CBN]
r:44 [binder, in PCF.CBV]
r:45 [binder, in PCF.CBN]
r:48 [binder, in PCF.CBV]
r:49 [binder, in PCF.CBN]
r:54 [binder, in PCF.CBV]
S
subst [definition, in PCF.PCF]s:15 [binder, in PCF.CBV]
s:15 [binder, in PCF.CBN]
s:26 [binder, in PCF.PCF]
s:38 [binder, in PCF.PCF]
s:6 [binder, in PCF.CBV]
s:6 [binder, in PCF.CBN]
s:68 [binder, in PCF.PCF]
s:77 [binder, in PCF.PCF]
s:82 [binder, in PCF.PCF]
s:89 [binder, in PCF.PCF]
s:92 [binder, in PCF.PCF]
s:95 [binder, in PCF.PCF]
T
type [inductive, in PCF.PCF]ty_func [constructor, in PCF.PCF]
ty_sum [constructor, in PCF.PCF]
ty_prod [constructor, in PCF.PCF]
ty_unit [constructor, in PCF.PCF]
ty_bool [constructor, in PCF.PCF]
ty_nat [constructor, in PCF.PCF]
ty:103 [binder, in PCF.PCF]
ty:107 [binder, in PCF.PCF]
ty:5 [binder, in PCF.PCF]
ty:74 [binder, in PCF.CBV]
t:111 [binder, in PCF.PCF]
t:14 [binder, in PCF.CBV]
t:14 [binder, in PCF.CBN]
t:17 [binder, in PCF.PCF]
t:21 [binder, in PCF.CBN]
t:25 [binder, in PCF.CBN]
t:36 [binder, in PCF.PCF]
t:41 [binder, in PCF.PCF]
t:45 [binder, in PCF.PCF]
t:49 [binder, in PCF.PCF]
t:5 [binder, in PCF.CBV]
t:5 [binder, in PCF.CBN]
t:53 [binder, in PCF.PCF]
t:65 [binder, in PCF.PCF]
t:7 [binder, in PCF.CBV]
t:7 [binder, in PCF.CBN]
t:71 [binder, in PCF.PCF]
t:79 [binder, in PCF.PCF]
t:8 [binder, in PCF.CBV]
t:8 [binder, in PCF.CBN]
t:84 [binder, in PCF.PCF]
t:88 [binder, in PCF.PCF]
t:9 [binder, in PCF.CBV]
t:9 [binder, in PCF.CBN]
t:91 [binder, in PCF.PCF]
t:94 [binder, in PCF.PCF]
V
value [inductive, in PCF.CBV]value [inductive, in PCF.CBN]
v_func [constructor, in PCF.CBV]
v_inr [constructor, in PCF.CBV]
v_inl [constructor, in PCF.CBV]
v_pair [constructor, in PCF.CBV]
v_star [constructor, in PCF.CBV]
v_nat [constructor, in PCF.CBV]
v_bool [constructor, in PCF.CBV]
v_func [constructor, in PCF.CBN]
v_inr [constructor, in PCF.CBN]
v_inl [constructor, in PCF.CBN]
v_pair [constructor, in PCF.CBN]
v_star [constructor, in PCF.CBN]
v_nat [constructor, in PCF.CBN]
v_bool [constructor, in PCF.CBN]
X
x:11 [binder, in PCF.PCF]x:12 [binder, in PCF.PCF]
x:13 [binder, in PCF.PCF]
x:23 [binder, in PCF.PCF]
x:25 [binder, in PCF.PCF]
x:31 [binder, in PCF.PCF]
x:4 [binder, in PCF.PCF]
Binder Index
A
A:106 [in PCF.PCF]A:112 [in PCF.PCF]
A:32 [in PCF.PCF]
A:37 [in PCF.PCF]
A:42 [in PCF.PCF]
A:46 [in PCF.PCF]
A:48 [in PCF.CBN]
A:50 [in PCF.PCF]
A:52 [in PCF.CBV]
A:54 [in PCF.PCF]
A:58 [in PCF.PCF]
A:64 [in PCF.PCF]
A:69 [in PCF.PCF]
A:78 [in PCF.PCF]
A:83 [in PCF.PCF]
A:86 [in PCF.PCF]
A:97 [in PCF.PCF]
B
b':30 [in PCF.CBN]b':33 [in PCF.CBV]
b':35 [in PCF.CBN]
b':38 [in PCF.CBV]
B:115 [in PCF.PCF]
b:13 [in PCF.CBV]
b:13 [in PCF.CBN]
b:29 [in PCF.CBN]
b:3 [in PCF.CBV]
b:3 [in PCF.CBN]
b:32 [in PCF.CBV]
b:34 [in PCF.CBN]
b:37 [in PCF.CBV]
B:39 [in PCF.PCF]
b:39 [in PCF.CBN]
b:42 [in PCF.CBV]
B:43 [in PCF.PCF]
b:43 [in PCF.CBN]
b:46 [in PCF.CBV]
B:47 [in PCF.PCF]
B:51 [in PCF.PCF]
B:53 [in PCF.CBV]
B:55 [in PCF.PCF]
b:57 [in PCF.PCF]
B:59 [in PCF.PCF]
B:66 [in PCF.PCF]
B:70 [in PCF.PCF]
b:70 [in PCF.CBV]
b:75 [in PCF.PCF]
b:81 [in PCF.PCF]
C
c:105 [in PCF.PCF]c:110 [in PCF.PCF]
c:113 [in PCF.PCF]
C:117 [in PCF.PCF]
c:22 [in PCF.PCF]
c:3 [in PCF.PCF]
c:33 [in PCF.PCF]
c:34 [in PCF.PCF]
c:35 [in PCF.PCF]
c:40 [in PCF.PCF]
c:44 [in PCF.PCF]
c:48 [in PCF.PCF]
c:52 [in PCF.PCF]
c:56 [in PCF.PCF]
C:61 [in PCF.PCF]
c:63 [in PCF.PCF]
c:67 [in PCF.PCF]
c:72 [in PCF.PCF]
c:74 [in PCF.PCF]
c:76 [in PCF.PCF]
c:80 [in PCF.PCF]
c:85 [in PCF.PCF]
c:87 [in PCF.PCF]
c:90 [in PCF.PCF]
c:93 [in PCF.PCF]
c:96 [in PCF.PCF]
c:99 [in PCF.PCF]
F
fixer:73 [in PCF.CBV]f1:100 [in PCF.PCF]
f2:101 [in PCF.PCF]
f:102 [in PCF.PCF]
f:104 [in PCF.PCF]
f:14 [in PCF.PCF]
f:24 [in PCF.PCF]
f:47 [in PCF.CBN]
f:50 [in PCF.CBV]
f:8 [in PCF.PCF]
f:98 [in PCF.PCF]
G
g:51 [in PCF.CBV]g:72 [in PCF.CBV]
I
i:16 [in PCF.PCF]i:21 [in PCF.PCF]
K
k:15 [in PCF.PCF]k:20 [in PCF.PCF]
M
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:71 [in PCF.CBV]
N
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]
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]
n:12 [in PCF.CBV]
n:12 [in PCF.CBN]
n:4 [in PCF.CBV]
n:4 [in PCF.CBN]
n:73 [in PCF.PCF]
n:75 [in PCF.CBV]
n:78 [in PCF.CBV]
P
p':18 [in PCF.CBV]p':18 [in PCF.CBN]
p:108 [in PCF.PCF]
p:114 [in PCF.PCF]
p:16 [in PCF.CBV]
p:16 [in PCF.CBN]
p:17 [in PCF.CBV]
p:17 [in PCF.CBN]
p:22 [in PCF.CBV]
p:22 [in PCF.CBN]
p:26 [in PCF.CBV]
p:26 [in PCF.CBN]
p:29 [in PCF.CBV]
p:31 [in PCF.CBN]
p:34 [in PCF.CBV]
p:36 [in PCF.CBN]
p:39 [in PCF.CBV]
p:40 [in PCF.CBN]
p:43 [in PCF.CBV]
p:44 [in PCF.CBN]
p:47 [in PCF.CBV]
p:53 [in PCF.CBN]
p:58 [in PCF.CBV]
p:58 [in PCF.CBN]
p:60 [in PCF.PCF]
p:63 [in PCF.CBV]
p:63 [in PCF.CBN]
p:68 [in PCF.CBV]
Q
q':20 [in PCF.CBV]q:109 [in PCF.PCF]
q:116 [in PCF.PCF]
q:19 [in PCF.CBV]
q:19 [in PCF.CBN]
q:23 [in PCF.CBN]
q:24 [in PCF.CBV]
q:27 [in PCF.CBN]
q:33 [in PCF.CBN]
q:36 [in PCF.CBV]
q:38 [in PCF.CBN]
q:41 [in PCF.CBV]
q:42 [in PCF.CBN]
q:45 [in PCF.CBV]
q:46 [in PCF.CBN]
q:49 [in PCF.CBV]
q:54 [in PCF.CBN]
q:59 [in PCF.CBV]
q:59 [in PCF.CBN]
q:62 [in PCF.PCF]
q:64 [in PCF.CBV]
q:64 [in PCF.CBN]
q:69 [in PCF.CBV]
R
r1:23 [in PCF.CBV]r1:27 [in PCF.CBV]
r1:30 [in PCF.CBV]
r2:25 [in PCF.CBV]
r2:28 [in PCF.CBV]
r2:31 [in PCF.CBV]
r:20 [in PCF.CBN]
r:21 [in PCF.CBV]
r:24 [in PCF.CBN]
r:28 [in PCF.CBN]
r:32 [in PCF.CBN]
r:35 [in PCF.CBV]
r:37 [in PCF.CBN]
r:40 [in PCF.CBV]
r:41 [in PCF.CBN]
r:44 [in PCF.CBV]
r:45 [in PCF.CBN]
r:48 [in PCF.CBV]
r:49 [in PCF.CBN]
r:54 [in PCF.CBV]
S
s:15 [in PCF.CBV]s:15 [in PCF.CBN]
s:26 [in PCF.PCF]
s:38 [in PCF.PCF]
s:6 [in PCF.CBV]
s:6 [in PCF.CBN]
s:68 [in PCF.PCF]
s:77 [in PCF.PCF]
s:82 [in PCF.PCF]
s:89 [in PCF.PCF]
s:92 [in PCF.PCF]
s:95 [in PCF.PCF]
T
ty:103 [in PCF.PCF]ty:107 [in PCF.PCF]
ty:5 [in PCF.PCF]
ty:74 [in PCF.CBV]
t:111 [in PCF.PCF]
t:14 [in PCF.CBV]
t:14 [in PCF.CBN]
t:17 [in PCF.PCF]
t:21 [in PCF.CBN]
t:25 [in PCF.CBN]
t:36 [in PCF.PCF]
t:41 [in PCF.PCF]
t:45 [in PCF.PCF]
t:49 [in PCF.PCF]
t:5 [in PCF.CBV]
t:5 [in PCF.CBN]
t:53 [in PCF.PCF]
t:65 [in PCF.PCF]
t:7 [in PCF.CBV]
t:7 [in PCF.CBN]
t:71 [in PCF.PCF]
t:79 [in PCF.PCF]
t:8 [in PCF.CBV]
t:8 [in PCF.CBN]
t:84 [in PCF.PCF]
t:88 [in PCF.PCF]
t:9 [in PCF.CBV]
t:9 [in PCF.CBN]
t:91 [in PCF.PCF]
t:94 [in PCF.PCF]
X
x:11 [in PCF.PCF]x:12 [in PCF.PCF]
x:13 [in PCF.PCF]
x:23 [in PCF.PCF]
x:25 [in PCF.PCF]
x:31 [in PCF.PCF]
x:4 [in PCF.PCF]
Module Index
M
MaybeMonad [in PCF.PCF]File Index
C
CBNCBV
P
PCFLemma Index
M
MaybeMonad.bind [in PCF.PCF]MaybeMonad.ret [in PCF.PCF]
P
pcf_fac_reduces_to_fac [in PCF.CBV]pcf_fac_type [in PCF.CBV]
Constructor Index
B
bigCBN_minus [in PCF.CBN]bigCBN_mul [in PCF.CBN]
bigCBN_leq [in PCF.CBN]
bigCBN_fix [in PCF.CBN]
bigCBN_ite_false [in PCF.CBN]
bigCBN_ite_true [in PCF.CBN]
bigCBN_sum_case_inr [in PCF.CBN]
bigCBN_sum_case_inl [in PCF.CBN]
bigCBN_pair_snd [in PCF.CBN]
bigCBN_pair_fst [in PCF.CBN]
bigCBN_beta [in PCF.CBN]
bigCBN_abs_refl [in PCF.CBN]
bigCBN_refl_pair [in PCF.CBN]
bigCBN_refl_star [in PCF.CBN]
bigCBN_refl_bool [in PCF.CBN]
bigCBN_refl_nat [in PCF.CBN]
bigCBV_minus [in PCF.CBV]
bigCBV_mul [in PCF.CBV]
bigCBV_leq [in PCF.CBV]
bigCBV_fix [in PCF.CBV]
bigCBV_ite_false [in PCF.CBV]
bigCBV_ite_true [in PCF.CBV]
bigCBV_sum_case_inr [in PCF.CBV]
bigCBV_sum_case_inl [in PCF.CBV]
bigCBV_snd [in PCF.CBV]
bigCBV_fst [in PCF.CBV]
bigCBV_pair [in PCF.CBV]
bigCBV_beta [in PCF.CBV]
bigCBV_refl_abs [in PCF.CBV]
bigCBV_refl_pair [in PCF.CBV]
bigCBV_refl_star [in PCF.CBV]
bigCBV_refl_bool [in PCF.CBV]
bigCBV_refl_nat [in PCF.CBV]
F
f_deriv_minus [in PCF.PCF]f_deriv_mul [in PCF.PCF]
f_deriv_leq [in PCF.PCF]
f_deriv_fix [in PCF.PCF]
f_deriv_ite [in PCF.PCF]
f_deriv_eq [in PCF.PCF]
f_deriv_bool [in PCF.PCF]
f_deriv_nat [in PCF.PCF]
f_deriv_app [in PCF.PCF]
f_deriv_abs [in PCF.PCF]
f_deriv_case [in PCF.PCF]
f_deriv_inr [in PCF.PCF]
f_deriv_inl [in PCF.PCF]
f_deriv_snd [in PCF.PCF]
f_deriv_fst [in PCF.PCF]
f_deriv_pair [in PCF.PCF]
f_deriv_star [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_fix [in PCF.PCF]
f_ite [in PCF.PCF]
f_eq [in PCF.PCF]
f_app [in PCF.PCF]
f_abs [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_star [in PCF.PCF]
f_bool [in PCF.PCF]
f_nat [in PCF.PCF]
f_var [in PCF.PCF]
T
ty_func [in PCF.PCF]ty_sum [in PCF.PCF]
ty_prod [in PCF.PCF]
ty_unit [in PCF.PCF]
ty_bool [in PCF.PCF]
ty_nat [in PCF.PCF]
V
v_func [in PCF.CBV]v_inr [in PCF.CBV]
v_inl [in PCF.CBV]
v_pair [in PCF.CBV]
v_star [in PCF.CBV]
v_nat [in PCF.CBV]
v_bool [in PCF.CBV]
v_func [in PCF.CBN]
v_inr [in PCF.CBN]
v_inl [in PCF.CBN]
v_pair [in PCF.CBN]
v_star [in PCF.CBN]
v_nat [in PCF.CBN]
v_bool [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]
I
is_term [in PCF.PCF]is_closed [in PCF.PCF]
L
lift [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]P
pcf_fac [in PCF.CBV]S
subst [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 | (357 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 | (237 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 | (4 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 | (89 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 | (16 entries) |
This page has been generated by coqdoc