Global Index

(192 entries)

Notation Index

other

(4 entries)

Variable Index

other

(30 entries)

Library Index

other

(1 entry)

Lemma Index

other

(24 entries)

Axiom Index

other

(2 entries)

Constructor Index

other

(3 entries)

Projection Index

other

(65 entries)

Inductive Index

other

(1 entry)

Section Index

other

(7 entries)

Instance Index

other

(2 entries)

Abbreviation Index

other

(2 entries)

Definition Index

other

(42 entries)

Record Index

other

(9 entries)

Global Index

A

abs [definition, in MCA]
after [projection, in MCA]
agreement [lemma, in MCA]
assoc [projection, in MCA]
ax_mono_imp [lemma, in MCA]
ax_mono_meet [lemma, in MCA]
ax_mono_ext [lemma, in MCA]
ax_mono_ext' [lemma, in MCA]
ax_inf' [lemma, in MCA]
ax_meet_right [lemma, in MCA]
ax_meet_left [lemma, in MCA]
ax_meet_assoc_inv [lemma, in MCA]
ax_meet_assoc [lemma, in MCA]
ax_meet_comm [lemma, in MCA]
ax_refl' [lemma, in MCA]
ax_mono [projection, in MCA]
ax_bind [projection, in MCA]
ax_ret [projection, in MCA]
ax_inf [projection, in MCA]
ax_imp [projection, in MCA]
ax_meet [projection, in MCA]
ax_meet2 [projection, in MCA]
ax_meet1 [projection, in MCA]
ax_bot [projection, in MCA]
ax_top [projection, in MCA]
ax_trans [projection, in MCA]
ax_refl [projection, in MCA]

B

Bcode1 [definition, in MCA]
Bcode2 [definition, in MCA]
bind [projection, in MCA]
bot [projection, in MCA]

C

ccomplete [definition, in MCA]
CE [lemma, in MCA]
cha [projection, in MCA]
CHA [record, in MCA]
code [projection, in MCA]
con [definition, in MCA]
conj [projection, in MCA]
continuation_monad [definition, in MCA]
con_eq [lemma, in MCA]
CPS [definition, in MCA]
cst [constructor, in MCA]

E

eapp [constructor, in MCA]
ebot [projection, in MCA]
EF [record, in MCA]
efst [projection, in MCA]
ef_uncurry [projection, in MCA]
ef_curry [projection, in MCA]
ef_snd [projection, in MCA]
ef_fst [projection, in MCA]
ef_pair [projection, in MCA]
ef_bot [projection, in MCA]
ef_top [projection, in MCA]
ef_trans [projection, in MCA]
ef_refl [projection, in MCA]
eid [projection, in MCA]
elam [projection, in MCA]
elem [projection, in MCA]
elem_proof [projection, in MCA]
epair [projection, in MCA]
erel [projection, in MCA]
erho [projection, in MCA]
eseq [projection, in MCA]
esnd [projection, in MCA]
etop [projection, in MCA]
eval [definition, in MCA]
evid [projection, in MCA]
Examples [section, in MCA]
Examples.CPS [section, in MCA]
Examples.CPS.Con [variable, in MCA]
Examples.mas_power [variable, in MCA]
Examples.mas_part [variable, in MCA]
Examples.ParCA [section, in MCA]
Examples.ParCA.mas_par [variable, in MCA]
Examples.ParCA.Par [variable, in MCA]
Examples.SCA [section, in MCA]
Examples.SCA.mas_state [variable, in MCA]
Examples.SCA.Sig [variable, in MCA]
Examples.SCA.srel [variable, in MCA]
Examples.SCA.srel_tran [variable, in MCA]
Examples.SCA.srel_refl [variable, in MCA]
exp [inductive, in MCA]
exp_sind [definition, in MCA]
exp_rec [definition, in MCA]
exp_ind [definition, in MCA]
exp_rect [definition, in MCA]

F

FE [axiom, in MCA]

H

hbot [projection, in MCA]
himp [projection, in MCA]
hinf [projection, in MCA]
hmeet [projection, in MCA]
hrel [projection, in MCA]
htop [projection, in MCA]

I

Icode [definition, in MCA]
imp_right [lemma, in MCA]

K

Kncode [definition, in MCA]
Kncode1 [definition, in MCA]

L

lam [projection, in MCA]
lam_O [projection, in MCA]
lam_S [projection, in MCA]
lunit [projection, in MCA]

M

M [projection, in MCA]
mapp [projection, in MCA]
MAS [record, in MCA]
MCA [record, in MCA]
MCA [library]
MCA_EF [instance, in MCA]
MMod [section, in MCA]
MMod [record, in MCA]
MMod.M [variable, in MCA]
MMod.mas [variable, in MCA]
MMod.mod [variable, in MCA]
Monad [record, in MCA]

