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 (166 entries)
Notation 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 (12 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 (16 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 (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 (61 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 (10 entries)
Projection 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 (8 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 (50 entries)
Record 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)

Global Index

A

All [library]
answer [projection, in Io.Effect]


C

C [library]
Call [constructor, in Io.Run]
Call [constructor, in Io.Trace]
call [definition, in Io.C]
Call [constructor, in Io.C]
choose [definition, in Io.C]
Choose [constructor, in Io.C]
ChooseLeft [constructor, in Io.Run]
ChooseLeft [constructor, in Io.Trace]
ChooseRight [constructor, in Io.Run]
ChooseRight [constructor, in Io.Trace]
command [projection, in Io.Effect]


E

Effect [library]


G

general [definition, in Io.UseCase]
Generalize [module, in Io.UseCase]
Generalize.t [definition, in Io.UseCase]


I

I [module, in Io.Run]
I [module, in Io.Trace]
I [module, in Io.UseCase]
I [module, in Io.C]
I.Call [constructor, in Io.Run]
I.Call [constructor, in Io.Trace]
I.call [definition, in Io.C]
I.Call [constructor, in Io.C]
I.choose [definition, in Io.C]
I.Choose [constructor, in Io.C]
I.ChooseLeft [constructor, in Io.Run]
I.ChooseLeft [constructor, in Io.Trace]
I.ChooseRight [constructor, in Io.Run]
I.ChooseRight [constructor, in Io.Trace]
I.Eq [module, in Io.Run]
I.Eq [module, in Io.Trace]
I.Eq.Call [constructor, in Io.Run]
I.Eq.Call [constructor, in Io.Trace]
I.Eq.ChooseLeft [constructor, in Io.Run]
I.Eq.ChooseLeft [constructor, in Io.Trace]
I.Eq.ChooseRight [constructor, in Io.Run]
I.Eq.ChooseRight [constructor, in Io.Trace]
I.Eq.Join [constructor, in Io.Run]
I.Eq.Join [constructor, in Io.Trace]
I.Eq.Let [constructor, in Io.Run]
I.Eq.Let [constructor, in Io.Trace]
I.Eq.Ret [constructor, in Io.Run]
I.Eq.Ret [constructor, in Io.Trace]
I.Eq.t [inductive, in Io.Run]
I.Eq.t [inductive, in Io.Trace]
I.Generalize [module, in Io.UseCase]
I.Generalize.t [definition, in Io.UseCase]
I.Join [constructor, in Io.Run]
I.Join [constructor, in Io.Trace]
I.join [definition, in Io.C]
I.Join [constructor, in Io.C]
I.Let [constructor, in Io.Run]
I.Let [constructor, in Io.Trace]
I.Let [constructor, in Io.C]
I.lift [definition, in Io.Run]
I.lift [definition, in Io.C]
I.New [constructor, in Io.UseCase]
I.Notations [module, in Io.Run]
I.Notations [module, in Io.Trace]
I.Notations [module, in Io.C]
I.Notations.call [definition, in Io.Run]
I.Notations.call [definition, in Io.Trace]
I.Notations.choose_right [definition, in Io.Run]
I.Notations.choose_left [definition, in Io.Run]
I.Notations.choose_right [definition, in Io.Trace]
I.Notations.choose_left [definition, in Io.Trace]
I.Notations.join [definition, in Io.Run]
I.Notations.join [definition, in Io.Trace]
I.Notations.ret [definition, in Io.Run]
I.Notations.ret [definition, in Io.Trace]
ido! _ in _ [notation, in Io.C]
ilet! _ : _ := _ in _ [notation, in Io.C]
ilet! _ := _ in _ [notation, in Io.C]
rdo! _ in _ [notation, in Io.Run]
rlet! _ in _ [notation, in Io.Run]
tilet! _ in _ [notation, in Io.Trace]
I.P [projection, in Io.UseCase]
I.r [projection, in Io.UseCase]
I.Ret [constructor, in Io.Run]
I.Ret [constructor, in Io.Trace]
I.ret [definition, in Io.C]
I.Ret [constructor, in Io.C]
I.t [inductive, in Io.Run]
I.t [inductive, in Io.Trace]
I.t [record, in Io.UseCase]
I.t [inductive, in Io.C]
I.to_of_run [definition, in Io.Trace]
I.to_run [definition, in Io.Trace]
I.trace_of_to_run [definition, in Io.Trace]
I.trace_of_run [definition, in Io.Trace]
I.unfold [definition, in Io.Run]
I.unfold [definition, in Io.Trace]
I.unfold [definition, in Io.C]
I.unfold_eq [definition, in Io.Run]
I.unfold_eq [definition, in Io.Trace]
I.unfold_eq [definition, in Io.C]
I.v [projection, in Io.UseCase]
I.Valid [module, in Io.Trace]
I.valid_of_run [definition, in Io.Trace]
I.Valid.Call [constructor, in Io.Trace]
I.Valid.ChooseLeft [constructor, in Io.Trace]
I.Valid.ChooseRight [constructor, in Io.Trace]
I.Valid.Join [constructor, in Io.Trace]
I.Valid.Let [constructor, in Io.Trace]
I.Valid.Ret [constructor, in Io.Trace]
I.Valid.t [inductive, in Io.Trace]
I.Valid.unfold [definition, in Io.Trace]
I.Valid.unfold_eq [definition, in Io.Trace]


J

Join [constructor, in Io.Run]
Join [constructor, in Io.Trace]
join [definition, in Io.C]
Join [constructor, in Io.C]


L

Let [constructor, in Io.Run]
Let [constructor, in Io.Trace]
Let [constructor, in Io.C]


N

New [constructor, in Io.Effect]
New [constructor, in Io.UseCase]
Notations [module, in Io.Run]
Notations [module, in Io.Trace]
Notations [module, in Io.C]
Notations.call [definition, in Io.Run]
Notations.call [definition, in Io.Trace]
Notations.choose_right [definition, in Io.Run]
Notations.choose_left [definition, in Io.Run]
Notations.choose_right [definition, in Io.Trace]
Notations.choose_left [definition, in Io.Trace]
Notations.join [definition, in Io.Run]
Notations.join [definition, in Io.Trace]
Notations.ret [definition, in Io.Run]
Notations.ret [definition, in Io.Trace]
do! _ in _ [notation, in Io.C]
let! _ : _ := _ in _ [notation, in Io.C]
let! _ := _ in _ [notation, in Io.C]
rdo! _ in _ [notation, in Io.Run]
rlet! _ in _ [notation, in Io.Run]
tlet! _ in _ [notation, in Io.Trace]


O

of_to_run [definition, in Io.Trace]
of_run [definition, in Io.Trace]


P

P [projection, in Io.UseCase]


R

r [projection, in Io.UseCase]
Ret [constructor, in Io.Run]
Ret [constructor, in Io.Trace]
ret [definition, in Io.C]
Ret [constructor, in Io.C]
Run [library]


T

t [inductive, in Io.Run]
t [record, in Io.Effect]
t [inductive, in Io.Trace]
t [record, in Io.UseCase]
t [inductive, in Io.C]
to_of_run [definition, in Io.Trace]
to_run [definition, in Io.Trace]
Trace [library]


U

UseCase [library]


V

v [projection, in Io.UseCase]
Valid [module, in Io.Trace]
Valid.Call [constructor, in Io.Trace]
Valid.ChooseLeft [constructor, in Io.Trace]
Valid.ChooseRight [constructor, in Io.Trace]
Valid.Join [constructor, in Io.Trace]
Valid.Let [constructor, in Io.Trace]
Valid.Ret [constructor, in Io.Trace]
Valid.t [inductive, in Io.Trace]



Notation Index

I

ido! _ in _ [in Io.C]
ilet! _ : _ := _ in _ [in Io.C]
ilet! _ := _ in _ [in Io.C]
rdo! _ in _ [in Io.Run]
rlet! _ in _ [in Io.Run]
tilet! _ in _ [in Io.Trace]


N

do! _ in _ [in Io.C]
let! _ : _ := _ in _ [in Io.C]
let! _ := _ in _ [in Io.C]
rdo! _ in _ [in Io.Run]
rlet! _ in _ [in Io.Run]
tlet! _ in _ [in Io.Trace]



Module Index

G

Generalize [in Io.UseCase]


I

I [in Io.Run]
I [in Io.Trace]
I [in Io.UseCase]
I [in Io.C]
I.Eq [in Io.Run]
I.Eq [in Io.Trace]
I.Generalize [in Io.UseCase]
I.Notations [in Io.Run]
I.Notations [in Io.Trace]
I.Notations [in Io.C]
I.Valid [in Io.Trace]


N

Notations [in Io.Run]
Notations [in Io.Trace]
Notations [in Io.C]


V

Valid [in Io.Trace]



Library Index

A

All


C

C


E

Effect


R

Run


T

Trace


U

UseCase



Constructor Index

C

Call [in Io.Run]
Call [in Io.Trace]
Call [in Io.C]
Choose [in Io.C]
ChooseLeft [in Io.Run]
ChooseLeft [in Io.Trace]
ChooseRight [in Io.Run]
ChooseRight [in Io.Trace]


I

I.Call [in Io.Run]
I.Call [in Io.Trace]
I.Call [in Io.C]
I.Choose [in Io.C]
I.ChooseLeft [in Io.Run]
I.ChooseLeft [in Io.Trace]
I.ChooseRight [in Io.Run]
I.ChooseRight [in Io.Trace]
I.Eq.Call [in Io.Run]
I.Eq.Call [in Io.Trace]
I.Eq.ChooseLeft [in Io.Run]
I.Eq.ChooseLeft [in Io.Trace]
I.Eq.ChooseRight [in Io.Run]
I.Eq.ChooseRight [in Io.Trace]
I.Eq.Join [in Io.Run]
I.Eq.Join [in Io.Trace]
I.Eq.Let [in Io.Run]
I.Eq.Let [in Io.Trace]
I.Eq.Ret [in Io.Run]
I.Eq.Ret [in Io.Trace]
I.Join [in Io.Run]
I.Join [in Io.Trace]
I.Join [in Io.C]
I.Let [in Io.Run]
I.Let [in Io.Trace]
I.Let [in Io.C]
I.New [in Io.UseCase]
I.Ret [in Io.Run]
I.Ret [in Io.Trace]
I.Ret [in Io.C]
I.Valid.Call [in Io.Trace]
I.Valid.ChooseLeft [in Io.Trace]
I.Valid.ChooseRight [in Io.Trace]
I.Valid.Join [in Io.Trace]
I.Valid.Let [in Io.Trace]
I.Valid.Ret [in Io.Trace]


J

Join [in Io.Run]
Join [in Io.Trace]
Join [in Io.C]


L

Let [in Io.Run]
Let [in Io.Trace]
Let [in Io.C]


N

New [in Io.Effect]
New [in Io.UseCase]


R

Ret [in Io.Run]
Ret [in Io.Trace]
Ret [in Io.C]


V

Valid.Call [in Io.Trace]
Valid.ChooseLeft [in Io.Trace]
Valid.ChooseRight [in Io.Trace]
Valid.Join [in Io.Trace]
Valid.Let [in Io.Trace]
Valid.Ret [in Io.Trace]



Inductive Index

I

I.Eq.t [in Io.Run]
I.Eq.t [in Io.Trace]
I.t [in Io.Run]
I.t [in Io.Trace]
I.t [in Io.C]
I.Valid.t [in Io.Trace]


T

t [in Io.Run]
t [in Io.Trace]
t [in Io.C]


V

Valid.t [in Io.Trace]



Projection Index

A

answer [in Io.Effect]


C

command [in Io.Effect]


I

I.P [in Io.UseCase]
I.r [in Io.UseCase]
I.v [in Io.UseCase]


P

P [in Io.UseCase]


R

r [in Io.UseCase]


V

v [in Io.UseCase]



Definition Index

C

call [in Io.C]
choose [in Io.C]


G

general [in Io.UseCase]
Generalize.t [in Io.UseCase]


I

I.call [in Io.C]
I.choose [in Io.C]
I.Generalize.t [in Io.UseCase]
I.join [in Io.C]
I.lift [in Io.Run]
I.lift [in Io.C]
I.Notations.call [in Io.Run]
I.Notations.call [in Io.Trace]
I.Notations.choose_right [in Io.Run]
I.Notations.choose_left [in Io.Run]
I.Notations.choose_right [in Io.Trace]
I.Notations.choose_left [in Io.Trace]
I.Notations.join [in Io.Run]
I.Notations.join [in Io.Trace]
I.Notations.ret [in Io.Run]
I.Notations.ret [in Io.Trace]
I.ret [in Io.C]
I.to_of_run [in Io.Trace]
I.to_run [in Io.Trace]
I.trace_of_to_run [in Io.Trace]
I.trace_of_run [in Io.Trace]
I.unfold [in Io.Run]
I.unfold [in Io.Trace]
I.unfold [in Io.C]
I.unfold_eq [in Io.Run]
I.unfold_eq [in Io.Trace]
I.unfold_eq [in Io.C]
I.valid_of_run [in Io.Trace]
I.Valid.unfold [in Io.Trace]
I.Valid.unfold_eq [in Io.Trace]


J

join [in Io.C]


N

Notations.call [in Io.Run]
Notations.call [in Io.Trace]
Notations.choose_right [in Io.Run]
Notations.choose_left [in Io.Run]
Notations.choose_right [in Io.Trace]
Notations.choose_left [in Io.Trace]
Notations.join [in Io.Run]
Notations.join [in Io.Trace]
Notations.ret [in Io.Run]
Notations.ret [in Io.Trace]


O

of_to_run [in Io.Trace]
of_run [in Io.Trace]


R

ret [in Io.C]


T

to_of_run [in Io.Trace]
to_run [in Io.Trace]



Record Index

I

I.t [in Io.UseCase]


T

t [in Io.Effect]
t [in Io.UseCase]



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 (166 entries)
Notation 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 (12 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 (16 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 (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 (61 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 (10 entries)
Projection 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 (8 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 (50 entries)
Record 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)

This page has been generated by coqdoc