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

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

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

(5 entries)

Variable 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

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

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

(19 entries)

Lemma 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

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

(15 entries)

Instance 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

(169 entries)

Section 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

(27 entries)

Abbreviation 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

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

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

(126 entries)

---

Global Index

A

alternative [definition, in bedrock.upoly.option]
alternative [definition, in bedrock.upoly.trace]
alternative [instance, in bedrock.upoly.readerT]
alternative [instance, in bedrock.upoly.stateT]
alternative [definition, in bedrock.upoly.traceT]
alternative [definition, in bedrock.upoly.list]
alternative [definition, in bedrock.upoly.listT]
alternative [definition, in bedrock.upoly.optionT]
alternative_not_lazy [definition, in bedrock.upoly.traceT]
alternative_not_lazy [definition, in bedrock.upoly.listT]
alternative_not_lazy [definition, in bedrock.upoly.optionT]
any [definition, in bedrock.upoly.parsec]
anyOf [definition, in bedrock.upoly.parsec]
ap [definition, in bedrock.upoly.option]
ap [definition, in bedrock.upoly.trace]
ap [instance, in bedrock.upoly.readerT]
ap [instance, in bedrock.upoly.reader]
ap [definition, in bedrock.upoly.stateT]
ap [instance, in bedrock.upoly.traceT]
ap [definition, in bedrock.upoly.list]
ap [instance, in bedrock.upoly.listT]
ap [instance, in bedrock.upoly.writerT]
ap [definition, in bedrock.upoly.state]
ap [definition, in bedrock.upoly.id]
ap [instance, in bedrock.upoly.optionT]
ap [instance, in bedrock.upoly.writer]
app [definition, in bedrock.upoly.list]
app' [definition, in bedrock.upoly.list]
Ap_M [instance, in bedrock.upoly.parsec]
ask [definition, in bedrock.upoly.readerT]
ask [definition, in bedrock.upoly.reader]
asks [definition, in bedrock.upoly.readerT]
asks [definition, in bedrock.upoly.reader]
asksM [definition, in bedrock.upoly.readerT]

B

Backtrace [constructor, in bedrock.upoly.trace]
base [library]
bind [instance, in bedrock.upoly.option]
bind [instance, in bedrock.upoly.trace]
bind [instance, in bedrock.upoly.readerT]
bind [instance, in bedrock.upoly.reader]
bind [instance, in bedrock.upoly.stateT]
bind [instance, in bedrock.upoly.traceT]
bind [instance, in bedrock.upoly.list]
bind [instance, in bedrock.upoly.listT]
bind [instance, in bedrock.upoly.writerT]
bind [instance, in bedrock.upoly.state]
bind [instance, in bedrock.upoly.id]
bind [instance, in bedrock.upoly.optionT]
bind [instance, in bedrock.upoly.writer]

C

catch [instance, in bedrock.upoly.option]
catch [instance, in bedrock.upoly.trace]
catch [instance, in bedrock.upoly.readerT]
catch [instance, in bedrock.upoly.stateT]
catch [instance, in bedrock.upoly.traceT]
catch [instance, in bedrock.upoly.list]
catch [instance, in bedrock.upoly.listT]
catch [instance, in bedrock.upoly.optionT]
catch' [instance, in bedrock.upoly.traceT]
catch' [instance, in bedrock.upoly.optionT]
char [definition, in bedrock.upoly.parsec]
charP [definition, in bedrock.upoly.parsec]
cons [constructor, in bedrock.upoly.UTypes]

D

default [definition, in bedrock.upoly.option]
default_params [instance, in bedrock.upoly.option]
drop [definition, in bedrock.upoly.list]

E

effects [library]
eos [definition, in bedrock.upoly.parsec]
epsilon [definition, in bedrock.upoly.parsec]
exact [definition, in bedrock.upoly.parsec]
exact_ [definition, in bedrock.upoly.parsec]

F

fail [instance, in bedrock.upoly.option]
fail [instance, in bedrock.upoly.trace]
fail [instance, in bedrock.upoly.readerT]
fail [instance, in bedrock.upoly.stateT]
fail [instance, in bedrock.upoly.traceT]
fail [instance, in bedrock.upoly.list]
fail [instance, in bedrock.upoly.listT]
fail [instance, in bedrock.upoly.optionT]
first [definition, in bedrock.upoly.base]
first [definition, in bedrock.upoly.prod]
FMap_M [instance, in bedrock.upoly.parsec]
foldl [definition, in bedrock.upoly.list]
foldr [definition, in bedrock.upoly.list]
force_map_ko [lemma, in bedrock.upoly.list]
force_map_ok [lemma, in bedrock.upoly.list]
force_app_correct [lemma, in bedrock.upoly.list]
force_app_dep_correct [lemma, in bedrock.upoly.list]
force_list_correct [lemma, in bedrock.upoly.list]
force_list_dep_correct [lemma, in bedrock.upoly.list]
force_map [definition, in bedrock.upoly.list]
force_app [definition, in bedrock.upoly.list]
force_app_dep [definition, in bedrock.upoly.list]
force_list [definition, in bedrock.upoly.list]
force_list_dep [definition, in bedrock.upoly.list]
from_option_params [instance, in bedrock.upoly.option]
from_option [definition, in bedrock.upoly.option]
fst [projection, in bedrock.upoly.UTypes]

G

get [definition, in bedrock.upoly.stateT]
get [definition, in bedrock.upoly.state]
gets [definition, in bedrock.upoly.stateT]
gets [definition, in bedrock.upoly.state]
getsM [definition, in bedrock.upoly.stateT]

I

id [library]
inj [definition, in bedrock.upoly.option]
inj [definition, in bedrock.upoly.sum]
inj [definition, in bedrock.upoly.list]
inj [definition, in bedrock.upoly.prod]
inl [constructor, in bedrock.upoly.UTypes]
inr [constructor, in bedrock.upoly.UTypes]

J

join [instance, in bedrock.upoly.option]
join [instance, in bedrock.upoly.trace]
join [instance, in bedrock.upoly.readerT]
join [instance, in bedrock.upoly.reader]
join [instance, in bedrock.upoly.stateT]
join [instance, in bedrock.upoly.traceT]
join [instance, in bedrock.upoly.list]
join [instance, in bedrock.upoly.listT]
join [instance, in bedrock.upoly.writerT]
join [instance, in bedrock.upoly.state]
join [instance, in bedrock.upoly.id]
join [instance, in bedrock.upoly.optionT]
join [instance, in bedrock.upoly.writer]

L

