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 | (347 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 | (233 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 | (6 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 | (81 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:44 [binder, in PCF.CBN]
A:46 [binder, in PCF.PCF]
A:48 [binder, in PCF.CBV]
A:50 [binder, in PCF.PCF]
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_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_fix [constructor, in PCF.CBN]
bigCBN_ite_false [constructor, in PCF.CBN]
bigCBN_ite_true [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_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_fix [constructor, in PCF.CBV]
bigCBV_ite_false [constructor, in PCF.CBV]
bigCBV_ite_true [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':26 [binder, in PCF.CBN]
b':29 [binder, in PCF.CBV]
b':31 [binder, in PCF.CBN]
b':34 [binder, in PCF.CBV]
B:115 [binder, in PCF.PCF]
b:25 [binder, in PCF.CBN]
b:28 [binder, in PCF.CBV]
b:3 [binder, in PCF.CBV]
b:3 [binder, in PCF.CBN]
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:39 [binder, in PCF.PCF]
b:39 [binder, in PCF.CBN]
b:42 [binder, in PCF.CBV]
B:43 [binder, in PCF.PCF]
B:47 [binder, in PCF.PCF]
B:49 [binder, in PCF.CBV]
B:51 [binder, in PCF.PCF]
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:68 [binder, in PCF.CBV]
B:70 [binder, in PCF.PCF]
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:71 [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:43 [binder, in PCF.CBN]
f:46 [binder, in PCF.CBV]
f:8 [binder, in PCF.PCF]
f:98 [binder, in PCF.PCF]
G
g:47 [binder, in PCF.CBV]g:70 [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:48 [binder, in PCF.CBN]
m:53 [binder, in PCF.CBV]
m:53 [binder, in PCF.CBN]
m:58 [binder, in PCF.CBV]
m:58 [binder, in PCF.CBN]
m:63 [binder, in PCF.CBV]
m:69 [binder, in PCF.CBV]
N
n1:46 [binder, in PCF.CBN]n1:51 [binder, in PCF.CBV]
n1:51 [binder, in PCF.CBN]
n1:56 [binder, in PCF.CBV]
n1:56 [binder, in PCF.CBN]
n1:61 [binder, in PCF.CBV]
n2:47 [binder, in PCF.CBN]
n2:52 [binder, in PCF.CBV]
n2:52 [binder, in PCF.CBN]
n2:57 [binder, in PCF.CBV]
n2:57 [binder, in PCF.CBN]
n2:62 [binder, in PCF.CBV]
n:4 [binder, in PCF.CBV]
n:4 [binder, in PCF.CBN]
n:73 [binder, in PCF.PCF]
n:73 [binder, in PCF.CBV]
n:76 [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':14 [binder, in PCF.CBV]
p':14 [binder, in PCF.CBN]
p:108 [binder, in PCF.PCF]
p:114 [binder, in PCF.PCF]
p:13 [binder, in PCF.CBV]
p:13 [binder, in PCF.CBN]
p:18 [binder, in PCF.CBV]
p:18 [binder, in PCF.CBN]
p:22 [binder, in PCF.CBV]
p:22 [binder, in PCF.CBN]
p:25 [binder, in PCF.CBV]
p:27 [binder, in PCF.CBN]
p:30 [binder, in PCF.CBV]
p:32 [binder, in PCF.CBN]
p:35 [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:49 [binder, in PCF.CBN]
p:54 [binder, in PCF.CBV]
p:54 [binder, in PCF.CBN]
p:59 [binder, in PCF.CBV]
p:59 [binder, in PCF.CBN]
p:60 [binder, in PCF.PCF]
p:61 [binder, in PCF.CBN]
p:64 [binder, in PCF.CBV]
p:66 [binder, in PCF.CBV]
Q
q':16 [binder, in PCF.CBV]q:109 [binder, in PCF.PCF]
q:116 [binder, in PCF.PCF]
q:15 [binder, in PCF.CBV]
q:15 [binder, in PCF.CBN]
q:19 [binder, in PCF.CBN]
q:20 [binder, in PCF.CBV]
q:23 [binder, in PCF.CBN]
q:29 [binder, in PCF.CBN]
q:32 [binder, in PCF.CBV]
q:34 [binder, in PCF.CBN]
q:37 [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:50 [binder, in PCF.CBN]
q:55 [binder, in PCF.CBV]
q:55 [binder, in PCF.CBN]
q:60 [binder, in PCF.CBV]
q:60 [binder, in PCF.CBN]
q:62 [binder, in PCF.PCF]
q:65 [binder, in PCF.CBV]
R
r1:19 [binder, in PCF.CBV]r1:23 [binder, in PCF.CBV]
r1:26 [binder, in PCF.CBV]
r2:21 [binder, in PCF.CBV]
r2:24 [binder, in PCF.CBV]
r2:27 [binder, in PCF.CBV]
r:16 [binder, in PCF.CBN]
r:17 [binder, in PCF.CBV]
r:20 [binder, in PCF.CBN]
r:24 [binder, in PCF.CBN]
r:28 [binder, in PCF.CBN]
r:31 [binder, in PCF.CBV]
r:33 [binder, in PCF.CBN]
r:36 [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:50 [binder, in PCF.CBV]
S
subst [definition, in PCF.PCF]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:72 [binder, in PCF.CBV]
t:111 [binder, in PCF.PCF]
t:17 [binder, in PCF.PCF]
t:17 [binder, in PCF.CBN]
t:21 [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_abs [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_abs [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]
v:12 [binder, in PCF.CBV]
v:12 [binder, in PCF.CBN]
v:62 [binder, in PCF.CBN]
v:67 [binder, in PCF.CBV]
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:44 [in PCF.CBN]
A:46 [in PCF.PCF]
A:48 [in PCF.CBV]
A:50 [in PCF.PCF]
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':26 [in PCF.CBN]b':29 [in PCF.CBV]
b':31 [in PCF.CBN]
b':34 [in PCF.CBV]
B:115 [in PCF.PCF]
b:25 [in PCF.CBN]
b:28 [in PCF.CBV]
b:3 [in PCF.CBV]
b:3 [in PCF.CBN]
b:30 [in PCF.CBN]
b:33 [in PCF.CBV]
b:35 [in PCF.CBN]
b:38 [in PCF.CBV]
B:39 [in PCF.PCF]
b:39 [in PCF.CBN]
b:42 [in PCF.CBV]
B:43 [in PCF.PCF]
B:47 [in PCF.PCF]
B:49 [in PCF.CBV]
B:51 [in PCF.PCF]
B:55 [in PCF.PCF]
b:57 [in PCF.PCF]
B:59 [in PCF.PCF]
B:66 [in PCF.PCF]
b:68 [in PCF.CBV]
B:70 [in PCF.PCF]
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:71 [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:43 [in PCF.CBN]
f:46 [in PCF.CBV]
f:8 [in PCF.PCF]
f:98 [in PCF.PCF]
G
g:47 [in PCF.CBV]g:70 [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:48 [in PCF.CBN]m:53 [in PCF.CBV]
m:53 [in PCF.CBN]
m:58 [in PCF.CBV]
m:58 [in PCF.CBN]
m:63 [in PCF.CBV]
m:69 [in PCF.CBV]
N
n1:46 [in PCF.CBN]n1:51 [in PCF.CBV]
n1:51 [in PCF.CBN]
n1:56 [in PCF.CBV]
n1:56 [in PCF.CBN]
n1:61 [in PCF.CBV]
n2:47 [in PCF.CBN]
n2:52 [in PCF.CBV]
n2:52 [in PCF.CBN]
n2:57 [in PCF.CBV]
n2:57 [in PCF.CBN]
n2:62 [in PCF.CBV]
n:4 [in PCF.CBV]
n:4 [in PCF.CBN]
n:73 [in PCF.PCF]
n:73 [in PCF.CBV]
n:76 [in PCF.CBV]
P
p':14 [in PCF.CBV]p':14 [in PCF.CBN]
p:108 [in PCF.PCF]
p:114 [in PCF.PCF]
p:13 [in PCF.CBV]
p:13 [in PCF.CBN]
p:18 [in PCF.CBV]
p:18 [in PCF.CBN]
p:22 [in PCF.CBV]
p:22 [in PCF.CBN]
p:25 [in PCF.CBV]
p:27 [in PCF.CBN]
p:30 [in PCF.CBV]
p:32 [in PCF.CBN]
p:35 [in PCF.CBV]
p:36 [in PCF.CBN]
p:39 [in PCF.CBV]
p:40 [in PCF.CBN]
p:43 [in PCF.CBV]
p:49 [in PCF.CBN]
p:54 [in PCF.CBV]
p:54 [in PCF.CBN]
p:59 [in PCF.CBV]
p:59 [in PCF.CBN]
p:60 [in PCF.PCF]
p:61 [in PCF.CBN]
p:64 [in PCF.CBV]
p:66 [in PCF.CBV]
Q
q':16 [in PCF.CBV]q:109 [in PCF.PCF]
q:116 [in PCF.PCF]
q:15 [in PCF.CBV]
q:15 [in PCF.CBN]
q:19 [in PCF.CBN]
q:20 [in PCF.CBV]
q:23 [in PCF.CBN]
q:29 [in PCF.CBN]
q:32 [in PCF.CBV]
q:34 [in PCF.CBN]
q:37 [in PCF.CBV]
q:38 [in PCF.CBN]
q:41 [in PCF.CBV]
q:42 [in PCF.CBN]
q:45 [in PCF.CBV]
q:50 [in PCF.CBN]
q:55 [in PCF.CBV]
q:55 [in PCF.CBN]
q:60 [in PCF.CBV]
q:60 [in PCF.CBN]
q:62 [in PCF.PCF]
q:65 [in PCF.CBV]
R
r1:19 [in PCF.CBV]r1:23 [in PCF.CBV]
r1:26 [in PCF.CBV]
r2:21 [in PCF.CBV]
r2:24 [in PCF.CBV]
r2:27 [in PCF.CBV]
r:16 [in PCF.CBN]
r:17 [in PCF.CBV]
r:20 [in PCF.CBN]
r:24 [in PCF.CBN]
r:28 [in PCF.CBN]
r:31 [in PCF.CBV]
r:33 [in PCF.CBN]
r:36 [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:50 [in PCF.CBV]
S
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:72 [in PCF.CBV]
t:111 [in PCF.PCF]
t:17 [in PCF.PCF]
t:17 [in PCF.CBN]
t:21 [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]
V
v:12 [in PCF.CBV]v:12 [in PCF.CBN]
v:62 [in PCF.CBN]
v:67 [in PCF.CBV]
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
B
bigCBN_reduces_to_value [in PCF.CBN]bigCBV_reduces_to_value [in PCF.CBV]
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_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_fix [in PCF.CBV]
bigCBV_ite_false [in PCF.CBV]
bigCBV_ite_true [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_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_abs [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_abs [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 | (347 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 | (233 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 | (6 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 | (81 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