| 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 | (217 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 | (24 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 | (9 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 | (65 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 | (11 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 | (13 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 | (78 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 | (5 entries) |
Global Index
A
algebraic [definition, in Io.Evaluate]All [library]
answer [projection, in Io.Effect]
answer [definition, in Io.Exception]
C
C [library]Call [constructor, in Io.Run]
Call [constructor, in Io.Trace]
Call [constructor, 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]
command [definition, in Io.Evaluate]
Command [module, in Io.Exception]
Command.Exc [constructor, in Io.Exception]
Command.Ok [constructor, in Io.Exception]
Command.t [inductive, in Io.Exception]
compose [definition, in Io.Effect]
E
effect [definition, in Io.Exception]Effect [library]
eval [definition, in Io.Exception]
EvalMonad [module, in Io.Evaluate]
EvalMonad.choose [projection, in Io.Evaluate]
EvalMonad.command [projection, in Io.Evaluate]
EvalMonad.join [projection, in Io.Evaluate]
EvalMonad.New [constructor, in Io.Evaluate]
EvalMonad.t [record, in Io.Evaluate]
Evaluate [library]
exception [definition, in Io.Evaluate]
Exception [library]
G
general [definition, in Io.UseCase]Generalize [module, in Io.UseCase]
Generalize.t [definition, in Io.UseCase]
H
handle [definition, in Io.Exception]Handler [module, in Io.Evaluate]
Handler.t [definition, in Io.Evaluate]
I
I [module, in Io.Run]I [module, in Io.Trace]
I [module, in Io.UseCase]
I [module, in Io.C]
I [module, in Io.Evaluate]
iter_par [definition, in Io.List]
iter_seq [definition, in Io.List]
I.Call [constructor, in Io.Run]
I.Call [constructor, in Io.Trace]
I.Call [constructor, 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.command [definition, in Io.Evaluate]
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.exception [definition, in Io.Evaluate]
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 [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.icall [definition, in Io.C]
I.Notations.ichoose [definition, in Io.C]
I.Notations.ijoin [definition, in Io.C]
I.Notations.iret [definition, in Io.C]
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 [constructor, in Io.C]
I.state [definition, in Io.Evaluate]
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 [constructor, in Io.C]
L
Let [constructor, in Io.Run]Let [constructor, in Io.Trace]
Let [constructor, in Io.C]
lift [definition, in Io.Exception]
List [library]
M
map_par [definition, in Io.List]map_seq [definition, in Io.List]
monad [definition, in Io.Evaluate]
Monad [module, in Io.Evaluate]
Monad.bind [projection, in Io.Evaluate]
Monad.New [constructor, in Io.Evaluate]
Monad.ret [projection, in Io.Evaluate]
Monad.t [record, in Io.Evaluate]
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.call [definition, in Io.C]
Notations.choose [definition, in Io.C]
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.join [definition, in Io.C]
Notations.ret [definition, in Io.Run]
Notations.ret [definition, in Io.Trace]
Notations.ret [definition, in Io.C]
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]pure [definition, in Io.Evaluate]
R
r [projection, in Io.UseCase]raise [definition, in Io.Exception]
Ret [constructor, in Io.Run]
Ret [constructor, in Io.Trace]
Ret [constructor, in Io.C]
Run [module, in Io.Evaluate]
Run [module, in Io.List]
Run [library]
Run.command [definition, in Io.Evaluate]
Run.exception [definition, in Io.Evaluate]
Run.I [module, in Io.Evaluate]
Run.I.command [definition, in Io.Evaluate]
Run.map_par_id [definition, in Io.List]
Run.map_par [definition, in Io.List]
Run.map_seq_id [definition, in Io.List]
Run.map_seq [definition, in Io.List]
S
state [definition, in Io.Evaluate]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
C
Command [in Io.Exception]E
EvalMonad [in Io.Evaluate]G
Generalize [in Io.UseCase]H
Handler [in Io.Evaluate]I
I [in Io.Run]I [in Io.Trace]
I [in Io.UseCase]
I [in Io.C]
I [in Io.Evaluate]
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]
M
Monad [in Io.Evaluate]N
Notations [in Io.Run]Notations [in Io.Trace]
Notations [in Io.C]
R
Run [in Io.Evaluate]Run [in Io.List]
Run.I [in Io.Evaluate]
V
Valid [in Io.Trace]Library Index
A
AllC
CE
EffectEvaluate
Exception
L
ListR
RunT
TraceU
UseCaseConstructor 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]
Command.Exc [in Io.Exception]
Command.Ok [in Io.Exception]
E
EvalMonad.New [in Io.Evaluate]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]
M
Monad.New [in Io.Evaluate]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
C
Command.t [in Io.Exception]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]E
EvalMonad.choose [in Io.Evaluate]EvalMonad.command [in Io.Evaluate]
EvalMonad.join [in Io.Evaluate]
I
I.P [in Io.UseCase]I.r [in Io.UseCase]
I.v [in Io.UseCase]
M
Monad.bind [in Io.Evaluate]Monad.ret [in Io.Evaluate]
P
P [in Io.UseCase]R
r [in Io.UseCase]V
v [in Io.UseCase]Definition Index
A
algebraic [in Io.Evaluate]answer [in Io.Exception]
C
command [in Io.Evaluate]compose [in Io.Effect]
E
effect [in Io.Exception]eval [in Io.Exception]
exception [in Io.Evaluate]
G
general [in Io.UseCase]Generalize.t [in Io.UseCase]
H
handle [in Io.Exception]Handler.t [in Io.Evaluate]
I
iter_par [in Io.List]iter_seq [in Io.List]
I.command [in Io.Evaluate]
I.exception [in Io.Evaluate]
I.Generalize.t [in Io.UseCase]
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.icall [in Io.C]
I.Notations.ichoose [in Io.C]
I.Notations.ijoin [in Io.C]
I.Notations.iret [in Io.C]
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.state [in Io.Evaluate]
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]
L
lift [in Io.Exception]M
map_par [in Io.List]map_seq [in Io.List]
monad [in Io.Evaluate]
N
Notations.call [in Io.Run]Notations.call [in Io.Trace]
Notations.call [in Io.C]
Notations.choose [in Io.C]
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.join [in Io.C]
Notations.ret [in Io.Run]
Notations.ret [in Io.Trace]
Notations.ret [in Io.C]
O
of_to_run [in Io.Trace]of_run [in Io.Trace]
P
pure [in Io.Evaluate]R
raise [in Io.Exception]Run.command [in Io.Evaluate]
Run.exception [in Io.Evaluate]
Run.I.command [in Io.Evaluate]
Run.map_par_id [in Io.List]
Run.map_par [in Io.List]
Run.map_seq_id [in Io.List]
Run.map_seq [in Io.List]
S
state [in Io.Evaluate]T
to_of_run [in Io.Trace]to_run [in Io.Trace]
Record Index
E
EvalMonad.t [in Io.Evaluate]I
I.t [in Io.UseCase]M
Monad.t [in Io.Evaluate]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 | (217 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 | (24 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 | (9 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 | (65 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 | (11 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 | (13 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 | (78 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 | (5 entries) |
This page has been generated by coqdoc