length [definition, in bedrock.upoly.list]
length_map [lemma, in bedrock.upoly.list]
lift [instance, in bedrock.upoly.readerT]
lift [instance, in bedrock.upoly.stateT]
lift [instance, in bedrock.upoly.traceT]
lift [instance, in bedrock.upoly.listT]
lift [instance, in bedrock.upoly.writerT]
lift [instance, in bedrock.upoly.optionT]
lift_option [instance, in bedrock.upoly.option]
lift_option [instance, in bedrock.upoly.trace]
lift_optionp [instance, in bedrock.upoly.trace]
lift_over [instance, in bedrock.upoly.readerT]
lift_reader [instance, in bedrock.upoly.stateT]
lift_over [instance, in bedrock.upoly.stateT]
lift_option [instance, in bedrock.upoly.traceT]
lift_optionp [instance, in bedrock.upoly.traceT]
lift_trace [instance, in bedrock.upoly.traceT]
lift_over [instance, in bedrock.upoly.traceT]
lift_option [instance, in bedrock.upoly.list]
lift_optionp [instance, in bedrock.upoly.list]
lift_list [instance, in bedrock.upoly.list]
lift_option [instance, in bedrock.upoly.listT]
lift_optionp [instance, in bedrock.upoly.listT]
lift_list [instance, in bedrock.upoly.listT]
lift_listp [instance, in bedrock.upoly.listT]
lift_over [instance, in bedrock.upoly.listT]
lift_option [instance, in bedrock.upoly.optionT]
lift_optionp [instance, in bedrock.upoly.optionT]
lift_over [instance, in bedrock.upoly.optionT]
list [inductive, in bedrock.upoly.UTypes]
list [section, in bedrock.upoly.list]
list [library]
listen [definition, in bedrock.upoly.writerT]
listen [definition, in bedrock.upoly.writer]
listT [section, in bedrock.upoly.listT]
listT [library]
listT.lift [section, in bedrock.upoly.listT]
listT.lift.m' [variable, in bedrock.upoly.listT]
listT.m [variable, in bedrock.upoly.listT]
list_sind [definition, in bedrock.upoly.UTypes]
list_rec [definition, in bedrock.upoly.UTypes]
list_ind [definition, in bedrock.upoly.UTypes]
list_rect [definition, in bedrock.upoly.UTypes]
list.A [variable, in bedrock.upoly.list]
local [definition, in bedrock.upoly.readerT]
local [definition, in bedrock.upoly.reader]
localM [definition, in bedrock.upoly.readerT]
lookup [instance, in bedrock.upoly.list]

M

M [abbreviation, in bedrock.upoly.trace]
M [inductive, in bedrock.upoly.trace]
M [abbreviation, in bedrock.upoly.readerT]
M [record, in bedrock.upoly.readerT]
M [abbreviation, in bedrock.upoly.reader]
M [record, in bedrock.upoly.reader]
M [abbreviation, in bedrock.upoly.stateT]
M [record, in bedrock.upoly.stateT]
M [abbreviation, in bedrock.upoly.traceT]
M [record, in bedrock.upoly.traceT]
M [abbreviation, in bedrock.upoly.listT]
M [record, in bedrock.upoly.listT]
M [abbreviation, in bedrock.upoly.writerT]
M [record, in bedrock.upoly.writerT]
M [abbreviation, in bedrock.upoly.state]
M [record, in bedrock.upoly.state]
M [definition, in bedrock.upoly.parsec]
M [record, in bedrock.upoly.id]
M [abbreviation, in bedrock.upoly.optionT]
M [record, in bedrock.upoly.optionT]
M [abbreviation, in bedrock.upoly.writer]
M [record, in bedrock.upoly.writer]
map [instance, in bedrock.upoly.option]
map [instance, in bedrock.upoly.trace]
map [instance, in bedrock.upoly.readerT]
map [instance, in bedrock.upoly.reader]
map [instance, in bedrock.upoly.stateT]
map [definition, in bedrock.upoly.sum]
map [section, in bedrock.upoly.sum]
map [instance, in bedrock.upoly.traceT]
map [instance, in bedrock.upoly.list]
map [definition, in bedrock.upoly.prod]
map [section, in bedrock.upoly.prod]
map [instance, in bedrock.upoly.listT]
map [instance, in bedrock.upoly.writerT]
map [instance, in bedrock.upoly.state]
map [instance, in bedrock.upoly.id]
map [instance, in bedrock.upoly.optionT]
map [instance, in bedrock.upoly.writer]
map_app [lemma, in bedrock.upoly.list]
map_id [lemma, in bedrock.upoly.list]
map_filter [definition, in bedrock.upoly.list]
map.A [variable, in bedrock.upoly.sum]
map.A [variable, in bedrock.upoly.prod]
map.A' [variable, in bedrock.upoly.sum]
map.A' [variable, in bedrock.upoly.prod]
map.B [variable, in bedrock.upoly.sum]
map.B [variable, in bedrock.upoly.prod]
map.B' [variable, in bedrock.upoly.sum]
map.B' [variable, in bedrock.upoly.prod]
MBind_M [instance, in bedrock.upoly.parsec]
MFail_M [instance, in bedrock.upoly.parsec]
MLift_M [instance, in bedrock.upoly.parsec]
modify [definition, in bedrock.upoly.stateT]
modify [definition, in bedrock.upoly.state]
modifyM [definition, in bedrock.upoly.stateT]
Monoid [record, in bedrock.upoly.monoid]
monoid [library]
monoid_op_params [instance, in bedrock.upoly.monoid]
monoid_unit_params [instance, in bedrock.upoly.monoid]
monoid_op [projection, in bedrock.upoly.monoid]
monoid_unit [projection, in bedrock.upoly.monoid]
MRet_M [instance, in bedrock.upoly.parsec]
M_Alternative [instance, in bedrock.upoly.parsec]

N

Next [record, in bedrock.upoly.parsec]
next_token [projection, in bedrock.upoly.parsec]
nil [constructor, in bedrock.upoly.UTypes]
None [constructor, in bedrock.upoly.UTypes]
not [definition, in bedrock.upoly.parsec]
Notations [module, in bedrock.upoly.sum]
Notations [module, in bedrock.upoly.list]
Notations [module, in bedrock.upoly.prod]
( _ , _ , .. , _ ) (core_scope) [notation, in bedrock.upoly.prod]
( _ ,.) (stdpp_scope) [notation, in bedrock.upoly.prod]
(., _ ) (stdpp_scope) [notation, in bedrock.upoly.prod]
_ + _ (type_scope) [notation, in bedrock.upoly.sum]
_ * _ (type_scope) [notation, in bedrock.upoly.prod]
_ ++ _ (ulist_scope) [notation, in bedrock.upoly.list]
[ _ ; _ ; .. ; _ ] (ulist_scope) [notation, in bedrock.upoly.list]
[ _ ] (ulist_scope) [notation, in bedrock.upoly.list]
[ ] (ulist_scope) [notation, in bedrock.upoly.list]
_ :: _ (ulist_scope) [notation, in bedrock.upoly.list]
_ .*2 [notation, in bedrock.upoly.prod]
_ .*1 [notation, in bedrock.upoly.prod]
_ .2 [notation, in bedrock.upoly.prod]
_ .1 [notation, in bedrock.upoly.prod]
nth_def [definition, in bedrock.upoly.list]

O

option [inductive, in bedrock.upoly.UTypes]
option [library]
optional [definition, in bedrock.upoly.parsec]
optionT [section, in bedrock.upoly.optionT]
optionT [library]
optionT.lift [section, in bedrock.upoly.optionT]
optionT.lift.m' [variable, in bedrock.upoly.optionT]
optionT.m [variable, in bedrock.upoly.optionT]
or [definition, in bedrock.upoly.parsec]

P

parsec [section, in bedrock.upoly.parsec]
parsec [library]
parsec.F [variable, in bedrock.upoly.parsec]
parsec.FM [variable, in bedrock.upoly.parsec]
parsec.MB [variable, in bedrock.upoly.parsec]
parsec.MR [variable, in bedrock.upoly.parsec]
parsec.N [variable, in bedrock.upoly.parsec]
parsec.P [variable, in bedrock.upoly.parsec]
ParseString [record, in bedrock.upoly.parsec]
parse_string [projection, in bedrock.upoly.parsec]
pass [definition, in bedrock.upoly.writerT]
pass [definition, in bedrock.upoly.writer]
peek [definition, in bedrock.upoly.parsec]
plus [definition, in bedrock.upoly.parsec]
prelude [library]
prod [record, in bedrock.upoly.UTypes]
prod [library]
put [definition, in bedrock.upoly.stateT]
put [definition, in bedrock.upoly.state]
putM [definition, in bedrock.upoly.stateT]

