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

(143 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15 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

(91 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

(14 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

(23 entries)

---

Global Index

A

abs [constructor, in lazyPCF.OpSem.syntax]
Ap [inductive, in lazyPCF.OpSem.OSrules]
appl [constructor, in lazyPCF.OpSem.syntax]
ApTypes [library]
Ap_clos [constructor, in lazyPCF.OpSem.OSrules]
Ap_abs [constructor, in lazyPCF.OpSem.OSrules]
arr [constructor, in lazyPCF.OpSem.syntax]

B

bool_ty [constructor, in lazyPCF.OpSem.syntax]

C

cfg [constructor, in lazyPCF.OpSem.environments]
cfgenv [definition, in lazyPCF.OpSem.environments]
cfgexp [definition, in lazyPCF.OpSem.environments]
clos [constructor, in lazyPCF.OpSem.syntax]
cond [constructor, in lazyPCF.OpSem.syntax]
config [inductive, in lazyPCF.OpSem.environments]

E

environments [library]
envprops [library]

F

F [inductive, in lazyPCF.SubjRed.NF]
fff [constructor, in lazyPCF.OpSem.syntax]
Fix [constructor, in lazyPCF.OpSem.syntax]
freevars [library]
fv [definition, in lazyPCF.OpSem.freevars]
FV [inductive, in lazyPCF.OpSem.freevars]
FV_closb [constructor, in lazyPCF.OpSem.freevars]
FV_closa [constructor, in lazyPCF.OpSem.freevars]
FV_is_o [constructor, in lazyPCF.OpSem.freevars]
FV_prd [constructor, in lazyPCF.OpSem.freevars]
FV_succ [constructor, in lazyPCF.OpSem.freevars]
FV_var [constructor, in lazyPCF.OpSem.freevars]
FV_cond3 [constructor, in lazyPCF.OpSem.freevars]
FV_cond2 [constructor, in lazyPCF.OpSem.freevars]
FV_cond1 [constructor, in lazyPCF.OpSem.freevars]
FV_appl2 [constructor, in lazyPCF.OpSem.freevars]
FV_appl1 [constructor, in lazyPCF.OpSem.freevars]
FV_fix [constructor, in lazyPCF.OpSem.freevars]
FV_abs [constructor, in lazyPCF.OpSem.freevars]
F_clos [constructor, in lazyPCF.SubjRed.NF]
F_abs [constructor, in lazyPCF.SubjRed.NF]

I

is_o [constructor, in lazyPCF.OpSem.syntax]
is_arr [definition, in lazyPCF.OpSem.utils]
is_bool [definition, in lazyPCF.OpSem.utils]
is_nat [definition, in lazyPCF.OpSem.utils]

M

mapsto [definition, in lazyPCF.OpSem.environments]
mapsto [library]
member [definition, in lazyPCF.OpSem.environments]

N

nat_ty [constructor, in lazyPCF.OpSem.syntax]
NF [inductive, in lazyPCF.SubjRed.NF]
NF [library]
NFprops [library]
NFsucc [definition, in lazyPCF.SubjRed.NF]
NF_F [constructor, in lazyPCF.SubjRed.NF]
NF_Sno [constructor, in lazyPCF.SubjRed.NF]
NF_fff [constructor, in lazyPCF.SubjRed.NF]
NF_ttt [constructor, in lazyPCF.SubjRed.NF]

O

o [constructor, in lazyPCF.OpSem.syntax]
OScons [definition, in lazyPCF.OpSem.OSrules]
OSred [inductive, in lazyPCF.OpSem.OSrules]
OSrules [library]
OS_Dom_ty [definition, in lazyPCF.OpSem.environments]
OS_Dom [definition, in lazyPCF.OpSem.environments]
OS_env [definition, in lazyPCF.OpSem.environments]
OS_CL' [constructor, in lazyPCF.OpSem.OSrules]
OS_CL [constructor, in lazyPCF.OpSem.OSrules]
OS_Fix [constructor, in lazyPCF.OpSem.OSrules]
OS_IfFalse [constructor, in lazyPCF.OpSem.OSrules]
OS_IfTrue [constructor, in lazyPCF.OpSem.OSrules]
OS_Appl [constructor, in lazyPCF.OpSem.OSrules]
OS_Var2 [constructor, in lazyPCF.OpSem.OSrules]
OS_Var1 [constructor, in lazyPCF.OpSem.OSrules]
OS_S [constructor, in lazyPCF.OpSem.OSrules]
OS_ZF [constructor, in lazyPCF.OpSem.OSrules]
OS_ZT [constructor, in lazyPCF.OpSem.OSrules]
OS_P [constructor, in lazyPCF.OpSem.OSrules]
OS_P0 [constructor, in lazyPCF.OpSem.OSrules]
OS_L [constructor, in lazyPCF.OpSem.OSrules]
OS_CF [constructor, in lazyPCF.OpSem.OSrules]
OS_CT [constructor, in lazyPCF.OpSem.OSrules]
OS_C0 [constructor, in lazyPCF.OpSem.OSrules]

P

prd [constructor, in lazyPCF.OpSem.syntax]

R

Rand_ty [definition, in lazyPCF.OpSem.utils]
Rator_ty [definition, in lazyPCF.OpSem.utils]
rename [inductive, in lazyPCF.OpSem.rename]
rename [library]
ren_clos3 [constructor, in lazyPCF.OpSem.rename]
ren_clos2 [constructor, in lazyPCF.OpSem.rename]
ren_clos1 [constructor, in lazyPCF.OpSem.rename]
ren_fix3 [constructor, in lazyPCF.OpSem.rename]
ren_fix2 [constructor, in lazyPCF.OpSem.rename]
ren_fix1 [constructor, in lazyPCF.OpSem.rename]
ren_is_o [constructor, in lazyPCF.OpSem.rename]
ren_prd [constructor, in lazyPCF.OpSem.rename]
ren_succ [constructor, in lazyPCF.OpSem.rename]
ren_var_not_eq [constructor, in lazyPCF.OpSem.rename]
ren_var_eq [constructor, in lazyPCF.OpSem.rename]
ren_cond [constructor, in lazyPCF.OpSem.rename]
ren_appl [constructor, in lazyPCF.OpSem.rename]
ren_abs3 [constructor, in lazyPCF.OpSem.rename]
ren_abs2 [constructor, in lazyPCF.OpSem.rename]
ren_abs1 [constructor, in lazyPCF.OpSem.rename]
ren_fff [constructor, in lazyPCF.OpSem.rename]
ren_ttt [constructor, in lazyPCF.OpSem.rename]
ren_o [constructor, in lazyPCF.OpSem.rename]

S

Sno [inductive, in lazyPCF.SubjRed.NF]
SnoSucc [definition, in lazyPCF.SubjRed.NF]
Sno_s [constructor, in lazyPCF.SubjRed.NF]
Sno_o [constructor, in lazyPCF.SubjRed.NF]
subjrnf [library]
succ [constructor, in lazyPCF.OpSem.syntax]
syntax [library]

T

tc [definition, in lazyPCF.OpSem.typecheck]
TC [inductive, in lazyPCF.OpSem.typecheck]
TC_clos [constructor, in lazyPCF.OpSem.typecheck]
TC_fix [constructor, in lazyPCF.OpSem.typecheck]
TC_cond [constructor, in lazyPCF.OpSem.typecheck]
TC_abs [constructor, in lazyPCF.OpSem.typecheck]
TC_appl [constructor, in lazyPCF.OpSem.typecheck]
TC_var [constructor, in lazyPCF.OpSem.typecheck]
TC_is_o [constructor, in lazyPCF.OpSem.typecheck]
TC_prd [constructor, in lazyPCF.OpSem.typecheck]
TC_succ [constructor, in lazyPCF.OpSem.typecheck]
TC_fff [constructor, in lazyPCF.OpSem.typecheck]
TC_ttt [constructor, in lazyPCF.OpSem.typecheck]
TC_o [constructor, in lazyPCF.OpSem.typecheck]
TE_Dom [definition, in lazyPCF.OpSem.environments]
tm [inductive, in lazyPCF.OpSem.syntax]
ttt [constructor, in lazyPCF.OpSem.syntax]
ty [inductive, in lazyPCF.OpSem.syntax]
typecheck [library]
TypeThms [library]
ty_env [definition, in lazyPCF.OpSem.environments]

U

utils [library]

V

valid [library]
valid_c [definition, in lazyPCF.SubjRed.valid]
valid_cfg [constructor, in lazyPCF.SubjRed.valid]
valid_config [inductive, in lazyPCF.SubjRed.valid]
valid_cons [constructor, in lazyPCF.SubjRed.valid]
valid_nil [constructor, in lazyPCF.SubjRed.valid]
valid_env [inductive, in lazyPCF.SubjRed.valid]
valu [definition, in lazyPCF.OpSem.utils]
var [constructor, in lazyPCF.OpSem.syntax]
vari [inductive, in lazyPCF.OpSem.syntax]
VT [definition, in lazyPCF.OpSem.environments]
VTT [definition, in lazyPCF.OpSem.environments]

X

x [constructor, in lazyPCF.OpSem.syntax]

---

Library Index

A

ApTypes

E

environments
envprops

F

freevars

M

mapsto

N

NF
NFprops

O

OSrules

R

rename

S

subjrnf
syntax

T

typecheck
TypeThms

U

utils

V

valid

---

Constructor Index

A

abs [in lazyPCF.OpSem.syntax]
appl [in lazyPCF.OpSem.syntax]
Ap_clos [in lazyPCF.OpSem.OSrules]
Ap_abs [in lazyPCF.OpSem.OSrules]
arr [in lazyPCF.OpSem.syntax]

B

bool_ty [in lazyPCF.OpSem.syntax]

C

cfg [in lazyPCF.OpSem.environments]
clos [in lazyPCF.OpSem.syntax]
cond [in lazyPCF.OpSem.syntax]

F

fff [in lazyPCF.OpSem.syntax]
Fix [in lazyPCF.OpSem.syntax]
FV_closb [in lazyPCF.OpSem.freevars]
FV_closa [in lazyPCF.OpSem.freevars]
FV_is_o [in lazyPCF.OpSem.freevars]
FV_prd [in lazyPCF.OpSem.freevars]
FV_succ [in lazyPCF.OpSem.freevars]
FV_var [in lazyPCF.OpSem.freevars]
FV_cond3 [in lazyPCF.OpSem.freevars]
FV_cond2 [in lazyPCF.OpSem.freevars]
FV_cond1 [in lazyPCF.OpSem.freevars]
FV_appl2 [in lazyPCF.OpSem.freevars]
FV_appl1 [in lazyPCF.OpSem.freevars]
FV_fix [in lazyPCF.OpSem.freevars]
FV_abs [in lazyPCF.OpSem.freevars]
F_clos [in lazyPCF.SubjRed.NF]
F_abs [in lazyPCF.SubjRed.NF]

I

is_o [in lazyPCF.OpSem.syntax]

N

nat_ty [in lazyPCF.OpSem.syntax]
NF_F [in lazyPCF.SubjRed.NF]
NF_Sno [in lazyPCF.SubjRed.NF]
NF_fff [in lazyPCF.SubjRed.NF]
NF_ttt [in lazyPCF.SubjRed.NF]

O

o [in lazyPCF.OpSem.syntax]
OS_CL' [in lazyPCF.OpSem.OSrules]
OS_CL [in lazyPCF.OpSem.OSrules]
OS_Fix [in lazyPCF.OpSem.OSrules]
OS_IfFalse [in lazyPCF.OpSem.OSrules]
OS_IfTrue [in lazyPCF.OpSem.OSrules]
OS_Appl [in lazyPCF.OpSem.OSrules]
OS_Var2 [in lazyPCF.OpSem.OSrules]
OS_Var1 [in lazyPCF.OpSem.OSrules]
OS_S [in lazyPCF.OpSem.OSrules]
OS_ZF [in lazyPCF.OpSem.OSrules]
OS_ZT [in lazyPCF.OpSem.OSrules]
OS_P [in lazyPCF.OpSem.OSrules]
OS_P0 [in lazyPCF.OpSem.OSrules]
OS_L [in lazyPCF.OpSem.OSrules]
OS_CF [in lazyPCF.OpSem.OSrules]
OS_CT [in lazyPCF.OpSem.OSrules]
OS_C0 [in lazyPCF.OpSem.OSrules]

P

prd [in lazyPCF.OpSem.syntax]

R

ren_clos3 [in lazyPCF.OpSem.rename]
ren_clos2 [in lazyPCF.OpSem.rename]
ren_clos1 [in lazyPCF.OpSem.rename]
ren_fix3 [in lazyPCF.OpSem.rename]
ren_fix2 [in lazyPCF.OpSem.rename]
ren_fix1 [in lazyPCF.OpSem.rename]
ren_is_o [in lazyPCF.OpSem.rename]
ren_prd [in lazyPCF.OpSem.rename]
ren_succ [in lazyPCF.OpSem.rename]
ren_var_not_eq [in lazyPCF.OpSem.rename]
ren_var_eq [in lazyPCF.OpSem.rename]
ren_cond [in lazyPCF.OpSem.rename]
ren_appl [in lazyPCF.OpSem.rename]
ren_abs3 [in lazyPCF.OpSem.rename]
ren_abs2 [in lazyPCF.OpSem.rename]
ren_abs1 [in lazyPCF.OpSem.rename]
ren_fff [in lazyPCF.OpSem.rename]
ren_ttt [in lazyPCF.OpSem.rename]
ren_o [in lazyPCF.OpSem.rename]

S

Sno_s [in lazyPCF.SubjRed.NF]
Sno_o [in lazyPCF.SubjRed.NF]
succ [in lazyPCF.OpSem.syntax]

T

TC_clos [in lazyPCF.OpSem.typecheck]
TC_fix [in lazyPCF.OpSem.typecheck]
TC_cond [in lazyPCF.OpSem.typecheck]
TC_abs [in lazyPCF.OpSem.typecheck]
TC_appl [in lazyPCF.OpSem.typecheck]
TC_var [in lazyPCF.OpSem.typecheck]
TC_is_o [in lazyPCF.OpSem.typecheck]
TC_prd [in lazyPCF.OpSem.typecheck]
TC_succ [in lazyPCF.OpSem.typecheck]
TC_fff [in lazyPCF.OpSem.typecheck]
TC_ttt [in lazyPCF.OpSem.typecheck]
TC_o [in lazyPCF.OpSem.typecheck]
ttt [in lazyPCF.OpSem.syntax]

V

valid_cfg [in lazyPCF.SubjRed.valid]
valid_cons [in lazyPCF.SubjRed.valid]
valid_nil [in lazyPCF.SubjRed.valid]
var [in lazyPCF.OpSem.syntax]

X

x [in lazyPCF.OpSem.syntax]

---

Inductive Index

A

Ap [in lazyPCF.OpSem.OSrules]

C

config [in lazyPCF.OpSem.environments]

F

F [in lazyPCF.SubjRed.NF]
FV [in lazyPCF.OpSem.freevars]

N

NF [in lazyPCF.SubjRed.NF]

O

OSred [in lazyPCF.OpSem.OSrules]

R

rename [in lazyPCF.OpSem.rename]

S

Sno [in lazyPCF.SubjRed.NF]

T

TC [in lazyPCF.OpSem.typecheck]
tm [in lazyPCF.OpSem.syntax]
ty [in lazyPCF.OpSem.syntax]

V

valid_config [in lazyPCF.SubjRed.valid]
valid_env [in lazyPCF.SubjRed.valid]
vari [in lazyPCF.OpSem.syntax]

---

Definition Index

C

cfgenv [in lazyPCF.OpSem.environments]
cfgexp [in lazyPCF.OpSem.environments]

F

fv [in lazyPCF.OpSem.freevars]

I

is_arr [in lazyPCF.OpSem.utils]
is_bool [in lazyPCF.OpSem.utils]
is_nat [in lazyPCF.OpSem.utils]

M

mapsto [in lazyPCF.OpSem.environments]
member [in lazyPCF.OpSem.environments]

N

NFsucc [in lazyPCF.SubjRed.NF]

O

OScons [in lazyPCF.OpSem.OSrules]
OS_Dom_ty [in lazyPCF.OpSem.environments]
OS_Dom [in lazyPCF.OpSem.environments]
OS_env [in lazyPCF.OpSem.environments]

R

Rand_ty [in lazyPCF.OpSem.utils]
Rator_ty [in lazyPCF.OpSem.utils]

S

SnoSucc [in lazyPCF.SubjRed.NF]

T

tc [in lazyPCF.OpSem.typecheck]
TE_Dom [in lazyPCF.OpSem.environments]
ty_env [in lazyPCF.OpSem.environments]

V

valid_c [in lazyPCF.SubjRed.valid]
valu [in lazyPCF.OpSem.utils]
VT [in lazyPCF.OpSem.environments]
VTT [in lazyPCF.OpSem.environments]

---

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

(143 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15 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

(91 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

(14 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

(23 entries)