O

Omega [projection, in MCA]

P

par [definition, in MCA]
parametric_progress [lemma, in MCA]
parametric_modality [definition, in MCA]
parametric_monad [definition, in MCA]
ParCA [definition, in MCA]
partiality_progress [lemma, in MCA]
partiality_modality [definition, in MCA]
partiality_monad [definition, in MCA]
par_eq [lemma, in MCA]
PCA [definition, in MCA]
PE [axiom, in MCA]
PI [lemma, in MCA]
powerset [definition, in MCA]
powerset_monad [definition, in MCA]
powerset_eq [lemma, in MCA]
pow_dem_modality [definition, in MCA]
pow_dem_naive_modality [definition, in MCA]
pow_ang_progress [lemma, in MCA]
pow_ang_modality [definition, in MCA]
progress [definition, in MCA]
prop [projection, in MCA]
p1 [abbreviation, in MCA]
p2 [abbreviation, in MCA]

R

RCA [definition, in MCA]
ret [projection, in MCA]
runit [projection, in MCA]

S

SCA [definition, in MCA]
Sep [section, in MCA]
separator [record, in MCA]
Sep.M [variable, in MCA]
Sep.mas [variable, in MCA]
Sep.mca [variable, in MCA]
Sep.mod [variable, in MCA]
Sep.sep [variable, in MCA]
Sep1 [projection, in MCA]
Sep2 [projection, in MCA]
size [definition, in MCA]
SK [section, in MCA]
skmca [instance, in MCA]
SK.appK [variable, in MCA]
SK.appK1 [variable, in MCA]
SK.appS [variable, in MCA]
SK.appS1 [variable, in MCA]
SK.appS2 [variable, in MCA]
SK.Kcode [variable, in MCA]
SK.Kcode1 [variable, in MCA]
SK.M [variable, in MCA]
SK.mas [variable, in MCA]
SK.Scode [variable, in MCA]
SK.Scode1 [variable, in MCA]
SK.Scode2 [variable, in MCA]
Sncode [definition, in MCA]
Sncode2 [definition, in MCA]
state [definition, in MCA]
state_ang_progress [lemma, in MCA]
state_ang_modality [definition, in MCA]
state_cha [definition, in MCA]
state_monad [definition, in MCA]
state_eq [lemma, in MCA]
subcode [record, in MCA]
subexp [definition, in MCA]
subs [definition, in MCA]
subset [projection, in MCA]
subsingleton [definition, in MCA]
subsingleton_eq [lemma, in MCA]
sub_cha [definition, in MCA]

T

TER [record, in MCA]
term_mod [definition, in MCA]
ter_bind [projection, in MCA]
ter_ret [projection, in MCA]
ter_pred [projection, in MCA]
top [projection, in MCA]

U

uimp [projection, in MCA]

V

var [constructor, in MCA]

other

_ <= _ [notation, in MCA]
$0 [notation, in MCA]
$1 [notation, in MCA]
$2 [notation, in MCA]

Notation Index

other

_ <= _ [in MCA]
$0 [in MCA]
$1 [in MCA]
$2 [in MCA]

Variable Index

E

Examples.CPS.Con [in MCA]
Examples.mas_power [in MCA]
Examples.mas_part [in MCA]
Examples.ParCA.mas_par [in MCA]
Examples.ParCA.Par [in MCA]
Examples.SCA.mas_state [in MCA]
Examples.SCA.Sig [in MCA]
Examples.SCA.srel [in MCA]
Examples.SCA.srel_tran [in MCA]
Examples.SCA.srel_refl [in MCA]

M

MMod.M [in MCA]
MMod.mas [in MCA]
MMod.mod [in MCA]

S

Sep.M [in MCA]
Sep.mas [in MCA]
Sep.mca [in MCA]
Sep.mod [in MCA]
Sep.sep [in MCA]
SK.appK [in MCA]
SK.appK1 [in MCA]
SK.appS [in MCA]
SK.appS1 [in MCA]
SK.appS2 [in MCA]
SK.Kcode [in MCA]
SK.Kcode1 [in MCA]
SK.M [in MCA]
SK.mas [in MCA]
SK.Scode [in MCA]
SK.Scode1 [in MCA]
SK.Scode2 [in MCA]

Library Index

M

MCA

Lemma Index

A

agreement [in MCA]
ax_mono_imp [in MCA]
ax_mono_meet [in MCA]
ax_mono_ext [in MCA]
ax_mono_ext' [in MCA]
ax_inf' [in MCA]
ax_meet_right [in MCA]
ax_meet_left [in MCA]
ax_meet_assoc_inv [in MCA]
ax_meet_assoc [in MCA]
ax_meet_comm [in MCA]
ax_refl' [in MCA]

C

CE [in MCA]
con_eq [in MCA]

I