R

reader [section, in bedrock.upoly.reader]
reader [library]
readerT [section, in bedrock.upoly.readerT]
readerT [library]
readerT.errors [section, in bedrock.upoly.readerT]
readerT.errors.E [variable, in bedrock.upoly.readerT]
readerT.lift [section, in bedrock.upoly.readerT]
readerT.lift.m' [variable, in bedrock.upoly.readerT]
readerT.m [variable, in bedrock.upoly.readerT]
readerT.S [variable, in bedrock.upoly.readerT]
reader.S [variable, in bedrock.upoly.reader]
result [projection, in bedrock.upoly.writer]
ret [instance, in bedrock.upoly.option]
ret [instance, in bedrock.upoly.trace]
ret [instance, in bedrock.upoly.readerT]
ret [instance, in bedrock.upoly.reader]
ret [instance, in bedrock.upoly.stateT]
ret [instance, in bedrock.upoly.traceT]
ret [instance, in bedrock.upoly.list]
ret [instance, in bedrock.upoly.listT]
ret [instance, in bedrock.upoly.writerT]
ret [instance, in bedrock.upoly.state]
ret [instance, in bedrock.upoly.id]
ret [instance, in bedrock.upoly.optionT]
ret [instance, in bedrock.upoly.writer]
rev [definition, in bedrock.upoly.list]
rev_app [definition, in bedrock.upoly.list]
run [definition, in bedrock.upoly.option]
run [definition, in bedrock.upoly.trace]
run [projection, in bedrock.upoly.readerT]
run [projection, in bedrock.upoly.reader]
run [definition, in bedrock.upoly.stateT]
run [definition, in bedrock.upoly.sum]
run [definition, in bedrock.upoly.traceT]
run [definition, in bedrock.upoly.list]
run [definition, in bedrock.upoly.prod]
run [definition, in bedrock.upoly.listT]
run [definition, in bedrock.upoly.writerT]
run [definition, in bedrock.upoly.state]
run [definition, in bedrock.upoly.parsec]
run [projection, in bedrock.upoly.id]
run [definition, in bedrock.upoly.optionT]
run [definition, in bedrock.upoly.writer]
runO [definition, in bedrock.upoly.trace]
runO [definition, in bedrock.upoly.traceT]
runp [projection, in bedrock.upoly.stateT]
runp [projection, in bedrock.upoly.traceT]
runp [projection, in bedrock.upoly.listT]
runp [projection, in bedrock.upoly.writerT]
runp [projection, in bedrock.upoly.state]
runp [projection, in bedrock.upoly.optionT]
runp [definition, in bedrock.upoly.writer]
run_full [definition, in bedrock.upoly.parsec]

S

second [definition, in bedrock.upoly.base]
second [definition, in bedrock.upoly.prod]
select [definition, in bedrock.upoly.list]
sepBy [definition, in bedrock.upoly.parsec]
seqs [definition, in bedrock.upoly.parsec]
snd [projection, in bedrock.upoly.UTypes]
Some [constructor, in bedrock.upoly.UTypes]
star [definition, in bedrock.upoly.parsec]
star_ [definition, in bedrock.upoly.parsec]
state [definition, in bedrock.upoly.stateT]
state [definition, in bedrock.upoly.state]
state [section, in bedrock.upoly.state]
state [library]
stateM [definition, in bedrock.upoly.stateT]
stateT [section, in bedrock.upoly.stateT]
stateT [library]
stateT.errors [section, in bedrock.upoly.stateT]
stateT.errors.E [variable, in bedrock.upoly.stateT]
stateT.lift [section, in bedrock.upoly.stateT]
stateT.lift.m' [variable, in bedrock.upoly.stateT]
stateT.m [variable, in bedrock.upoly.stateT]
stateT.S [variable, in bedrock.upoly.stateT]
state.S [variable, in bedrock.upoly.state]
Success [constructor, in bedrock.upoly.trace]
sum [inductive, in bedrock.upoly.UTypes]
sum [library]

T

take [definition, in bedrock.upoly.list]
take_drop [lemma, in bedrock.upoly.list]
tell [definition, in bedrock.upoly.writerT]
tell [definition, in bedrock.upoly.writer]
throw [instance, in bedrock.upoly.trace]
throw [instance, in bedrock.upoly.readerT]
throw [instance, in bedrock.upoly.stateT]
throw [instance, in bedrock.upoly.traceT]
throw [instance, in bedrock.upoly.optionT]
throw' [instance, in bedrock.upoly.traceT]
trace [instance, in bedrock.upoly.trace]
trace [section, in bedrock.upoly.trace]
trace [instance, in bedrock.upoly.readerT]
trace [instance, in bedrock.upoly.stateT]
trace [instance, in bedrock.upoly.traceT]
trace [instance, in bedrock.upoly.optionT]
trace [library]
traceT [section, in bedrock.upoly.traceT]
traceT [library]
traceT.E [variable, in bedrock.upoly.traceT]
traceT.lift [section, in bedrock.upoly.traceT]
traceT.lift.m' [variable, in bedrock.upoly.traceT]
traceT.m [variable, in bedrock.upoly.traceT]
trace.E [variable, in bedrock.upoly.trace]
traverse [instance, in bedrock.upoly.option]
traverse [instance, in bedrock.upoly.trace]
traverse [definition, in bedrock.upoly.sum]
traverse [section, in bedrock.upoly.sum]
traverse [instance, in bedrock.upoly.list]
traverse [definition, in bedrock.upoly.prod]
traverse [section, in bedrock.upoly.prod]
traverse [instance, in bedrock.upoly.id]
traverse [instance, in bedrock.upoly.writer]
traverse.A [variable, in bedrock.upoly.sum]
traverse.A [variable, in bedrock.upoly.prod]
traverse.AP [variable, in bedrock.upoly.prod]
traverse.A' [variable, in bedrock.upoly.sum]
traverse.A' [variable, in bedrock.upoly.prod]
traverse.B [variable, in bedrock.upoly.sum]
traverse.B [variable, in bedrock.upoly.prod]
traverse.B' [variable, in bedrock.upoly.sum]
traverse.B' [variable, in bedrock.upoly.prod]
traverse.F [variable, in bedrock.upoly.sum]
traverse.F [variable, in bedrock.upoly.prod]

U

