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
AllC
CE
EffectR
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]
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