imp_right [in MCA]

P

parametric_progress [in MCA]
partiality_progress [in MCA]
par_eq [in MCA]
PI [in MCA]
powerset_eq [in MCA]
pow_ang_progress [in MCA]

S

state_ang_progress [in MCA]
state_eq [in MCA]
subsingleton_eq [in MCA]

Axiom Index

F

FE [in MCA]

P

PE [in MCA]

Constructor Index

C

cst [in MCA]

E

eapp [in MCA]

V

var [in MCA]

Projection Index

A

after [in MCA]
assoc [in MCA]
ax_mono [in MCA]
ax_bind [in MCA]
ax_ret [in MCA]
ax_inf [in MCA]
ax_imp [in MCA]
ax_meet [in MCA]
ax_meet2 [in MCA]
ax_meet1 [in MCA]
ax_bot [in MCA]
ax_top [in MCA]
ax_trans [in MCA]
ax_refl [in MCA]

B

bind [in MCA]
bot [in MCA]

C

cha [in MCA]
code [in MCA]
conj [in MCA]

E

ebot [in MCA]
efst [in MCA]
ef_uncurry [in MCA]
ef_curry [in MCA]
ef_snd [in MCA]
ef_fst [in MCA]
ef_pair [in MCA]
ef_bot [in MCA]
ef_top [in MCA]
ef_trans [in MCA]
ef_refl [in MCA]
eid [in MCA]
elam [in MCA]
elem [in MCA]
elem_proof [in MCA]
epair [in MCA]
erel [in MCA]
erho [in MCA]
eseq [in MCA]
esnd [in MCA]
etop [in MCA]
evid [in MCA]

H

hbot [in MCA]
himp [in MCA]
hinf [in MCA]
hmeet [in MCA]
hrel [in MCA]
htop [in MCA]

L

lam [in MCA]
lam_O [in MCA]
lam_S [in MCA]
lunit [in MCA]

M

M [in MCA]
mapp [in MCA]

O

Omega [in MCA]

P

prop [in MCA]

R

ret [in MCA]
runit [in MCA]

S

Sep1 [in MCA]
Sep2 [in MCA]
subset [in MCA]

T

ter_bind [in MCA]
ter_ret [in MCA]
ter_pred [in MCA]
top [in MCA]

U

uimp [in MCA]

Inductive Index

E

exp [in MCA]

Section Index

E

Examples [in MCA]
Examples.CPS [in MCA]
Examples.ParCA [in MCA]
Examples.SCA [in MCA]

M

MMod [in MCA]

S

Sep [in MCA]
SK [in MCA]

Instance Index

M

MCA_EF [in MCA]

S

skmca [in MCA]

Abbreviation Index

P

p1 [in MCA]
p2 [in MCA]

Definition Index

A

abs [in MCA]

B

Bcode1 [in MCA]
Bcode2 [in MCA]

C

ccomplete [in MCA]
con [in MCA]
continuation_monad [in MCA]
CPS [in MCA]

E

eval [in MCA]
exp_sind [in MCA]
exp_rec [in MCA]
exp_ind [in MCA]
exp_rect [in MCA]

I

Icode [in MCA]

K

Kncode [in MCA]
Kncode1 [in MCA]

P

par [in MCA]
parametric_modality [in MCA]
parametric_monad [in MCA]
ParCA [in MCA]
partiality_modality [in MCA]
partiality_monad [in MCA]
PCA [in MCA]
powerset [in MCA]
powerset_monad [in MCA]
pow_dem_modality [in MCA]
pow_dem_naive_modality [in MCA]
pow_ang_modality [in MCA]
progress [in MCA]

R

RCA [in MCA]

S

SCA [in MCA]
size [in MCA]
Sncode [in MCA]
Sncode2 [in MCA]
state [in MCA]
state_ang_modality [in MCA]
state_cha [in MCA]
state_monad [in MCA]
subexp [in MCA]
subs [in MCA]
subsingleton [in MCA]
sub_cha [in MCA]

T

term_mod [in MCA]

Record Index

C

CHA [in MCA]

E

EF [in MCA]

M

MAS [in MCA]
MCA [in MCA]
MMod [in MCA]
Monad [in MCA]

S

separator [in MCA]
subcode [in MCA]

T

TER [in MCA]

Global Index

other

(192 entries)

Notation Index

other

(4 entries)

Variable Index

other

(30 entries)

Library Index

other

(1 entry)

Lemma Index

other

(24 entries)

Axiom Index

other

(2 entries)

Constructor Index

other

(3 entries)

Projection Index

other

(65 entries)

Inductive Index

other

(1 entry)

Section Index

other

(7 entries)

Instance Index

other

(2 entries)

Abbreviation Index

other

(2 entries)

Definition Index

other

(42 entries)

Record Index

other

(9 entries)