U [abbreviation, in bedrock.upoly.traceT]
UPoly [module, in bedrock.upoly.base]
upoly [library]
UPoly.alternative [projection, in bedrock.upoly.base]
UPoly.Alternative [record, in bedrock.upoly.base]
UPoly.alternative [constructor, in bedrock.upoly.base]
UPoly.Alternative [inductive, in bedrock.upoly.base]
UPoly.alternative_params [instance, in bedrock.upoly.base]
UPoly.ap [projection, in bedrock.upoly.base]
UPoly.Ap [record, in bedrock.upoly.base]
UPoly.ap [constructor, in bedrock.upoly.base]
UPoly.Ap [inductive, in bedrock.upoly.base]
UPoly.applicative_fmap [instance, in bedrock.upoly.base]
UPoly.bind_params [instance, in bedrock.upoly.base]
UPoly.catch_alternative [instance, in bedrock.upoly.base]
UPoly.compose [definition, in bedrock.upoly.base]
UPoly.const [abbreviation, in bedrock.upoly.base]
UPoly.const1 [abbreviation, in bedrock.upoly.base]
UPoly.const2 [abbreviation, in bedrock.upoly.base]
UPoly.const3 [abbreviation, in bedrock.upoly.base]
UPoly.const4 [abbreviation, in bedrock.upoly.base]
UPoly.const5 [abbreviation, in bedrock.upoly.base]
UPoly.const6 [abbreviation, in bedrock.upoly.base]
UPoly.const7 [abbreviation, in bedrock.upoly.base]
UPoly.eta [abbreviation, in bedrock.upoly.base]
UPoly.fmap [projection, in bedrock.upoly.base]
UPoly.FMap [record, in bedrock.upoly.base]
UPoly.fmap [constructor, in bedrock.upoly.base]
UPoly.FMap [inductive, in bedrock.upoly.base]
UPoly.fmap_params [instance, in bedrock.upoly.base]
UPoly.guard [abbreviation, in bedrock.upoly.base]
UPoly.guard_or_params [instance, in bedrock.upoly.base]
UPoly.guard_or [definition, in bedrock.upoly.base]
UPoly.id [abbreviation, in bedrock.upoly.base]
UPoly.join_params [instance, in bedrock.upoly.base]
UPoly.lift_params [instance, in bedrock.upoly.base]
UPoly.list_alternative [definition, in bedrock.upoly.base]
UPoly.list_catch [instance, in bedrock.upoly.base]
UPoly.list_fail [instance, in bedrock.upoly.base]
UPoly.list_traverse [instance, in bedrock.upoly.base]
UPoly.list_ap [definition, in bedrock.upoly.base]
UPoly.list_join [instance, in bedrock.upoly.base]
UPoly.list_bind [instance, in bedrock.upoly.base]
UPoly.list_ret [instance, in bedrock.upoly.base]
UPoly.list_fmap [instance, in bedrock.upoly.base]
UPoly.mbind [projection, in bedrock.upoly.base]
UPoly.MBind [record, in bedrock.upoly.base]
UPoly.mbind [constructor, in bedrock.upoly.base]
UPoly.MBind [inductive, in bedrock.upoly.base]
UPoly.mcatch [projection, in bedrock.upoly.base]
UPoly.MCatch [record, in bedrock.upoly.base]
UPoly.mcatch [constructor, in bedrock.upoly.base]
UPoly.MCatch [inductive, in bedrock.upoly.base]
UPoly.mcatch_params [instance, in bedrock.upoly.base]
UPoly.mfail [abbreviation, in bedrock.upoly.base]
UPoly.MFail [abbreviation, in bedrock.upoly.base]
UPoly.mjoin [projection, in bedrock.upoly.base]
UPoly.MJoin [record, in bedrock.upoly.base]
UPoly.mjoin [constructor, in bedrock.upoly.base]
UPoly.MJoin [inductive, in bedrock.upoly.base]
UPoly.mlift [projection, in bedrock.upoly.base]
UPoly.MLift [record, in bedrock.upoly.base]
UPoly.mlift [constructor, in bedrock.upoly.base]
UPoly.MLift [inductive, in bedrock.upoly.base]
UPoly.monad_ap [instance, in bedrock.upoly.base]
UPoly.monad_fmap [instance, in bedrock.upoly.base]
UPoly.mret [projection, in bedrock.upoly.base]
UPoly.MRet [record, in bedrock.upoly.base]
UPoly.mret [constructor, in bedrock.upoly.base]
UPoly.MRet [inductive, in bedrock.upoly.base]
UPoly.mthrow [projection, in bedrock.upoly.base]
UPoly.MThrow [record, in bedrock.upoly.base]
UPoly.mthrow [constructor, in bedrock.upoly.base]
UPoly.MThrow [inductive, in bedrock.upoly.base]
UPoly.mthrow_params [instance, in bedrock.upoly.base]
UPoly.Notations [module, in bedrock.upoly.base]
funM _ .. _ => _ (function_scope) [notation, in bedrock.upoly.base]
let* := _ in _ (monad_scope) [notation, in bedrock.upoly.base]
let* _ , .. , _ := _ in _ (monad_scope) [notation, in bedrock.upoly.base]
_ `catch` _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ ← _ ; _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ ;; _ (stdpp_scope) [notation, in bedrock.upoly.base]
(>>=) (stdpp_scope) [notation, in bedrock.upoly.base]
(.>>= _ ) (stdpp_scope) [notation, in bedrock.upoly.base]
( _ >>=.) (stdpp_scope) [notation, in bedrock.upoly.base]
_ >>=@{ _ } _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ >>= _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <|>@{ _ } _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <|> _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ *> _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <* _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <*>@{ _ } _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <*> _ (stdpp_scope) [notation, in bedrock.upoly.base]
_ <$> _ (stdpp_scope) [notation, in bedrock.upoly.base]
letM* := _ in _ (stdpp_scope) [notation, in bedrock.upoly.base]
letM* _ , .. , _ := _ in _ (stdpp_scope) [notation, in bedrock.upoly.base]
UPoly.option_alternative [definition, in bedrock.upoly.base]
UPoly.option_catch [instance, in bedrock.upoly.base]
UPoly.option_fail [instance, in bedrock.upoly.base]
UPoly.option_traverse [instance, in bedrock.upoly.base]
UPoly.option_ap [definition, in bedrock.upoly.base]
UPoly.option_join [instance, in bedrock.upoly.base]
UPoly.option_bind [instance, in bedrock.upoly.base]
UPoly.option_ret [instance, in bedrock.upoly.base]
UPoly.option_fmap [instance, in bedrock.upoly.base]
UPoly.pair_traverse_right [instance, in bedrock.upoly.base]
UPoly.prod_traverse [definition, in bedrock.upoly.base]
UPoly.prod_traverse.B' [variable, in bedrock.upoly.base]
UPoly.prod_traverse.A' [variable, in bedrock.upoly.base]
UPoly.prod_traverse.B [variable, in bedrock.upoly.base]
UPoly.prod_traverse.A [variable, in bedrock.upoly.base]
UPoly.prod_traverse.AP [variable, in bedrock.upoly.base]
UPoly.prod_traverse.F [variable, in bedrock.upoly.base]
UPoly.prod_traverse [section, in bedrock.upoly.base]
UPoly.prod_fmap [definition, in bedrock.upoly.base]
UPoly.prod_fmap.B' [variable, in bedrock.upoly.base]
UPoly.prod_fmap.A' [variable, in bedrock.upoly.base]
UPoly.prod_fmap.B [variable, in bedrock.upoly.base]
UPoly.prod_fmap.A [variable, in bedrock.upoly.base]
UPoly.prod_fmap [section, in bedrock.upoly.base]
UPoly.relation [abbreviation, in bedrock.upoly.base]
UPoly.ret_params [instance, in bedrock.upoly.base]
UPoly.sequence [abbreviation, in bedrock.upoly.base]
UPoly.sum_traverse_right [instance, in bedrock.upoly.base]
UPoly.sum_join_right [instance, in bedrock.upoly.base]
UPoly.sum_bind_right [instance, in bedrock.upoly.base]
UPoly.sum_fmap_right [instance, in bedrock.upoly.base]
UPoly.sum_ret_right [instance, in bedrock.upoly.base]
UPoly.sum_traverse [definition, in bedrock.upoly.base]
UPoly.sum_traverse.B' [variable, in bedrock.upoly.base]
UPoly.sum_traverse.A' [variable, in bedrock.upoly.base]
UPoly.sum_traverse.B [variable, in bedrock.upoly.base]
UPoly.sum_traverse.A [variable, in bedrock.upoly.base]
UPoly.sum_traverse.F [variable, in bedrock.upoly.base]
UPoly.sum_traverse [section, in bedrock.upoly.base]
UPoly.sum_fmap [definition, in bedrock.upoly.base]
UPoly.sum_fmap.B' [variable, in bedrock.upoly.base]
UPoly.sum_fmap.A' [variable, in bedrock.upoly.base]
UPoly.sum_fmap.B [variable, in bedrock.upoly.base]
UPoly.sum_fmap.A [variable, in bedrock.upoly.base]
UPoly.sum_fmap [section, in bedrock.upoly.base]
UPoly.trace [projection, in bedrock.upoly.base]
UPoly.Trace [record, in bedrock.upoly.base]
UPoly.trace [constructor, in bedrock.upoly.base]
UPoly.Trace [inductive, in bedrock.upoly.base]
UPoly.trace_params [instance, in bedrock.upoly.base]
UPoly.traverse [projection, in bedrock.upoly.base]
UPoly.Traverse [record, in bedrock.upoly.base]
UPoly.traverse [constructor, in bedrock.upoly.base]
UPoly.Traverse [inductive, in bedrock.upoly.base]
UPoly.traverse_params [instance, in bedrock.upoly.base]
_ \o _ (stdpp_scope) [notation, in bedrock.upoly.base]
sequence@{ _ } [notation, in bedrock.upoly.base]
UTypes [library]

V

value [projection, in bedrock.upoly.writer]

W

writer [definition, in bedrock.upoly.writerT]
writer [section, in bedrock.upoly.writerT]
writer [definition, in bedrock.upoly.writer]
writer [section, in bedrock.upoly.writer]
writer [library]
writerT [library]
writer.m [variable, in bedrock.upoly.writerT]
writer.V [variable, in bedrock.upoly.writerT]
writer.V [variable, in bedrock.upoly.writer]

Z

zip_with [definition, in bedrock.upoly.list]

---

Notation Index

N

( _ , _ , .. , _ ) (core_scope) [in bedrock.upoly.prod]
( _ ,.) (stdpp_scope) [in bedrock.upoly.prod]
(., _ ) (stdpp_scope) [in bedrock.upoly.prod]
_ + _ (type_scope) [in bedrock.upoly.sum]
_ * _ (type_scope) [in bedrock.upoly.prod]
_ ++ _ (ulist_scope) [in bedrock.upoly.list]
[ _ ; _ ; .. ; _ ] (ulist_scope) [in bedrock.upoly.list]
[ _ ] (ulist_scope) [in bedrock.upoly.list]
[ ] (ulist_scope) [in bedrock.upoly.list]
_ :: _ (ulist_scope) [in bedrock.upoly.list]
_ .*2 [in bedrock.upoly.prod]
_ .*1 [in bedrock.upoly.prod]
_ .2 [in bedrock.upoly.prod]
_ .1 [in bedrock.upoly.prod]

U

funM _ .. _ => _ (function_scope) [in bedrock.upoly.base]
let* := _ in _ (monad_scope) [in bedrock.upoly.base]
let* _ , .. , _ := _ in _ (monad_scope) [in bedrock.upoly.base]
_ `catch` _ (stdpp_scope) [in bedrock.upoly.base]
_ ← _ ; _ (stdpp_scope) [in bedrock.upoly.base]
_ ;; _ (stdpp_scope) [in bedrock.upoly.base]
(>>=) (stdpp_scope) [in bedrock.upoly.base]
(.>>= _ ) (stdpp_scope) [in bedrock.upoly.base]
( _ >>=.) (stdpp_scope) [in bedrock.upoly.base]
_ >>=@{ _ } _ (stdpp_scope) [in bedrock.upoly.base]
_ >>= _ (stdpp_scope) [in bedrock.upoly.base]
_ <|>@{ _ } _ (stdpp_scope) [in bedrock.upoly.base]
_ <|> _ (stdpp_scope) [in bedrock.upoly.base]
_ *> _ (stdpp_scope) [in bedrock.upoly.base]
_ <* _ (stdpp_scope) [in bedrock.upoly.base]
_ <*>@{ _ } _ (stdpp_scope) [in bedrock.upoly.base]
_ <*> _ (stdpp_scope) [in bedrock.upoly.base]
_ <$> _ (stdpp_scope) [in bedrock.upoly.base]
letM* := _ in _ (stdpp_scope) [in bedrock.upoly.base]
letM* _ , .. , _ := _ in _ (stdpp_scope) [in bedrock.upoly.base]
_ \o _ (stdpp_scope) [in bedrock.upoly.base]
sequence@{ _ } [in bedrock.upoly.base]

---

Module Index

N

Notations [in bedrock.upoly.sum]
Notations [in bedrock.upoly.list]
Notations [in bedrock.upoly.prod]

U

UPoly [in bedrock.upoly.base]
UPoly.Notations [in bedrock.upoly.base]

---

Variable Index

L

listT.lift.m' [in bedrock.upoly.listT]
listT.m [in bedrock.upoly.listT]
list.A [in bedrock.upoly.list]

M

map.A [in bedrock.upoly.sum]
map.A [in bedrock.upoly.prod]
map.A' [in bedrock.upoly.sum]
map.A' [in bedrock.upoly.prod]
map.B [in bedrock.upoly.sum]
map.B [in bedrock.upoly.prod]
map.B' [in bedrock.upoly.sum]
map.B' [in bedrock.upoly.prod]

O

optionT.lift.m' [in bedrock.upoly.optionT]
optionT.m [in bedrock.upoly.optionT]

P

parsec.F [in bedrock.upoly.parsec]
parsec.FM [in bedrock.upoly.parsec]
parsec.MB [in bedrock.upoly.parsec]
parsec.MR [in bedrock.upoly.parsec]
parsec.N [in bedrock.upoly.parsec]
parsec.P [in bedrock.upoly.parsec]

R

readerT.errors.E [in bedrock.upoly.readerT]
readerT.lift.m' [in bedrock.upoly.readerT]
readerT.m [in bedrock.upoly.readerT]
readerT.S [in bedrock.upoly.readerT]
reader.S [in bedrock.upoly.reader]

S

stateT.errors.E [in bedrock.upoly.stateT]
stateT.lift.m' [in bedrock.upoly.stateT]
stateT.m [in bedrock.upoly.stateT]
stateT.S [in bedrock.upoly.stateT]
state.S [in bedrock.upoly.state]

T

traceT.E [in bedrock.upoly.traceT]
traceT.lift.m' [in bedrock.upoly.traceT]
traceT.m [in bedrock.upoly.traceT]
trace.E [in bedrock.upoly.trace]
traverse.A [in bedrock.upoly.sum]
traverse.A [in bedrock.upoly.prod]
traverse.AP [in bedrock.upoly.prod]
traverse.A' [in bedrock.upoly.sum]
traverse.A' [in bedrock.upoly.prod]
traverse.B [in bedrock.upoly.sum]
traverse.B [in bedrock.upoly.prod]
traverse.B' [in bedrock.upoly.sum]
traverse.B' [in bedrock.upoly.prod]
traverse.F [in bedrock.upoly.sum]
traverse.F [in bedrock.upoly.prod]

U

UPoly.prod_traverse.B' [in bedrock.upoly.base]
UPoly.prod_traverse.A' [in bedrock.upoly.base]
UPoly.prod_traverse.B [in bedrock.upoly.base]
UPoly.prod_traverse.A [in bedrock.upoly.base]
UPoly.prod_traverse.AP [in bedrock.upoly.base]
UPoly.prod_traverse.F [in bedrock.upoly.base]
UPoly.prod_fmap.B' [in bedrock.upoly.base]
UPoly.prod_fmap.A' [in bedrock.upoly.base]
UPoly.prod_fmap.B [in bedrock.upoly.base]
UPoly.prod_fmap.A [in bedrock.upoly.base]
UPoly.sum_traverse.B' [in bedrock.upoly.base]
UPoly.sum_traverse.A' [in bedrock.upoly.base]
UPoly.sum_traverse.B [in bedrock.upoly.base]
UPoly.sum_traverse.A [in bedrock.upoly.base]
UPoly.sum_traverse.F [in bedrock.upoly.base]
UPoly.sum_fmap.B' [in bedrock.upoly.base]
UPoly.sum_fmap.A' [in bedrock.upoly.base]
UPoly.sum_fmap.B [in bedrock.upoly.base]
UPoly.sum_fmap.A [in bedrock.upoly.base]

W

writer.m [in bedrock.upoly.writerT]
writer.V [in bedrock.upoly.writerT]
writer.V [in bedrock.upoly.writer]

---

Library Index

B

base

E

effects

I

id

L

list
listT

M

monoid

O

option
optionT

P

parsec
prelude
prod

R

reader
readerT

S

state
stateT
sum

T

trace
traceT

U

upoly
UTypes

W

writer
writerT

---

Constructor Index

B

Backtrace [in bedrock.upoly.trace]

C

cons [in bedrock.upoly.UTypes]

I

inl [in bedrock.upoly.UTypes]
inr [in bedrock.upoly.UTypes]

N

nil [in bedrock.upoly.UTypes]
None [in bedrock.upoly.UTypes]

S

Some [in bedrock.upoly.UTypes]
Success [in bedrock.upoly.trace]

U

UPoly.alternative [in bedrock.upoly.base]
UPoly.ap [in bedrock.upoly.base]
UPoly.fmap [in bedrock.upoly.base]
UPoly.mbind [in bedrock.upoly.base]
UPoly.mcatch [in bedrock.upoly.base]
UPoly.mjoin [in bedrock.upoly.base]
UPoly.mlift [in bedrock.upoly.base]
UPoly.mret [in bedrock.upoly.base]
UPoly.mthrow [in bedrock.upoly.base]
UPoly.trace [in bedrock.upoly.base]
UPoly.traverse [in bedrock.upoly.base]

---

Lemma Index

F

force_map_ko [in bedrock.upoly.list]
force_map_ok [in bedrock.upoly.list]
force_app_correct [in bedrock.upoly.list]
force_app_dep_correct [in bedrock.upoly.list]
force_list_correct [in bedrock.upoly.list]
force_list_dep_correct [in bedrock.upoly.list]

L

length_map [in bedrock.upoly.list]

M

map_app [in bedrock.upoly.list]
map_id [in bedrock.upoly.list]

T

take_drop [in bedrock.upoly.list]

---

Projection Index

F

fst [in bedrock.upoly.UTypes]

M

monoid_op [in bedrock.upoly.monoid]
monoid_unit [in bedrock.upoly.monoid]

N

next_token [in bedrock.upoly.parsec]

P

parse_string [in bedrock.upoly.parsec]

R

result [in bedrock.upoly.writer]
run [in bedrock.upoly.readerT]
run [in bedrock.upoly.reader]
run [in bedrock.upoly.id]
runp [in bedrock.upoly.stateT]
runp [in bedrock.upoly.traceT]
runp [in bedrock.upoly.listT]
runp [in bedrock.upoly.writerT]
runp [in bedrock.upoly.state]
runp [in bedrock.upoly.optionT]

S

snd [in bedrock.upoly.UTypes]

U

UPoly.alternative [in bedrock.upoly.base]
UPoly.ap [in bedrock.upoly.base]
UPoly.fmap [in bedrock.upoly.base]
UPoly.mbind [in bedrock.upoly.base]
UPoly.mcatch [in bedrock.upoly.base]
UPoly.mjoin [in bedrock.upoly.base]
UPoly.mlift [in bedrock.upoly.base]
UPoly.mret [in bedrock.upoly.base]
UPoly.mthrow [in bedrock.upoly.base]
UPoly.trace [in bedrock.upoly.base]
UPoly.traverse [in bedrock.upoly.base]

V

value [in bedrock.upoly.writer]

---

Inductive Index

L

list [in bedrock.upoly.UTypes]

M

M [in bedrock.upoly.trace]

O

option [in bedrock.upoly.UTypes]

S

sum [in bedrock.upoly.UTypes]

U

UPoly.Alternative [in bedrock.upoly.base]
UPoly.Ap [in bedrock.upoly.base]
UPoly.FMap [in bedrock.upoly.base]
UPoly.MBind [in bedrock.upoly.base]
UPoly.MCatch [in bedrock.upoly.base]
UPoly.MJoin [in bedrock.upoly.base]
UPoly.MLift [in bedrock.upoly.base]
UPoly.MRet [in bedrock.upoly.base]
UPoly.MThrow [in bedrock.upoly.base]
UPoly.Trace [in bedrock.upoly.base]
UPoly.Traverse [in bedrock.upoly.base]

---

Instance Index

A

alternative [in bedrock.upoly.readerT]
alternative [in bedrock.upoly.stateT]
ap [in bedrock.upoly.readerT]
ap [in bedrock.upoly.reader]
ap [in bedrock.upoly.traceT]
ap [in bedrock.upoly.listT]
ap [in bedrock.upoly.writerT]
ap [in bedrock.upoly.optionT]
ap [in bedrock.upoly.writer]
Ap_M [in bedrock.upoly.parsec]

B

bind [in bedrock.upoly.option]
bind [in bedrock.upoly.trace]
bind [in bedrock.upoly.readerT]
bind [in bedrock.upoly.reader]
bind [in bedrock.upoly.stateT]
bind [in bedrock.upoly.traceT]
bind [in bedrock.upoly.list]
bind [in bedrock.upoly.listT]
bind [in bedrock.upoly.writerT]
bind [in bedrock.upoly.state]
bind [in bedrock.upoly.id]
bind [in bedrock.upoly.optionT]
bind [in bedrock.upoly.writer]

C

catch [in bedrock.upoly.option]
catch [in bedrock.upoly.trace]
catch [in bedrock.upoly.readerT]
catch [in bedrock.upoly.stateT]
catch [in bedrock.upoly.traceT]
catch [in bedrock.upoly.list]
catch [in bedrock.upoly.listT]
catch [in bedrock.upoly.optionT]
catch' [in bedrock.upoly.traceT]
catch' [in bedrock.upoly.optionT]

D

default_params [in bedrock.upoly.option]

F

fail [in bedrock.upoly.option]
fail [in bedrock.upoly.trace]
fail [in bedrock.upoly.readerT]
fail [in bedrock.upoly.stateT]
fail [in bedrock.upoly.traceT]
fail [in bedrock.upoly.list]
fail [in bedrock.upoly.listT]
fail [in bedrock.upoly.optionT]
FMap_M [in bedrock.upoly.parsec]
from_option_params [in bedrock.upoly.option]

J

join [in bedrock.upoly.option]
join [in bedrock.upoly.trace]
join [in bedrock.upoly.readerT]
join [in bedrock.upoly.reader]
join [in bedrock.upoly.stateT]
join [in bedrock.upoly.traceT]
join [in bedrock.upoly.list]
join [in bedrock.upoly.listT]
join [in bedrock.upoly.writerT]
join [in bedrock.upoly.state]
join [in bedrock.upoly.id]
join [in bedrock.upoly.optionT]
join [in bedrock.upoly.writer]

L

lift [in bedrock.upoly.readerT]
lift [in bedrock.upoly.stateT]
lift [in bedrock.upoly.traceT]
lift [in bedrock.upoly.listT]
lift [in bedrock.upoly.writerT]
lift [in bedrock.upoly.optionT]
lift_option [in bedrock.upoly.option]
lift_option [in bedrock.upoly.trace]
lift_optionp [in bedrock.upoly.trace]
lift_over [in bedrock.upoly.readerT]
lift_reader [in bedrock.upoly.stateT]
lift_over [in bedrock.upoly.stateT]
lift_option [in bedrock.upoly.traceT]
lift_optionp [in bedrock.upoly.traceT]
lift_trace [in bedrock.upoly.traceT]
lift_over [in bedrock.upoly.traceT]
lift_option [in bedrock.upoly.list]
lift_optionp [in bedrock.upoly.list]
lift_list [in bedrock.upoly.list]
lift_option [in bedrock.upoly.listT]
lift_optionp [in bedrock.upoly.listT]
lift_list [in bedrock.upoly.listT]
lift_listp [in bedrock.upoly.listT]
lift_over [in bedrock.upoly.listT]
lift_option [in bedrock.upoly.optionT]
lift_optionp [in bedrock.upoly.optionT]
lift_over [in bedrock.upoly.optionT]
lookup [in bedrock.upoly.list]

M

map [in bedrock.upoly.option]
map [in bedrock.upoly.trace]
map [in bedrock.upoly.readerT]
map [in bedrock.upoly.reader]
map [in bedrock.upoly.stateT]
map [in bedrock.upoly.traceT]
map [in bedrock.upoly.list]
map [in bedrock.upoly.listT]
map [in bedrock.upoly.writerT]
map [in bedrock.upoly.state]
map [in bedrock.upoly.id]
map [in bedrock.upoly.optionT]
map [in bedrock.upoly.writer]
MBind_M [in bedrock.upoly.parsec]
MFail_M [in bedrock.upoly.parsec]
MLift_M [in bedrock.upoly.parsec]
monoid_op_params [in bedrock.upoly.monoid]
monoid_unit_params [in bedrock.upoly.monoid]
MRet_M [in bedrock.upoly.parsec]
M_Alternative [in bedrock.upoly.parsec]

R

ret [in bedrock.upoly.option]
ret [in bedrock.upoly.trace]
ret [in bedrock.upoly.readerT]
ret [in bedrock.upoly.reader]
ret [in bedrock.upoly.stateT]
ret [in bedrock.upoly.traceT]
ret [in bedrock.upoly.list]
ret [in bedrock.upoly.listT]
ret [in bedrock.upoly.writerT]
ret [in bedrock.upoly.state]
ret [in bedrock.upoly.id]
ret [in bedrock.upoly.optionT]
ret [in bedrock.upoly.writer]

T

throw [in bedrock.upoly.trace]
throw [in bedrock.upoly.readerT]
throw [in bedrock.upoly.stateT]
throw [in bedrock.upoly.traceT]
throw [in bedrock.upoly.optionT]
throw' [in bedrock.upoly.traceT]
trace [in bedrock.upoly.trace]
trace [in bedrock.upoly.readerT]
trace [in bedrock.upoly.stateT]
trace [in bedrock.upoly.traceT]
trace [in bedrock.upoly.optionT]
traverse [in bedrock.upoly.option]
traverse [in bedrock.upoly.trace]
traverse [in bedrock.upoly.list]
traverse [in bedrock.upoly.id]
traverse [in bedrock.upoly.writer]

U

UPoly.alternative_params [in bedrock.upoly.base]
UPoly.applicative_fmap [in bedrock.upoly.base]
UPoly.bind_params [in bedrock.upoly.base]
UPoly.catch_alternative [in bedrock.upoly.base]
UPoly.fmap_params [in bedrock.upoly.base]
UPoly.guard_or_params [in bedrock.upoly.base]
UPoly.join_params [in bedrock.upoly.base]
UPoly.lift_params [in bedrock.upoly.base]
UPoly.list_catch [in bedrock.upoly.base]
UPoly.list_fail [in bedrock.upoly.base]
UPoly.list_traverse [in bedrock.upoly.base]
UPoly.list_join [in bedrock.upoly.base]
UPoly.list_bind [in bedrock.upoly.base]
UPoly.list_ret [in bedrock.upoly.base]
UPoly.list_fmap [in bedrock.upoly.base]
UPoly.mcatch_params [in bedrock.upoly.base]
UPoly.monad_ap [in bedrock.upoly.base]
UPoly.monad_fmap [in bedrock.upoly.base]
UPoly.mthrow_params [in bedrock.upoly.base]
UPoly.option_catch [in bedrock.upoly.base]
UPoly.option_fail [in bedrock.upoly.base]
UPoly.option_traverse [in bedrock.upoly.base]
UPoly.option_join [in bedrock.upoly.base]
UPoly.option_bind [in bedrock.upoly.base]
UPoly.option_ret [in bedrock.upoly.base]
UPoly.option_fmap [in bedrock.upoly.base]
UPoly.pair_traverse_right [in bedrock.upoly.base]
UPoly.ret_params [in bedrock.upoly.base]
UPoly.sum_traverse_right [in bedrock.upoly.base]
UPoly.sum_join_right [in bedrock.upoly.base]
UPoly.sum_bind_right [in bedrock.upoly.base]
UPoly.sum_fmap_right [in bedrock.upoly.base]
UPoly.sum_ret_right [in bedrock.upoly.base]
UPoly.trace_params [in bedrock.upoly.base]
UPoly.traverse_params [in bedrock.upoly.base]

---

Section Index

L

list [in bedrock.upoly.list]
listT [in bedrock.upoly.listT]
listT.lift [in bedrock.upoly.listT]

M

map [in bedrock.upoly.sum]
map [in bedrock.upoly.prod]

O

optionT [in bedrock.upoly.optionT]
optionT.lift [in bedrock.upoly.optionT]

P

parsec [in bedrock.upoly.parsec]

R

reader [in bedrock.upoly.reader]
readerT [in bedrock.upoly.readerT]
readerT.errors [in bedrock.upoly.readerT]
readerT.lift [in bedrock.upoly.readerT]

S

state [in bedrock.upoly.state]
stateT [in bedrock.upoly.stateT]
stateT.errors [in bedrock.upoly.stateT]
stateT.lift [in bedrock.upoly.stateT]

T

trace [in bedrock.upoly.trace]
traceT [in bedrock.upoly.traceT]
traceT.lift [in bedrock.upoly.traceT]
traverse [in bedrock.upoly.sum]
traverse [in bedrock.upoly.prod]

U

UPoly.prod_traverse [in bedrock.upoly.base]
UPoly.prod_fmap [in bedrock.upoly.base]
UPoly.sum_traverse [in bedrock.upoly.base]
UPoly.sum_fmap [in bedrock.upoly.base]

W

writer [in bedrock.upoly.writerT]
writer [in bedrock.upoly.writer]

---

Abbreviation Index

M

M [in bedrock.upoly.trace]
M [in bedrock.upoly.readerT]
M [in bedrock.upoly.reader]
M [in bedrock.upoly.stateT]
M [in bedrock.upoly.traceT]
M [in bedrock.upoly.listT]
M [in bedrock.upoly.writerT]
M [in bedrock.upoly.state]
M [in bedrock.upoly.optionT]
M [in bedrock.upoly.writer]

U

U [in bedrock.upoly.traceT]
UPoly.const [in bedrock.upoly.base]
UPoly.const1 [in bedrock.upoly.base]
UPoly.const2 [in bedrock.upoly.base]
UPoly.const3 [in bedrock.upoly.base]
UPoly.const4 [in bedrock.upoly.base]
UPoly.const5 [in bedrock.upoly.base]
UPoly.const6 [in bedrock.upoly.base]
UPoly.const7 [in bedrock.upoly.base]
UPoly.eta [in bedrock.upoly.base]
UPoly.guard [in bedrock.upoly.base]
UPoly.id [in bedrock.upoly.base]
UPoly.mfail [in bedrock.upoly.base]
UPoly.MFail [in bedrock.upoly.base]
UPoly.relation [in bedrock.upoly.base]
UPoly.sequence [in bedrock.upoly.base]

---

Record Index

M

M [in bedrock.upoly.readerT]
M [in bedrock.upoly.reader]
M [in bedrock.upoly.stateT]
M [in bedrock.upoly.traceT]
M [in bedrock.upoly.listT]
M [in bedrock.upoly.writerT]
M [in bedrock.upoly.state]
M [in bedrock.upoly.id]
M [in bedrock.upoly.optionT]
M [in bedrock.upoly.writer]
Monoid [in bedrock.upoly.monoid]

N

Next [in bedrock.upoly.parsec]

P

ParseString [in bedrock.upoly.parsec]
prod [in bedrock.upoly.UTypes]

U

UPoly.Alternative [in bedrock.upoly.base]
UPoly.Ap [in bedrock.upoly.base]
UPoly.FMap [in bedrock.upoly.base]
UPoly.MBind [in bedrock.upoly.base]
UPoly.MCatch [in bedrock.upoly.base]
UPoly.MJoin [in bedrock.upoly.base]
UPoly.MLift [in bedrock.upoly.base]
UPoly.MRet [in bedrock.upoly.base]
UPoly.MThrow [in bedrock.upoly.base]
UPoly.Trace [in bedrock.upoly.base]
UPoly.Traverse [in bedrock.upoly.base]

---

Definition Index

A

alternative [in bedrock.upoly.option]
alternative [in bedrock.upoly.trace]
alternative [in bedrock.upoly.traceT]
alternative [in bedrock.upoly.list]
alternative [in bedrock.upoly.listT]
alternative [in bedrock.upoly.optionT]
alternative_not_lazy [in bedrock.upoly.traceT]
alternative_not_lazy [in bedrock.upoly.listT]
alternative_not_lazy [in bedrock.upoly.optionT]
any [in bedrock.upoly.parsec]
anyOf [in bedrock.upoly.parsec]
ap [in bedrock.upoly.option]
ap [in bedrock.upoly.trace]
ap [in bedrock.upoly.stateT]
ap [in bedrock.upoly.list]
ap [in bedrock.upoly.state]
ap [in bedrock.upoly.id]
app [in bedrock.upoly.list]
app' [in bedrock.upoly.list]
ask [in bedrock.upoly.readerT]
ask [in bedrock.upoly.reader]
asks [in bedrock.upoly.readerT]
asks [in bedrock.upoly.reader]
asksM [in bedrock.upoly.readerT]

C

char [in bedrock.upoly.parsec]
charP [in bedrock.upoly.parsec]

D

default [in bedrock.upoly.option]
drop [in bedrock.upoly.list]

E

eos [in bedrock.upoly.parsec]
epsilon [in bedrock.upoly.parsec]
exact [in bedrock.upoly.parsec]
exact_ [in bedrock.upoly.parsec]

F

first [in bedrock.upoly.base]
first [in bedrock.upoly.prod]
foldl [in bedrock.upoly.list]
foldr [in bedrock.upoly.list]
force_map [in bedrock.upoly.list]
force_app [in bedrock.upoly.list]
force_app_dep [in bedrock.upoly.list]
force_list [in bedrock.upoly.list]
force_list_dep [in bedrock.upoly.list]
from_option [in bedrock.upoly.option]

G

get [in bedrock.upoly.stateT]
get [in bedrock.upoly.state]
gets [in bedrock.upoly.stateT]
gets [in bedrock.upoly.state]
getsM [in bedrock.upoly.stateT]

I

inj [in bedrock.upoly.option]
inj [in bedrock.upoly.sum]
inj [in bedrock.upoly.list]
inj [in bedrock.upoly.prod]

L

length [in bedrock.upoly.list]
listen [in bedrock.upoly.writerT]
listen [in bedrock.upoly.writer]
list_sind [in bedrock.upoly.UTypes]
list_rec [in bedrock.upoly.UTypes]
list_ind [in bedrock.upoly.UTypes]
list_rect [in bedrock.upoly.UTypes]
local [in bedrock.upoly.readerT]
local [in bedrock.upoly.reader]
localM [in bedrock.upoly.readerT]

M

M [in bedrock.upoly.parsec]
map [in bedrock.upoly.sum]
map [in bedrock.upoly.prod]
map_filter [in bedrock.upoly.list]
modify [in bedrock.upoly.stateT]
modify [in bedrock.upoly.state]
modifyM [in bedrock.upoly.stateT]

N

not [in bedrock.upoly.parsec]
nth_def [in bedrock.upoly.list]

O

optional [in bedrock.upoly.parsec]
or [in bedrock.upoly.parsec]

P

pass [in bedrock.upoly.writerT]
pass [in bedrock.upoly.writer]
peek [in bedrock.upoly.parsec]
plus [in bedrock.upoly.parsec]
put [in bedrock.upoly.stateT]
put [in bedrock.upoly.state]
putM [in bedrock.upoly.stateT]

R

rev [in bedrock.upoly.list]
rev_app [in bedrock.upoly.list]
run [in bedrock.upoly.option]
run [in bedrock.upoly.trace]
run [in bedrock.upoly.stateT]
run [in bedrock.upoly.sum]
run [in bedrock.upoly.traceT]
run [in bedrock.upoly.list]
run [in bedrock.upoly.prod]
run [in bedrock.upoly.listT]
run [in bedrock.upoly.writerT]
run [in bedrock.upoly.state]
run [in bedrock.upoly.parsec]
run [in bedrock.upoly.optionT]
run [in bedrock.upoly.writer]
runO [in bedrock.upoly.trace]
runO [in bedrock.upoly.traceT]
runp [in bedrock.upoly.writer]
run_full [in bedrock.upoly.parsec]

S

second [in bedrock.upoly.base]
second [in bedrock.upoly.prod]
select [in bedrock.upoly.list]
sepBy [in bedrock.upoly.parsec]
seqs [in bedrock.upoly.parsec]
star [in bedrock.upoly.parsec]
star_ [in bedrock.upoly.parsec]
state [in bedrock.upoly.stateT]
state [in bedrock.upoly.state]
stateM [in bedrock.upoly.stateT]

T

take [in bedrock.upoly.list]
tell [in bedrock.upoly.writerT]
tell [in bedrock.upoly.writer]
traverse [in bedrock.upoly.sum]
traverse [in bedrock.upoly.prod]

U

UPoly.compose [in bedrock.upoly.base]
UPoly.guard_or [in bedrock.upoly.base]
UPoly.list_alternative [in bedrock.upoly.base]
UPoly.list_ap [in bedrock.upoly.base]
UPoly.option_alternative [in bedrock.upoly.base]
UPoly.option_ap [in bedrock.upoly.base]
UPoly.prod_traverse [in bedrock.upoly.base]
UPoly.prod_fmap [in bedrock.upoly.base]
UPoly.sum_traverse [in bedrock.upoly.base]
UPoly.sum_fmap [in bedrock.upoly.base]

W

writer [in bedrock.upoly.writerT]
writer [in bedrock.upoly.writer]

Z

zip_with [in bedrock.upoly.list]

---

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

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

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

(5 entries)

Variable 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

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

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

(19 entries)

Lemma 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

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

(15 entries)

Instance 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

(169 entries)

Section 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

(27 entries)

Abbreviation 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

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

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

(126 entries)

Generated by coqdoc and improved with CoqdocJS