Global Index

J

Q

X

Y

_

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

_

(29 entries)

Module Index

D

F

G

H

J

K

L

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(14 entries)

Variable Index

G

I

J

K

L

N

O

Q

R

U

V

W

X

Y

_

other

(133 entries)

Library Index

D

G

H

I

J

K

M

N

Q

V

X

Y

Z

_

other

(42 entries)

Axiom Index

A

B

D

E

G

H

J

N

O

P

Q

R

V

W

X

Y

_

other

(17 entries)

Lemma Index

J

K

O

Q

V

X

Y

_

other

(214 entries)

Constructor Index

D

F

G

H

I

J

K

L

N

O

P

Q

T

V

W

X

Y

Z

_

other

(11 entries)

Projection Index

B

C

D

E

G

H

I

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(4 entries)

Section Index

G

I

J

K

L

N

O

Q

R

U

V

W

X

Y

_

other

(45 entries)

Definition Index

G

J

K

Q

X

Y

_

other

(265 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Global Index

A

accept [definition, in regexp.synthesis]
accept [definition, in regexp.abstract.automata]
accept [definition, in regexp.concrete.automata.simulation]
accept [definition, in regexp.abstract.automata.simulation]
accept [definition, in regexp.concrete.automata]
accept [definition, in regexp.synthesis.clash.automata]
accept_app [lemma, in regexp.abstract.automata.oneOrMore]
accept_cover [lemma, in regexp.abstract.automata.oneOrMore]
accept_one [lemma, in regexp.abstract.automata.oneOrMore]
accept_concat [lemma, in regexp.abstract.automata.concat]
accept_nil [lemma, in regexp.abstract.automata.concat]
access [module, in regexp.abstract.automata.path]
access.cons [definition, in regexp.abstract.automata.path]
access.Cxt [section, in regexp.abstract.automata.path]
access.Cxt.B [variable, in regexp.abstract.automata.path]
access.Cxt.St [variable, in regexp.abstract.automata.path]
access.Cxt.tr [variable, in regexp.abstract.automata.path]
access.from [definition, in regexp.abstract.automata.path]
access.fromsub [lemma, in regexp.abstract.automata.path]
access.fromU [lemma, in regexp.abstract.automata.path]
access.single_from [definition, in regexp.abstract.automata.path]
access.single_to [definition, in regexp.abstract.automata.path]
access.to [definition, in regexp.abstract.automata.path]
access.tosub [lemma, in regexp.abstract.automata.path]
access.toU [lemma, in regexp.abstract.automata.path]
alphabet [definition, in regexp.syn]
alt [definition, in regexp.lang]
alt [constructor, in regexp.expr]
alt [library]
alt [library]
and [definition, in regexp.concrete.relation]
andC [definition, in regexp.synthesis.clash.constraint]
any [definition, in regexp.byte]
atomTable [projection, in regexp.concrete.rule]
attach [definition, in regexp.syn]
automata [library]
automata [library]
automata [library]
automata_NFA__canonical__eqtype_Equality [definition, in regexp.abstract.automata]
axioms [library]

B

backward [lemma, in regexp.abstract.automata.oneOrMore]
between [definition, in regexp.byte]
big [module, in regexp.synthesis.clash.subset]
big [module, in regexp.concrete.subset]
bigStartBackU [lemma, in regexp.abstract.automata.oneOrMore]
BigSyn [section, in regexp.synthesis.clash.subset]
BigSyn.f [variable, in regexp.synthesis.clash.subset]
BigSyn.idx [variable, in regexp.synthesis.clash.subset]
BigSyn.s [variable, in regexp.synthesis.clash.subset]
bigunion_spec [lemma, in regexp.synthesis.clash.subset]
big.bigcap_sum [lemma, in regexp.concrete.subset]
big.bigcup_sum [lemma, in regexp.concrete.subset]
big.Cxt [section, in regexp.synthesis.clash.subset]
big.Cxt [section, in regexp.concrete.subset]
big.Cxt.F [variable, in regexp.concrete.subset]
big.Cxt.idx [variable, in regexp.synthesis.clash.subset]
big.Cxt.idx [variable, in regexp.concrete.subset]
big.Cxt.s [variable, in regexp.synthesis.clash.subset]
big.Cxt.s [variable, in regexp.concrete.subset]
big.intersection [definition, in regexp.synthesis.clash.subset]
big.intersection [definition, in regexp.concrete.subset]
big.intersection_spec [lemma, in regexp.concrete.subset]
big.union [definition, in regexp.synthesis.clash.subset]
big.union [definition, in regexp.concrete.subset]
big.union_spec [lemma, in regexp.concrete.subset]
binary [module, in regexp.concrete.relation]
binary [module, in regexp.abstract.relation]
binary [module, in regexp.synthesis.clash.relation]
binary.img [definition, in regexp.synthesis.clash.relation]
binary.t [definition, in regexp.concrete.relation]
binary.t [definition, in regexp.abstract.relation]
binary.t [definition, in regexp.synthesis.clash.relation]
Bind [constructor, in regexp.syn]
build [definition, in regexp.abstract.automata.singleton]
build [definition, in regexp.concrete.automata.concat]
build [definition, in regexp.concrete.automata.singleton]
build [definition, in regexp.abstract.automata.alt]
build [definition, in regexp.abstract.automata.epsilon]
build [definition, in regexp.abstract.automata.oneOrMore]
build [definition, in regexp.concrete.automata.alt]
Build [section, in regexp.concrete.automata.alt]
build [definition, in regexp.concrete.automata.oneOrMore]
build [definition, in regexp.concrete.automata.epsilon]
build [definition, in regexp.abstract.automata.concat]
build [library]
build [library]
Build.B [variable, in regexp.concrete.automata.alt]
Build.mac0 [variable, in regexp.concrete.automata.alt]
Build.mac1 [variable, in regexp.concrete.automata.alt]
Build.St0 [variable, in regexp.concrete.automata.alt]
Build.St1 [variable, in regexp.concrete.automata.alt]
byte [library]

C

char [definition, in regexp.byte]
Comap [section, in regexp.lang]
comap [definition, in regexp.lang]
comap_comap [lemma, in regexp.lang]
comap_many1 [lemma, in regexp.lang]
comap_pow [lemma, in regexp.lang]
comap_concat [lemma, in regexp.lang]
comap_satisfy [lemma, in regexp.lang]
comap_alt [lemma, in regexp.lang]
comap_epsilon [lemma, in regexp.lang]
Comap.A [variable, in regexp.lang]
Comap.B [variable, in regexp.lang]
Comap.f [variable, in regexp.lang]
compile [definition, in regexp.syn]
compose [definition, in regexp.concrete.relation]
composeP [lemma, in regexp.concrete.relation]
concat [constructor, in regexp.concrete.function]
concat [axiom, in regexp.synthesis.clash.function]
concat [definition, in regexp.lang]
concat [lemma, in regexp.abstract.automata.path]
concat [constructor, in regexp.expr]
concat [library]
concat [library]
concat_epsilon [lemma, in regexp.lang]
concat_accept [lemma, in regexp.abstract.automata.concat]
consistent [module, in regexp.lang.world]
consistent.concat [lemma, in regexp.lang.world]
consistent.left [module, in regexp.lang.world]
consistent.left.consP [lemma, in regexp.lang.world]
consistent.left.Cxt [section, in regexp.lang.world]
consistent.left.Cxt.B [variable, in regexp.lang.world]
consistent.left.nilE [lemma, in regexp.lang.world]
consistent.rel [definition, in regexp.lang.world]
consistent.right [module, in regexp.lang.world]
consistent.right.concat [lemma, in regexp.lang.world]
consistent.right.consP [lemma, in regexp.lang.world]
consistent.right.Cxt [section, in regexp.lang.world]
consistent.right.Cxt.B [variable, in regexp.lang.world]
consistent.right.nilE [lemma, in regexp.lang.world]
consistent.right.singletonP [lemma, in regexp.lang.world]
consP [lemma, in regexp.abstract.automata.path]
const [constructor, in regexp.concrete.function]
constant [definition, in regexp.concrete.function]
constant [axiom, in regexp.synthesis.clash.function]
constantE [lemma, in regexp.concrete.function]
constant_spec [axiom, in regexp.synthesis.clash.axioms]
constraint [library]
consume [definition, in regexp.concrete.automata.simulation]
consume [definition, in regexp.abstract.automata.simulation]
consume [definition, in regexp.synthesis.clash.automata]
consume_spec [lemma, in regexp.concrete.automata.simulation]
consume_spec [lemma, in regexp.synthesis.clash.automata]
CoProd [axiom, in regexp.synthesis.clash.universe]
CoProd [constructor, in regexp.concrete.universe]
correctness [lemma, in regexp.abstract.automata.singleton]
correctness [lemma, in regexp.concrete.automata.concat]
correctness [lemma, in regexp.synthesis]
Correctness [section, in regexp.synthesis]
correctness [lemma, in regexp.concrete.automata.singleton]
correctness [lemma, in regexp.concrete.automata.simulation]
correctness [lemma, in regexp.abstract.automata.build]
correctness [lemma, in regexp.abstract.automata.alt]
correctness [lemma, in regexp.abstract.automata.epsilon]
correctness [lemma, in regexp.abstract.automata.simulation]
correctness [lemma, in regexp.abstract.automata.oneOrMore]
correctness [lemma, in regexp.concrete.automata.alt]
correctness [lemma, in regexp.concrete.automata.oneOrMore]
correctness [lemma, in regexp.concrete.automata.epsilon]
correctness [lemma, in regexp.concrete.automata.build]
correctness [lemma, in regexp.synthesis.clash.automata]
correctness [lemma, in regexp.abstract.automata.concat]
Correctness.I [variable, in regexp.synthesis]
Correctness.rls [variable, in regexp.synthesis]
cover [definition, in regexp.abstract.automata.path]
coverLRE [lemma, in regexp.abstract.automata.concat]
cover_subR [lemma, in regexp.abstract.automata.path]
cover_supL [lemma, in regexp.abstract.automata.path]
cover_concat [lemma, in regexp.abstract.automata.path]
cover_nil [lemma, in regexp.abstract.automata.path]
cover_start1 [lemma, in regexp.abstract.automata.concat]
crossing [definition, in regexp.concrete.automata.concat]
crossRel [definition, in regexp.concrete.automata.concat]
Cxt [section, in regexp.concrete.automata.concat]
Cxt [section, in regexp.abstract.utils]
Cxt [section, in regexp.abstract.automata.build]
Cxt [section, in regexp.abstract.automata.alt]
Cxt [section, in regexp.abstract.automata.oneOrMore]
Cxt [section, in regexp.concrete.automata.alt]
Cxt [section, in regexp.abstract.automata.path]
Cxt [section, in regexp.concrete.automata.oneOrMore]
Cxt [section, in regexp.concrete.automata.build]
Cxt [section, in regexp.concrete.rule]
Cxt [section, in regexp.concrete.rule]
Cxt [section, in regexp.abstract.automata.concat]
Cxt.aT [variable, in regexp.concrete.rule]
Cxt.aT [variable, in regexp.concrete.rule]
Cxt.B [variable, in regexp.concrete.automata.concat]
Cxt.B [variable, in regexp.abstract.automata.build]
Cxt.B [variable, in regexp.abstract.automata.alt]
Cxt.B [variable, in regexp.abstract.automata.oneOrMore]
Cxt.B [variable, in regexp.concrete.automata.alt]
Cxt.B [variable, in regexp.abstract.automata.path]
Cxt.B [variable, in regexp.concrete.automata.oneOrMore]
Cxt.B [variable, in regexp.concrete.automata.build]
Cxt.B [variable, in regexp.abstract.automata.concat]
Cxt.I [variable, in regexp.concrete.rule]
Cxt.I [variable, in regexp.concrete.rule]
Cxt.mac [variable, in regexp.abstract.automata.oneOrMore]
Cxt.mac [variable, in regexp.concrete.automata.oneOrMore]
Cxt.mac0 [variable, in regexp.concrete.automata.concat]
Cxt.mac0 [variable, in regexp.abstract.automata.alt]
Cxt.mac0 [variable, in regexp.abstract.automata.concat]
Cxt.mac1 [variable, in regexp.concrete.automata.concat]
Cxt.mac1 [variable, in regexp.abstract.automata.alt]
Cxt.mac1 [variable, in regexp.abstract.automata.concat]
Cxt.s [variable, in regexp.concrete.rule]
Cxt.s [variable, in regexp.concrete.rule]
Cxt.St [variable, in regexp.abstract.automata.oneOrMore]
Cxt.St [variable, in regexp.abstract.automata.path]
Cxt.St [variable, in regexp.concrete.automata.oneOrMore]
Cxt.St0 [variable, in regexp.concrete.automata.concat]
Cxt.St0 [variable, in regexp.abstract.utils]
Cxt.St0 [variable, in regexp.abstract.automata.alt]
Cxt.St0 [variable, in regexp.concrete.automata.alt]
Cxt.St0 [variable, in regexp.abstract.automata.concat]
Cxt.St1 [variable, in regexp.concrete.automata.concat]
Cxt.St1 [variable, in regexp.abstract.utils]
Cxt.St1 [variable, in regexp.abstract.automata.alt]
Cxt.St1 [variable, in regexp.concrete.automata.alt]
Cxt.St1 [variable, in regexp.abstract.automata.concat]
Cxt.tr [variable, in regexp.abstract.automata.path]
Cxt.tr0 [variable, in regexp.concrete.automata.alt]
Cxt.tr1 [variable, in regexp.concrete.automata.alt]

D

deadEnd [definition, in regexp.abstract.automata.path]
DecEq [section, in regexp.abstract.automata]
DecEq.B [variable, in regexp.abstract.automata]
DecEq.St [variable, in regexp.abstract.automata]
Defn [section, in regexp.synthesis.clash.automata]
Defn.b [variable, in regexp.synthesis.clash.automata]
Defn.s [variable, in regexp.synthesis.clash.automata]
denote [definition, in regexp.concrete.relation]
denote [definition, in regexp.concrete.function]
denote [definition, in regexp.concrete.subset]
denote [definition, in regexp.syn]
denote [definition, in regexp.concrete.universe]
denote [definition, in regexp.concrete.automata]
denoteE [lemma, in regexp.concrete.function]
denoteE [lemma, in regexp.concrete.subset]
diagonal [definition, in regexp.concrete.relation]
diagonal [definition, in regexp.abstract.automata.transition]
diagonal [definition, in regexp.abstract.relation]
diagonal_spec [lemma, in regexp.concrete.relation]
diagonal_matrix [lemma, in regexp.abstract.relation]
disjoint_union [definition, in regexp.synthesis.clash.subset]
disjoint_union [definition, in regexp.concrete.subset]
disjULE [lemma, in regexp.concrete.subset]
disjURE [lemma, in regexp.concrete.subset]
disUUU [lemma, in regexp.concrete.subset]

E

empty [definition, in regexp.concrete.relation]
empty [definition, in regexp.synthesis.clash.subset]
empty [definition, in regexp.concrete.subset]
empty [definition, in regexp.abstract.relation]
emptyE [lemma, in regexp.abstract.relation]
emptyPath [lemma, in regexp.abstract.automata.epsilon]
emptyRel [definition, in regexp.concrete.automata.singleton]
empty_spec [lemma, in regexp.concrete.relation]
empty_spec [lemma, in regexp.synthesis.clash.subset]
empty_spec [lemma, in regexp.concrete.subset]
encode [definition, in regexp.concrete.rule]
eps [constructor, in regexp.expr]
epsilon [definition, in regexp.lang]
Epsilon [section, in regexp.concrete.automata.epsilon]
epsilon [library]
epsilon [library]
epsilon_concat [lemma, in regexp.lang]
Epsilon.B [variable, in regexp.concrete.automata.epsilon]
eq [module, in regexp.lang]
EqFun [section, in regexp.prelude]
eqfun_trans [lemma, in regexp.prelude]
eqfun_sym [lemma, in regexp.prelude]
eqfun_refl [lemma, in regexp.prelude]
EqFun.A [variable, in regexp.prelude]
EqFun.B [variable, in regexp.prelude]
eqnfa [definition, in regexp.abstract.automata]
eqnfaP [lemma, in regexp.abstract.automata]
equality [lemma, in regexp.concrete.automata.concat]
equality [lemma, in regexp.concrete.automata.singleton]
equality [lemma, in regexp.concrete.automata.alt]
equality [lemma, in regexp.concrete.automata.oneOrMore]
equality [lemma, in regexp.concrete.automata.epsilon]
equiv [definition, in regexp.abstract.automata]
Equiv [section, in regexp.abstract.automata]
equivalence [lemma, in regexp.concrete.rule]
Equiv.B [variable, in regexp.abstract.automata]
Equiv.St [variable, in regexp.abstract.automata]
eq_equiv [lemma, in regexp.abstract.automata]
eq.Cxt [section, in regexp.lang]
eq.Cxt.A [variable, in regexp.lang]
eq.refl [lemma, in regexp.lang]
eq.rel [definition, in regexp.lang]
eq.sym [lemma, in regexp.lang]
eq.trans [lemma, in regexp.lang]
eval [definition, in regexp.expr]
expr [library]
extensionality [lemma, in regexp.concrete.function]

F

fill [definition, in regexp.syn]
filled [definition, in regexp.syn]
final [projection, in regexp.abstract.automata]
final [projection, in regexp.concrete.automata]
final [projection, in regexp.synthesis.clash.automata]
final0 [definition, in regexp.concrete.automata.concat]
final0 [definition, in regexp.abstract.automata.concat]
final1 [definition, in regexp.concrete.automata.concat]
final1 [definition, in regexp.abstract.automata.concat]
fold [definition, in regexp.concrete.function]
fold [axiom, in regexp.synthesis.clash.function]
foldl_map [lemma, in regexp.prelude]
FoldMap [section, in regexp.concrete.function]
FoldMap.A [variable, in regexp.concrete.function]
FoldMap.B [variable, in regexp.concrete.function]
FoldMap.conv [variable, in regexp.concrete.function]
FoldMap.f [variable, in regexp.concrete.function]
FoldMap.g [variable, in regexp.concrete.function]
FoldMap.Hconv [variable, in regexp.concrete.function]
fold_spec [axiom, in regexp.synthesis.clash.axioms]
fold_map [lemma, in regexp.concrete.function]
foo [definition, in regexp.syn]
forward [lemma, in regexp.abstract.automata.oneOrMore]
from [definition, in regexp.concrete.function]
fromeq [lemma, in regexp.concrete.function]
from_to [lemma, in regexp.concrete.function]
full [definition, in regexp.concrete.relation]
full [definition, in regexp.synthesis.clash.subset]
full [definition, in regexp.concrete.subset]
full [definition, in regexp.abstract.relation]
full_spec [lemma, in regexp.concrete.relation]
full_spec [lemma, in regexp.concrete.subset]
function [library]
function [library]

G

graded_reachability [lemma, in regexp.abstract.automata.oneOrMore]

H

hasfinal0 [definition, in regexp.concrete.automata.concat]
hasfinal0 [definition, in regexp.abstract.automata.concat]
hasfinal0_denote [lemma, in regexp.concrete.automata.concat]
hb_instance_1.St [variable, in regexp.abstract.automata]
hb_instance_1.B [variable, in regexp.abstract.automata]
hb_instance_1.hb_instance_1 [section, in regexp.abstract.automata]

I

ifeq [definition, in regexp.concrete.function]
ifeq_spec [lemma, in regexp.concrete.function]
iLanguage [definition, in regexp.concrete.rule]
img [definition, in regexp.concrete.relation]
img [definition, in regexp.abstract.relation]
img [definition, in regexp.synthesis.clash.relation]
img_spec [lemma, in regexp.synthesis.clash.relation]
imset_inr_inl [lemma, in regexp.abstract.utils]
imset_inl_inr [lemma, in regexp.abstract.utils]
imset_inr [lemma, in regexp.abstract.utils]
imset_inl [lemma, in regexp.abstract.utils]
inhabited [definition, in regexp.abstract.utils]
inhabited [definition, in regexp.synthesis.clash.subset]
inhabited [definition, in regexp.concrete.subset]
inhabitedIP [lemma, in regexp.abstract.utils]
inhabitedP [definition, in regexp.abstract.utils]
inhabitedP [lemma, in regexp.concrete.subset]
inhabited_spec [lemma, in regexp.synthesis.clash.subset]
inhabited_spec [lemma, in regexp.concrete.subset]
initial [definition, in regexp.abstract.automata.singleton]
initial [definition, in regexp.concrete.automata.concat]
initial [definition, in regexp.concrete.automata.singleton]
initial [definition, in regexp.abstract.automata.oneOrMore]
initial [definition, in regexp.concrete.automata.oneOrMore]
initial [definition, in regexp.abstract.automata.concat]
injDU [lemma, in regexp.concrete.subset]
injl [definition, in regexp.concrete.subset]
injlinv_spec [lemma, in regexp.concrete.subset]
injl_spec [lemma, in regexp.concrete.subset]
injr [definition, in regexp.concrete.subset]
injrinv_spec [lemma, in regexp.concrete.subset]
injr_spec [lemma, in regexp.concrete.subset]
inl_inj [lemma, in regexp.concrete.subset]
inr_inj [lemma, in regexp.concrete.subset]
internal [module, in regexp.syn]
internal.alloc [definition, in regexp.syn]
internal.compile [definition, in regexp.syn]
internal.denote [definition, in regexp.syn]
interpret [definition, in regexp.concrete.rule]
interpretation [lemma, in regexp.concrete.rule]
intersection [definition, in regexp.synthesis.clash.subset]
intersection [definition, in regexp.concrete.subset]
intersection_spec [lemma, in regexp.synthesis.clash.subset]
intersection_spec [lemma, in regexp.concrete.subset]
in_initialR [lemma, in regexp.abstract.automata.concat]
in_initialL [lemma, in regexp.abstract.automata.concat]
isAlpha [definition, in regexp.byte]
isAlphaNum [definition, in regexp.byte]
isAscii [definition, in regexp.byte]
isDigit [definition, in regexp.byte]
isFinal [definition, in regexp.synthesis]
isSmallAlpha [definition, in regexp.byte]
isSucc [axiom, in regexp.synthesis.clash.constraint]

K

knownNat [axiom, in regexp.synthesis.clash.constraint]

L

lang [definition, in regexp.lang]
lang [library]
language [definition, in regexp.expr]
language [definition, in regexp.concrete.rule]
leb [axiom, in regexp.byte]
lemb [lemma, in regexp.abstract.utils]
letter [projection, in regexp.concrete.rule]
lift [definition, in regexp.synthesis.clash.universe]
liftPath [lemma, in regexp.abstract.automata.oneOrMore]
liftStep [lemma, in regexp.abstract.automata.oneOrMore]

M

machine [record, in regexp.synthesis]
makeRule [definition, in regexp.syn]
many [definition, in regexp.lang]
many [definition, in regexp.expr]
many1 [definition, in regexp.lang]
many1 [constructor, in regexp.expr]
many1_nil [lemma, in regexp.lang]
map [definition, in regexp.concrete.function]
map [axiom, in regexp.synthesis.clash.function]
Map [section, in regexp.prelude]
map [definition, in regexp.expr]
mapper [definition, in regexp.synthesis]
map_spec [axiom, in regexp.synthesis.clash.axioms]
map_eqfun [lemma, in regexp.concrete.function]
map_compose [lemma, in regexp.concrete.function]
map_catE [lemma, in regexp.prelude]
map_single [lemma, in regexp.prelude]
map_nil [lemma, in regexp.prelude]
Map.A [variable, in regexp.prelude]
Map.B [variable, in regexp.prelude]
Map.f [variable, in regexp.prelude]
matcher [module, in regexp.expr]
matcher_of [definition, in regexp.concrete.rule]
matcher.language [definition, in regexp.expr]
matcher.t [definition, in regexp.expr]
matrix [definition, in regexp.concrete.relation]
Matrix [section, in regexp.concrete.relation]
Matrix [section, in regexp.abstract.automata.path]
Matrix [section, in regexp.abstract.automata.transition]
matrix [definition, in regexp.abstract.relation]
Matrix [section, in regexp.abstract.relation]
matrix_spec [lemma, in regexp.concrete.relation]
matrix_eq [lemma, in regexp.abstract.relation]
Matrix.a1 [variable, in regexp.concrete.relation]
Matrix.a1 [variable, in regexp.abstract.relation]
Matrix.a2 [variable, in regexp.concrete.relation]
Matrix.a2 [variable, in regexp.abstract.relation]
Matrix.B [variable, in regexp.abstract.automata.path]
Matrix.B [variable, in regexp.abstract.automata.transition]
Matrix.b1 [variable, in regexp.concrete.relation]
Matrix.b1 [variable, in regexp.abstract.relation]
Matrix.b2 [variable, in regexp.concrete.relation]
Matrix.b2 [variable, in regexp.abstract.relation]
Matrix.r01 [variable, in regexp.abstract.automata.path]
Matrix.r01 [variable, in regexp.abstract.automata.transition]
Matrix.St0 [variable, in regexp.abstract.automata.path]
Matrix.St0 [variable, in regexp.abstract.automata.transition]
Matrix.St1 [variable, in regexp.abstract.automata.path]
Matrix.St1 [variable, in regexp.abstract.automata.transition]
Matrix.tr0 [variable, in regexp.abstract.automata.path]
Matrix.tr0 [variable, in regexp.abstract.automata.transition]
Matrix.tr1 [variable, in regexp.abstract.automata.path]
Matrix.tr1 [variable, in regexp.abstract.automata.transition]
mkTrans [definition, in regexp.abstract.automata.singleton]
mkTrans [definition, in regexp.concrete.automata.concat]
mkTrans [definition, in regexp.concrete.automata.singleton]
mkTrans [definition, in regexp.abstract.automata.oneOrMore]
mkTrans [definition, in regexp.concrete.automata.alt]
mkTrans [definition, in regexp.concrete.automata.oneOrMore]
mkTrans [definition, in regexp.abstract.automata.concat]
mLanguage [definition, in regexp.concrete.rule]

N

neighbourhood [lemma, in regexp.abstract.automata.oneOrMore]
neighbourhood_reachable [lemma, in regexp.abstract.automata.path]
neighbourhood_cover [lemma, in regexp.abstract.automata.path]
neighbours [definition, in regexp.abstract.automata.transition]
next [definition, in regexp.concrete.automata.simulation]
next [definition, in regexp.abstract.automata.simulation]
next [definition, in regexp.synthesis.clash.automata]
nexts [definition, in regexp.abstract.automata.simulation]
nexts_wpath [lemma, in regexp.abstract.automata.simulation]
next_spec [lemma, in regexp.concrete.automata.simulation]
next_step [lemma, in regexp.abstract.automata.simulation]
next_spec [lemma, in regexp.synthesis.clash.automata]
nfa [projection, in regexp.synthesis]
NFA [record, in regexp.abstract.automata]
NFA [record, in regexp.concrete.automata]
NFA [record, in regexp.synthesis.clash.automata]
nfaeqdec [definition, in regexp.abstract.automata]
nilP [definition, in regexp.abstract.automata.path]
noPathLRE [lemma, in regexp.abstract.automata.path]
nopathP [definition, in regexp.abstract.automata.path]
noPathRLE [lemma, in regexp.abstract.automata.path]
noStepLRE [lemma, in regexp.abstract.automata.transition]
noStepRLE [lemma, in regexp.abstract.automata.transition]

O

oneOf [definition, in regexp.byte]
oneOrMore [library]
oneOrMore [library]
or [definition, in regexp.concrete.relation]

P

Path [section, in regexp.abstract.automata.path]
path [library]
pathLP [lemma, in regexp.abstract.automata.path]
pathLRE [lemma, in regexp.abstract.automata.concat]
pathP [lemma, in regexp.abstract.automata.singleton]
pathRP [lemma, in regexp.abstract.automata.path]
PathThickening [section, in regexp.abstract.automata.world]
PathThickening.B [variable, in regexp.abstract.automata.world]
PathThickening.mac [variable, in regexp.abstract.automata.world]
PathThickening.St [variable, in regexp.abstract.automata.world]
path_thickening [lemma, in regexp.abstract.automata.world]
Path.B [variable, in regexp.abstract.automata.path]
Path.St [variable, in regexp.abstract.automata.path]
Path.tr [variable, in regexp.abstract.automata.path]
pow [definition, in regexp.lang]
pow0 [lemma, in regexp.lang]
pow1 [lemma, in regexp.lang]
predlift [definition, in regexp.synthesis.clash.universe]
prefinal0 [definition, in regexp.abstract.automata.concat]
prelude [library]
prelude [library]
process [definition, in regexp.concrete.automata.simulation]
process [definition, in regexp.abstract.automata.simulation]
process [definition, in regexp.synthesis.clash.automata]
process_spec [lemma, in regexp.concrete.automata.simulation]
process_spec [lemma, in regexp.synthesis.clash.automata]
proj_sum_2 [lemma, in regexp.concrete.function]
proj_sum_1 [lemma, in regexp.concrete.function]
proj1 [definition, in regexp.concrete.function]
proj2 [definition, in regexp.concrete.function]

R

reach [definition, in regexp.abstract.automata.oneOrMore]
reachability [lemma, in regexp.abstract.automata.simulation]
reachable [definition, in regexp.abstract.automata.path]
reachableLL [lemma, in regexp.abstract.automata.path]
reachableRR [lemma, in regexp.abstract.automata.path]
reachableULE [lemma, in regexp.abstract.automata.path]
reachableURE [lemma, in regexp.abstract.automata.path]
reachable_cover [lemma, in regexp.abstract.automata.oneOrMore]
reachable_concat [lemma, in regexp.abstract.automata.path]
reachable1 [lemma, in regexp.abstract.automata.path]
reach_cons [lemma, in regexp.abstract.automata.oneOrMore]
reach_accept [lemma, in regexp.abstract.automata.oneOrMore]
README [library]
regexp [projection, in regexp.concrete.rule]
reject [definition, in regexp.synthesis]
relation [library]
relation [library]
relation [library]
rel01 [definition, in regexp.concrete.automata.concat]
rel01 [definition, in regexp.abstract.automata.concat]
Ret [constructor, in regexp.syn]
re2nfa [definition, in regexp.abstract.automata.build]
re2nfa [definition, in regexp.concrete.automata.build]
Rule [record, in regexp.concrete.rule]
rule [library]
runOnList [definition, in regexp.synthesis]

S

satisfy [definition, in regexp.lang]
satisfy_ext [lemma, in regexp.lang]
scanner [definition, in regexp.synthesis]
scanTable [projection, in regexp.synthesis]
setUnit [lemma, in regexp.concrete.subset]
set_unit [lemma, in regexp.abstract.utils]
Simulation [section, in regexp.abstract.automata.simulation]
simulation [library]
simulation [library]
Simulation.B [variable, in regexp.abstract.automata.simulation]
Simulation.St [variable, in regexp.abstract.automata.simulation]
Simulation.tr [variable, in regexp.abstract.automata.simulation]
single [constructor, in regexp.expr]
singleP [lemma, in regexp.abstract.automata.path]
singleton [axiom, in regexp.synthesis.clash.function]
singleton [definition, in regexp.lang]
singleton [definition, in regexp.concrete.subset]
singleton [library]
singleton [library]
singleton_spec [lemma, in regexp.concrete.subset]
snocE [lemma, in regexp.abstract.utils]
snocP [lemma, in regexp.abstract.automata.path]
sort [inductive, in regexp.concrete.universe]
sortOf [definition, in regexp.syn]
sort_sind [definition, in regexp.concrete.universe]
sort_rec [definition, in regexp.concrete.universe]
sort_ind [definition, in regexp.concrete.universe]
sort_rect [definition, in regexp.concrete.universe]
split [definition, in regexp.syn]
start [definition, in regexp.synthesis]
start [projection, in regexp.abstract.automata]
start [projection, in regexp.concrete.automata]
start [projection, in regexp.synthesis.clash.automata]
startBack [definition, in regexp.abstract.automata.oneOrMore]
startBack [definition, in regexp.concrete.automata.oneOrMore]
startBack_denote [lemma, in regexp.concrete.automata.oneOrMore]
start0 [definition, in regexp.concrete.automata.concat]
start0 [definition, in regexp.abstract.automata.concat]
start0_subset_initial [lemma, in regexp.abstract.automata.concat]
start1 [definition, in regexp.concrete.automata.concat]
start1 [definition, in regexp.abstract.automata.concat]
State [definition, in regexp.abstract.automata.singleton]
State [definition, in regexp.concrete.automata.concat]
State [definition, in regexp.abstract.utils]
state [definition, in regexp.synthesis]
State [definition, in regexp.concrete.automata.singleton]
State [definition, in regexp.abstract.automata.build]
State [definition, in regexp.abstract.automata.alt]
State [definition, in regexp.abstract.automata.epsilon]
State [definition, in regexp.concrete.automata.alt]
State [definition, in regexp.concrete.automata.epsilon]
State [definition, in regexp.concrete.automata.build]
State [definition, in regexp.abstract.automata.concat]
stateE [lemma, in regexp.concrete.automata.build]
state_deadend [lemma, in regexp.abstract.automata.epsilon]
step [definition, in regexp.abstract.automata.transition]
stepFinal [lemma, in regexp.abstract.automata.oneOrMore]
stepLP [lemma, in regexp.abstract.automata.transition]
stepLRP [lemma, in regexp.abstract.automata.concat]
stepP [lemma, in regexp.abstract.automata.singleton]
stepRP [lemma, in regexp.abstract.automata.transition]
step_next [lemma, in regexp.abstract.automata.simulation]
subset [library]
subset [library]
success [definition, in regexp.concrete.automata.simulation]
success [definition, in regexp.abstract.automata.simulation]
success [definition, in regexp.synthesis.clash.automata]
success_spec [lemma, in regexp.concrete.automata.simulation]
success_spec [lemma, in regexp.synthesis.clash.automata]
sum_proj [lemma, in regexp.concrete.function]
syn [definition, in regexp.synthesis.clash.function]
syn [definition, in regexp.synthesis.clash.subset]
Syn [section, in regexp.synthesis.clash.subset]
syn [definition, in regexp.synthesis.clash.relation]
syn [definition, in regexp.synthesis.clash.automata]
syn [library]
Synthesis [section, in regexp.synthesis.clash.relation]
Synthesis [section, in regexp.synthesis.clash.automata]
synthesis [library]
Synthesis.B [variable, in regexp.synthesis.clash.automata]
Synthesis.mac [variable, in regexp.synthesis.clash.automata]
Synthesis.St [variable, in regexp.synthesis.clash.automata]
Synthesis.s1 [variable, in regexp.synthesis.clash.relation]
Synthesis.s2 [variable, in regexp.synthesis.clash.relation]
synthesize [definition, in regexp.synthesis]
Syn.s [variable, in regexp.synthesis.clash.subset]

T

t [definition, in regexp.concrete.relation]
t [inductive, in regexp.concrete.function]
t [axiom, in regexp.synthesis.clash.function]
t [definition, in regexp.synthesis.clash.subset]
t [definition, in regexp.abstract.automata.path]
t [definition, in regexp.abstract.automata.transition]
t [definition, in regexp.concrete.subset]
T [definition, in regexp.syn]
t [inductive, in regexp.syn]
t [definition, in regexp.abstract.relation]
t [inductive, in regexp.expr]
t [definition, in regexp.synthesis.clash.relation]
terminal [definition, in regexp.abstract.automata.singleton]
terminal [definition, in regexp.concrete.automata.concat]
terminal [definition, in regexp.concrete.automata.singleton]
terminal [definition, in regexp.abstract.automata.oneOrMore]
terminal [definition, in regexp.concrete.automata.oneOrMore]
terminal [definition, in regexp.abstract.automata.concat]
terminal_deadend [lemma, in regexp.abstract.automata.singleton]
thicken [definition, in regexp.lang.world]
Thickening [section, in regexp.lang.world]
Thickening.B [variable, in regexp.lang.world]
thicken_many1 [lemma, in regexp.lang.world]
thicken_pow [lemma, in regexp.lang.world]
thicken_concat [lemma, in regexp.lang.world]
thicken_alt [lemma, in regexp.lang.world]
thicken_singleton [lemma, in regexp.lang.world]
thicken_epsilon [lemma, in regexp.lang.world]
to [definition, in regexp.concrete.function]
to_proj2 [lemma, in regexp.concrete.function]
to_proj1 [lemma, in regexp.concrete.function]
to_map [lemma, in regexp.concrete.function]
to_plus_2 [lemma, in regexp.concrete.function]
to_plus_1 [lemma, in regexp.concrete.function]
to_from [lemma, in regexp.concrete.function]
tr [definition, in regexp.abstract.automata.epsilon]
tr [definition, in regexp.abstract.automata.oneOrMore]
tr [definition, in regexp.abstract.automata.path]
tr [definition, in regexp.abstract.automata.transition]
tr [definition, in regexp.concrete.automata.oneOrMore]
trans [projection, in regexp.abstract.automata]
trans [projection, in regexp.concrete.automata]
trans [projection, in regexp.synthesis.clash.automata]
Transition [section, in regexp.abstract.automata.singleton]
transition [definition, in regexp.synthesis]
Transition [section, in regexp.abstract.automata.epsilon]
transition [module, in regexp.concrete.automata]
transition [module, in regexp.synthesis.clash.automata]
transition [library]
transition_equality [lemma, in regexp.concrete.automata.singleton]
transition_equality [lemma, in regexp.concrete.automata.epsilon]
Transition.b [variable, in regexp.abstract.automata.singleton]
Transition.B [variable, in regexp.abstract.automata.singleton]
Transition.b [variable, in regexp.abstract.automata.epsilon]
Transition.B [variable, in regexp.abstract.automata.epsilon]
transition.denote [definition, in regexp.concrete.automata]
transition.syn [definition, in regexp.synthesis.clash.automata]
transition.t [definition, in regexp.concrete.automata]
transition.t [definition, in regexp.synthesis.clash.automata]
transpose [definition, in regexp.concrete.function]
transpose_spec [lemma, in regexp.concrete.function]
trivialpathP [lemma, in regexp.abstract.automata.path]
tr0 [definition, in regexp.abstract.automata.concat]
tr1 [definition, in regexp.abstract.automata.concat]
typ [definition, in regexp.synthesis.clash.constraint]
typeOf [definition, in regexp.concrete.universe]
t_sind [definition, in regexp.concrete.function]
t_rec [definition, in regexp.concrete.function]
t_ind [definition, in regexp.concrete.function]
t_rect [definition, in regexp.concrete.function]
t_sind [definition, in regexp.syn]
t_rec [definition, in regexp.syn]
t_ind [definition, in regexp.syn]
t_rect [definition, in regexp.syn]
t_sind [definition, in regexp.expr]
t_rec [definition, in regexp.expr]
t_ind [definition, in regexp.expr]
t_rect [definition, in regexp.expr]

U

unbind [definition, in regexp.syn]
unconst [definition, in regexp.concrete.function]
unconst_const [lemma, in regexp.concrete.function]
union [definition, in regexp.synthesis.clash.subset]
union [definition, in regexp.concrete.subset]
union_spec [lemma, in regexp.synthesis.clash.subset]
union_spec [lemma, in regexp.concrete.subset]
union_empty_l [lemma, in regexp.concrete.subset]
union_empty_r [lemma, in regexp.concrete.subset]
Unit [axiom, in regexp.synthesis.clash.universe]
Unit [constructor, in regexp.concrete.universe]
universe [library]
universe [library]
unnest [definition, in regexp.expr]
unReachableLR [lemma, in regexp.abstract.automata.path]
unReachableRL [lemma, in regexp.abstract.automata.path]
unret [definition, in regexp.syn]
unsum [definition, in regexp.concrete.function]
unsum_sum [lemma, in regexp.concrete.function]
utils [library]
utmatrix [definition, in regexp.abstract.automata.transition]

V

vars [definition, in regexp.syn]

W

wAccept [definition, in regexp.abstract.automata.world]
wLanguage [definition, in regexp.concrete.rule]
world [definition, in regexp.lang.world]
world [library]
world [library]
wpath [definition, in regexp.abstract.automata.world]
wpath_nexts [lemma, in regexp.abstract.automata.simulation]
wpath_uncons [lemma, in regexp.abstract.automata.world]
wpath_nilE [lemma, in regexp.abstract.automata.world]
wreachable [definition, in regexp.abstract.automata.world]

Z

Zero [axiom, in regexp.synthesis.clash.universe]
zipWith [definition, in regexp.concrete.function]
zipWith [axiom, in regexp.synthesis.clash.function]
ZipWithMap [section, in regexp.concrete.function]
ZipWithMap.A [variable, in regexp.concrete.function]
ZipWithMap.B [variable, in regexp.concrete.function]
ZipWithMap.C [variable, in regexp.concrete.function]
ZipWithMap.f [variable, in regexp.concrete.function]
ZipWithMap.Right [section, in regexp.concrete.function]
ZipWithMap.Right.Bp [variable, in regexp.concrete.function]
ZipWithMap.Right.convB [variable, in regexp.concrete.function]
ZipWithMap.Right.convC [variable, in regexp.concrete.function]
ZipWithMap.Right.Cp [variable, in regexp.concrete.function]
ZipWithMap.Right.fp [variable, in regexp.concrete.function]
ZipWithMap.Right.Hconv [variable, in regexp.concrete.function]
zipWith_spec [axiom, in regexp.synthesis.clash.axioms]
zipWith_mapR [lemma, in regexp.concrete.function]
zipWith3 [definition, in regexp.concrete.function]
zipWith4 [definition, in regexp.concrete.function]
zip_pointwise4 [lemma, in regexp.concrete.function]
zip_pointwise3 [lemma, in regexp.concrete.function]
zip_pointwise [lemma, in regexp.concrete.function]

other

rules:let _ := _ in _ [notation, in regexp.syn]
rules:match _ [notation, in regexp.syn]
_ ∘ _ (concrete_scope) [notation, in regexp.concrete.relation]
_ .2 (concrete_scope) [notation, in regexp.concrete.function]
_ .1 (concrete_scope) [notation, in regexp.concrete.function]
_ ~> _ (concrete_scope) [notation, in regexp.concrete.function]
_ ++ _ (concrete_scope) [notation, in regexp.concrete.function]
∅ (concrete_scope) [notation, in regexp.concrete.subset]
_ ⊎ _ (concrete_scope) [notation, in regexp.concrete.subset]
_ ∩ _ (concrete_scope) [notation, in regexp.concrete.subset]
_ ∪ _ (concrete_scope) [notation, in regexp.concrete.subset]
_ ∐ _ (concrete_scope) [notation, in regexp.concrete.universe]
𝟙 (concrete_scope) [notation, in regexp.concrete.universe]
_ ^ _ (language_scope) [notation, in regexp.lang]
_ ++ _ (language_scope) [notation, in regexp.lang]
_ || _ (language_scope) [notation, in regexp.lang]
_ ++ _ (regexp_scope) [notation, in regexp.expr]
_ || _ (regexp_scope) [notation, in regexp.expr]
ε (regexp_scope) [notation, in regexp.expr]
_ ∐ _ (synthesis_scope) [notation, in regexp.synthesis.clash.universe]
𝟙 (synthesis_scope) [notation, in regexp.synthesis.clash.universe]
_ ~> _ (synthesis_scope) [notation, in regexp.synthesis.clash.function]
[ _ , .. , _ , _ => _ ] (synthesis_scope) [notation, in regexp.synthesis.clash.constraint]
[ _ => _ ] (synthesis_scope) [notation, in regexp.synthesis.clash.constraint]
_ =A= _ [notation, in regexp.abstract.automata]
_ ≡ _ [notation, in regexp.lang]
[rule| _ |] [notation, in regexp.syn]
ε [notation, in regexp.lang]
⟨ _ ⟩ [notation, in regexp.synthesis.clash.universe]

Notation Index

other

rules:let _ := _ in _ [in regexp.syn]
rules:match _ [in regexp.syn]
_ ∘ _ (concrete_scope) [in regexp.concrete.relation]
_ .2 (concrete_scope) [in regexp.concrete.function]
_ .1 (concrete_scope) [in regexp.concrete.function]
_ ~> _ (concrete_scope) [in regexp.concrete.function]
_ ++ _ (concrete_scope) [in regexp.concrete.function]
∅ (concrete_scope) [in regexp.concrete.subset]
_ ⊎ _ (concrete_scope) [in regexp.concrete.subset]
_ ∩ _ (concrete_scope) [in regexp.concrete.subset]
_ ∪ _ (concrete_scope) [in regexp.concrete.subset]
_ ∐ _ (concrete_scope) [in regexp.concrete.universe]
𝟙 (concrete_scope) [in regexp.concrete.universe]
_ ^ _ (language_scope) [in regexp.lang]
_ ++ _ (language_scope) [in regexp.lang]
_ || _ (language_scope) [in regexp.lang]
_ ++ _ (regexp_scope) [in regexp.expr]
_ || _ (regexp_scope) [in regexp.expr]
ε (regexp_scope) [in regexp.expr]
_ ∐ _ (synthesis_scope) [in regexp.synthesis.clash.universe]
𝟙 (synthesis_scope) [in regexp.synthesis.clash.universe]
_ ~> _ (synthesis_scope) [in regexp.synthesis.clash.function]
[ _ , .. , _ , _ => _ ] (synthesis_scope) [in regexp.synthesis.clash.constraint]
[ _ => _ ] (synthesis_scope) [in regexp.synthesis.clash.constraint]
_ =A= _ [in regexp.abstract.automata]
_ ≡ _ [in regexp.lang]
[rule| _ |] [in regexp.syn]
ε [in regexp.lang]
⟨ _ ⟩ [in regexp.synthesis.clash.universe]

Module Index

A

access [in regexp.abstract.automata.path]

B

big [in regexp.synthesis.clash.subset]
big [in regexp.concrete.subset]
binary [in regexp.concrete.relation]
binary [in regexp.abstract.relation]
binary [in regexp.synthesis.clash.relation]

C

consistent [in regexp.lang.world]
consistent.left [in regexp.lang.world]
consistent.right [in regexp.lang.world]

E

eq [in regexp.lang]

I

internal [in regexp.syn]

M

matcher [in regexp.expr]

T

transition [in regexp.concrete.automata]
transition [in regexp.synthesis.clash.automata]

Variable Index

A

access.Cxt.B [in regexp.abstract.automata.path]
access.Cxt.St [in regexp.abstract.automata.path]
access.Cxt.tr [in regexp.abstract.automata.path]

B

BigSyn.f [in regexp.synthesis.clash.subset]
BigSyn.idx [in regexp.synthesis.clash.subset]
BigSyn.s [in regexp.synthesis.clash.subset]
big.Cxt.F [in regexp.concrete.subset]
big.Cxt.idx [in regexp.synthesis.clash.subset]
big.Cxt.idx [in regexp.concrete.subset]
big.Cxt.s [in regexp.synthesis.clash.subset]
big.Cxt.s [in regexp.concrete.subset]
Build.B [in regexp.concrete.automata.alt]
Build.mac0 [in regexp.concrete.automata.alt]
Build.mac1 [in regexp.concrete.automata.alt]
Build.St0 [in regexp.concrete.automata.alt]
Build.St1 [in regexp.concrete.automata.alt]

C

Comap.A [in regexp.lang]
Comap.B [in regexp.lang]
Comap.f [in regexp.lang]
consistent.left.Cxt.B [in regexp.lang.world]
consistent.right.Cxt.B [in regexp.lang.world]
Correctness.I [in regexp.synthesis]
Correctness.rls [in regexp.synthesis]
Cxt.aT [in regexp.concrete.rule]
Cxt.aT [in regexp.concrete.rule]
Cxt.B [in regexp.concrete.automata.concat]
Cxt.B [in regexp.abstract.automata.build]
Cxt.B [in regexp.abstract.automata.alt]
Cxt.B [in regexp.abstract.automata.oneOrMore]
Cxt.B [in regexp.concrete.automata.alt]
Cxt.B [in regexp.abstract.automata.path]
Cxt.B [in regexp.concrete.automata.oneOrMore]
Cxt.B [in regexp.concrete.automata.build]
Cxt.B [in regexp.abstract.automata.concat]
Cxt.I [in regexp.concrete.rule]
Cxt.I [in regexp.concrete.rule]
Cxt.mac [in regexp.abstract.automata.oneOrMore]
Cxt.mac [in regexp.concrete.automata.oneOrMore]
Cxt.mac0 [in regexp.concrete.automata.concat]
Cxt.mac0 [in regexp.abstract.automata.alt]
Cxt.mac0 [in regexp.abstract.automata.concat]
Cxt.mac1 [in regexp.concrete.automata.concat]
Cxt.mac1 [in regexp.abstract.automata.alt]
Cxt.mac1 [in regexp.abstract.automata.concat]
Cxt.s [in regexp.concrete.rule]
Cxt.s [in regexp.concrete.rule]
Cxt.St [in regexp.abstract.automata.oneOrMore]
Cxt.St [in regexp.abstract.automata.path]
Cxt.St [in regexp.concrete.automata.oneOrMore]
Cxt.St0 [in regexp.concrete.automata.concat]
Cxt.St0 [in regexp.abstract.utils]
Cxt.St0 [in regexp.abstract.automata.alt]
Cxt.St0 [in regexp.concrete.automata.alt]
Cxt.St0 [in regexp.abstract.automata.concat]
Cxt.St1 [in regexp.concrete.automata.concat]
Cxt.St1 [in regexp.abstract.utils]
Cxt.St1 [in regexp.abstract.automata.alt]
Cxt.St1 [in regexp.concrete.automata.alt]
Cxt.St1 [in regexp.abstract.automata.concat]
Cxt.tr [in regexp.abstract.automata.path]
Cxt.tr0 [in regexp.concrete.automata.alt]
Cxt.tr1 [in regexp.concrete.automata.alt]

D

DecEq.B [in regexp.abstract.automata]
DecEq.St [in regexp.abstract.automata]
Defn.b [in regexp.synthesis.clash.automata]
Defn.s [in regexp.synthesis.clash.automata]

E

Epsilon.B [in regexp.concrete.automata.epsilon]
EqFun.A [in regexp.prelude]
EqFun.B [in regexp.prelude]
Equiv.B [in regexp.abstract.automata]
Equiv.St [in regexp.abstract.automata]
eq.Cxt.A [in regexp.lang]

F

FoldMap.A [in regexp.concrete.function]
FoldMap.B [in regexp.concrete.function]
FoldMap.conv [in regexp.concrete.function]
FoldMap.f [in regexp.concrete.function]
FoldMap.g [in regexp.concrete.function]
FoldMap.Hconv [in regexp.concrete.function]

H

hb_instance_1.St [in regexp.abstract.automata]
hb_instance_1.B [in regexp.abstract.automata]

M

Map.A [in regexp.prelude]
Map.B [in regexp.prelude]
Map.f [in regexp.prelude]
Matrix.a1 [in regexp.concrete.relation]
Matrix.a1 [in regexp.abstract.relation]
Matrix.a2 [in regexp.concrete.relation]
Matrix.a2 [in regexp.abstract.relation]
Matrix.B [in regexp.abstract.automata.path]
Matrix.B [in regexp.abstract.automata.transition]
Matrix.b1 [in regexp.concrete.relation]
Matrix.b1 [in regexp.abstract.relation]
Matrix.b2 [in regexp.concrete.relation]
Matrix.b2 [in regexp.abstract.relation]
Matrix.r01 [in regexp.abstract.automata.path]
Matrix.r01 [in regexp.abstract.automata.transition]
Matrix.St0 [in regexp.abstract.automata.path]
Matrix.St0 [in regexp.abstract.automata.transition]
Matrix.St1 [in regexp.abstract.automata.path]
Matrix.St1 [in regexp.abstract.automata.transition]
Matrix.tr0 [in regexp.abstract.automata.path]
Matrix.tr0 [in regexp.abstract.automata.transition]
Matrix.tr1 [in regexp.abstract.automata.path]
Matrix.tr1 [in regexp.abstract.automata.transition]

P

PathThickening.B [in regexp.abstract.automata.world]
PathThickening.mac [in regexp.abstract.automata.world]
PathThickening.St [in regexp.abstract.automata.world]
Path.B [in regexp.abstract.automata.path]
Path.St [in regexp.abstract.automata.path]
Path.tr [in regexp.abstract.automata.path]

S

Simulation.B [in regexp.abstract.automata.simulation]
Simulation.St [in regexp.abstract.automata.simulation]
Simulation.tr [in regexp.abstract.automata.simulation]
Synthesis.B [in regexp.synthesis.clash.automata]
Synthesis.mac [in regexp.synthesis.clash.automata]
Synthesis.St [in regexp.synthesis.clash.automata]
Synthesis.s1 [in regexp.synthesis.clash.relation]
Synthesis.s2 [in regexp.synthesis.clash.relation]
Syn.s [in regexp.synthesis.clash.subset]

T

Thickening.B [in regexp.lang.world]
Transition.b [in regexp.abstract.automata.singleton]
Transition.B [in regexp.abstract.automata.singleton]
Transition.b [in regexp.abstract.automata.epsilon]
Transition.B [in regexp.abstract.automata.epsilon]

Z

ZipWithMap.A [in regexp.concrete.function]
ZipWithMap.B [in regexp.concrete.function]
ZipWithMap.C [in regexp.concrete.function]
ZipWithMap.f [in regexp.concrete.function]
ZipWithMap.Right.Bp [in regexp.concrete.function]
ZipWithMap.Right.convB [in regexp.concrete.function]
ZipWithMap.Right.convC [in regexp.concrete.function]
ZipWithMap.Right.Cp [in regexp.concrete.function]
ZipWithMap.Right.fp [in regexp.concrete.function]
ZipWithMap.Right.Hconv [in regexp.concrete.function]

Library Index

A

alt
alt
automata
automata
automata
axioms

B

build
build
byte

C

concat
concat
constraint

E

epsilon
epsilon
expr

F

function
function

L

lang

O

oneOrMore
oneOrMore

P

path
prelude
prelude

R

README
relation
relation
relation
rule

S

simulation
simulation
singleton
singleton
subset
subset
syn
synthesis

T

U

universe
universe
utils

W

Axiom Index

C

concat [in regexp.synthesis.clash.function]
constant [in regexp.synthesis.clash.function]
constant_spec [in regexp.synthesis.clash.axioms]
CoProd [in regexp.synthesis.clash.universe]

F

fold [in regexp.synthesis.clash.function]
fold_spec [in regexp.synthesis.clash.axioms]

I

isSucc [in regexp.synthesis.clash.constraint]

K

knownNat [in regexp.synthesis.clash.constraint]

L

leb [in regexp.byte]

M

map [in regexp.synthesis.clash.function]
map_spec [in regexp.synthesis.clash.axioms]

S

singleton [in regexp.synthesis.clash.function]

T

t [in regexp.synthesis.clash.function]

U

Unit [in regexp.synthesis.clash.universe]

Z

Zero [in regexp.synthesis.clash.universe]
zipWith [in regexp.synthesis.clash.function]
zipWith_spec [in regexp.synthesis.clash.axioms]

Lemma Index

A

accept_app [in regexp.abstract.automata.oneOrMore]
accept_cover [in regexp.abstract.automata.oneOrMore]
accept_one [in regexp.abstract.automata.oneOrMore]
accept_concat [in regexp.abstract.automata.concat]
accept_nil [in regexp.abstract.automata.concat]
access.fromsub [in regexp.abstract.automata.path]
access.fromU [in regexp.abstract.automata.path]
access.tosub [in regexp.abstract.automata.path]
access.toU [in regexp.abstract.automata.path]

B

backward [in regexp.abstract.automata.oneOrMore]
bigStartBackU [in regexp.abstract.automata.oneOrMore]
bigunion_spec [in regexp.synthesis.clash.subset]
big.bigcap_sum [in regexp.concrete.subset]
big.bigcup_sum [in regexp.concrete.subset]
big.intersection_spec [in regexp.concrete.subset]
big.union_spec [in regexp.concrete.subset]

C

comap_comap [in regexp.lang]
comap_many1 [in regexp.lang]
comap_pow [in regexp.lang]
comap_concat [in regexp.lang]
comap_satisfy [in regexp.lang]
comap_alt [in regexp.lang]
comap_epsilon [in regexp.lang]
composeP [in regexp.concrete.relation]
concat [in regexp.abstract.automata.path]
concat_epsilon [in regexp.lang]
concat_accept [in regexp.abstract.automata.concat]
consistent.concat [in regexp.lang.world]
consistent.left.consP [in regexp.lang.world]
consistent.left.nilE [in regexp.lang.world]
consistent.right.concat [in regexp.lang.world]
consistent.right.consP [in regexp.lang.world]
consistent.right.nilE [in regexp.lang.world]
consistent.right.singletonP [in regexp.lang.world]
consP [in regexp.abstract.automata.path]
constantE [in regexp.concrete.function]
consume_spec [in regexp.concrete.automata.simulation]
consume_spec [in regexp.synthesis.clash.automata]
correctness [in regexp.abstract.automata.singleton]
correctness [in regexp.concrete.automata.concat]
correctness [in regexp.synthesis]
correctness [in regexp.concrete.automata.singleton]
correctness [in regexp.concrete.automata.simulation]
correctness [in regexp.abstract.automata.build]
correctness [in regexp.abstract.automata.alt]
correctness [in regexp.abstract.automata.epsilon]
correctness [in regexp.abstract.automata.simulation]
correctness [in regexp.abstract.automata.oneOrMore]
correctness [in regexp.concrete.automata.alt]
correctness [in regexp.concrete.automata.oneOrMore]
correctness [in regexp.concrete.automata.epsilon]
correctness [in regexp.concrete.automata.build]
correctness [in regexp.synthesis.clash.automata]
correctness [in regexp.abstract.automata.concat]
coverLRE [in regexp.abstract.automata.concat]
cover_subR [in regexp.abstract.automata.path]
cover_supL [in regexp.abstract.automata.path]
cover_concat [in regexp.abstract.automata.path]
cover_nil [in regexp.abstract.automata.path]
cover_start1 [in regexp.abstract.automata.concat]

D

denoteE [in regexp.concrete.function]
denoteE [in regexp.concrete.subset]
diagonal_spec [in regexp.concrete.relation]
diagonal_matrix [in regexp.abstract.relation]
disjULE [in regexp.concrete.subset]
disjURE [in regexp.concrete.subset]
disUUU [in regexp.concrete.subset]

E

emptyE [in regexp.abstract.relation]
emptyPath [in regexp.abstract.automata.epsilon]
empty_spec [in regexp.concrete.relation]
empty_spec [in regexp.synthesis.clash.subset]
empty_spec [in regexp.concrete.subset]
epsilon_concat [in regexp.lang]
eqfun_trans [in regexp.prelude]
eqfun_sym [in regexp.prelude]
eqfun_refl [in regexp.prelude]
eqnfaP [in regexp.abstract.automata]
equality [in regexp.concrete.automata.concat]
equality [in regexp.concrete.automata.singleton]
equality [in regexp.concrete.automata.alt]
equality [in regexp.concrete.automata.oneOrMore]
equality [in regexp.concrete.automata.epsilon]
equivalence [in regexp.concrete.rule]
eq_equiv [in regexp.abstract.automata]
eq.refl [in regexp.lang]
eq.sym [in regexp.lang]
eq.trans [in regexp.lang]
extensionality [in regexp.concrete.function]

F

foldl_map [in regexp.prelude]
fold_map [in regexp.concrete.function]
forward [in regexp.abstract.automata.oneOrMore]
fromeq [in regexp.concrete.function]
from_to [in regexp.concrete.function]
full_spec [in regexp.concrete.relation]
full_spec [in regexp.concrete.subset]

G

graded_reachability [in regexp.abstract.automata.oneOrMore]

H

hasfinal0_denote [in regexp.concrete.automata.concat]

I

ifeq_spec [in regexp.concrete.function]
img_spec [in regexp.synthesis.clash.relation]
imset_inr_inl [in regexp.abstract.utils]
imset_inl_inr [in regexp.abstract.utils]
imset_inr [in regexp.abstract.utils]
imset_inl [in regexp.abstract.utils]
inhabitedIP [in regexp.abstract.utils]
inhabitedP [in regexp.concrete.subset]
inhabited_spec [in regexp.synthesis.clash.subset]
inhabited_spec [in regexp.concrete.subset]
injDU [in regexp.concrete.subset]
injlinv_spec [in regexp.concrete.subset]
injl_spec [in regexp.concrete.subset]
injrinv_spec [in regexp.concrete.subset]
injr_spec [in regexp.concrete.subset]
inl_inj [in regexp.concrete.subset]
inr_inj [in regexp.concrete.subset]
interpretation [in regexp.concrete.rule]
intersection_spec [in regexp.synthesis.clash.subset]
intersection_spec [in regexp.concrete.subset]
in_initialR [in regexp.abstract.automata.concat]
in_initialL [in regexp.abstract.automata.concat]

L

lemb [in regexp.abstract.utils]
liftPath [in regexp.abstract.automata.oneOrMore]
liftStep [in regexp.abstract.automata.oneOrMore]

M

many1_nil [in regexp.lang]
map_eqfun [in regexp.concrete.function]
map_compose [in regexp.concrete.function]
map_catE [in regexp.prelude]
map_single [in regexp.prelude]
map_nil [in regexp.prelude]
matrix_spec [in regexp.concrete.relation]
matrix_eq [in regexp.abstract.relation]

N

neighbourhood [in regexp.abstract.automata.oneOrMore]
neighbourhood_reachable [in regexp.abstract.automata.path]
neighbourhood_cover [in regexp.abstract.automata.path]
nexts_wpath [in regexp.abstract.automata.simulation]
next_spec [in regexp.concrete.automata.simulation]
next_step [in regexp.abstract.automata.simulation]
next_spec [in regexp.synthesis.clash.automata]
noPathLRE [in regexp.abstract.automata.path]
noPathRLE [in regexp.abstract.automata.path]
noStepLRE [in regexp.abstract.automata.transition]
noStepRLE [in regexp.abstract.automata.transition]

P

pathLP [in regexp.abstract.automata.path]
pathLRE [in regexp.abstract.automata.concat]
pathP [in regexp.abstract.automata.singleton]
pathRP [in regexp.abstract.automata.path]
path_thickening [in regexp.abstract.automata.world]
pow0 [in regexp.lang]
pow1 [in regexp.lang]
process_spec [in regexp.concrete.automata.simulation]
process_spec [in regexp.synthesis.clash.automata]
proj_sum_2 [in regexp.concrete.function]
proj_sum_1 [in regexp.concrete.function]

R

reachability [in regexp.abstract.automata.simulation]
reachableLL [in regexp.abstract.automata.path]
reachableRR [in regexp.abstract.automata.path]
reachableULE [in regexp.abstract.automata.path]
reachableURE [in regexp.abstract.automata.path]
reachable_cover [in regexp.abstract.automata.oneOrMore]
reachable_concat [in regexp.abstract.automata.path]
reachable1 [in regexp.abstract.automata.path]
reach_cons [in regexp.abstract.automata.oneOrMore]
reach_accept [in regexp.abstract.automata.oneOrMore]

S

satisfy_ext [in regexp.lang]
setUnit [in regexp.concrete.subset]
set_unit [in regexp.abstract.utils]
singleP [in regexp.abstract.automata.path]
singleton_spec [in regexp.concrete.subset]
snocE [in regexp.abstract.utils]
snocP [in regexp.abstract.automata.path]
startBack_denote [in regexp.concrete.automata.oneOrMore]
start0_subset_initial [in regexp.abstract.automata.concat]
stateE [in regexp.concrete.automata.build]
state_deadend [in regexp.abstract.automata.epsilon]
stepFinal [in regexp.abstract.automata.oneOrMore]
stepLP [in regexp.abstract.automata.transition]
stepLRP [in regexp.abstract.automata.concat]
stepP [in regexp.abstract.automata.singleton]
stepRP [in regexp.abstract.automata.transition]
step_next [in regexp.abstract.automata.simulation]
success_spec [in regexp.concrete.automata.simulation]
success_spec [in regexp.synthesis.clash.automata]
sum_proj [in regexp.concrete.function]

T

terminal_deadend [in regexp.abstract.automata.singleton]
thicken_many1 [in regexp.lang.world]
thicken_pow [in regexp.lang.world]
thicken_concat [in regexp.lang.world]
thicken_alt [in regexp.lang.world]
thicken_singleton [in regexp.lang.world]
thicken_epsilon [in regexp.lang.world]
to_proj2 [in regexp.concrete.function]
to_proj1 [in regexp.concrete.function]
to_map [in regexp.concrete.function]
to_plus_2 [in regexp.concrete.function]
to_plus_1 [in regexp.concrete.function]
to_from [in regexp.concrete.function]
transition_equality [in regexp.concrete.automata.singleton]
transition_equality [in regexp.concrete.automata.epsilon]
transpose_spec [in regexp.concrete.function]
trivialpathP [in regexp.abstract.automata.path]

U

unconst_const [in regexp.concrete.function]
union_spec [in regexp.synthesis.clash.subset]
union_spec [in regexp.concrete.subset]
union_empty_l [in regexp.concrete.subset]
union_empty_r [in regexp.concrete.subset]
unReachableLR [in regexp.abstract.automata.path]
unReachableRL [in regexp.abstract.automata.path]
unsum_sum [in regexp.concrete.function]

W

wpath_nexts [in regexp.abstract.automata.simulation]
wpath_uncons [in regexp.abstract.automata.world]
wpath_nilE [in regexp.abstract.automata.world]

Z

zipWith_mapR [in regexp.concrete.function]
zip_pointwise4 [in regexp.concrete.function]
zip_pointwise3 [in regexp.concrete.function]
zip_pointwise [in regexp.concrete.function]

Constructor Index

A

alt [in regexp.expr]

B

Bind [in regexp.syn]

C

concat [in regexp.concrete.function]
concat [in regexp.expr]
const [in regexp.concrete.function]
CoProd [in regexp.concrete.universe]

E

eps [in regexp.expr]

M

many1 [in regexp.expr]

R

Ret [in regexp.syn]

S

single [in regexp.expr]

U

Unit [in regexp.concrete.universe]

Projection Index

A

atomTable [in regexp.concrete.rule]

F

final [in regexp.abstract.automata]
final [in regexp.concrete.automata]
final [in regexp.synthesis.clash.automata]

L

letter [in regexp.concrete.rule]

N

nfa [in regexp.synthesis]

R

regexp [in regexp.concrete.rule]

S

scanTable [in regexp.synthesis]
start [in regexp.abstract.automata]
start [in regexp.concrete.automata]
start [in regexp.synthesis.clash.automata]

T

trans [in regexp.abstract.automata]
trans [in regexp.concrete.automata]
trans [in regexp.synthesis.clash.automata]

Inductive Index

S

sort [in regexp.concrete.universe]

T

t [in regexp.concrete.function]
t [in regexp.syn]
t [in regexp.expr]

Section Index

A

access.Cxt [in regexp.abstract.automata.path]

B

BigSyn [in regexp.synthesis.clash.subset]
big.Cxt [in regexp.synthesis.clash.subset]
big.Cxt [in regexp.concrete.subset]
Build [in regexp.concrete.automata.alt]

C

Comap [in regexp.lang]
consistent.left.Cxt [in regexp.lang.world]
consistent.right.Cxt [in regexp.lang.world]
Correctness [in regexp.synthesis]
Cxt [in regexp.concrete.automata.concat]
Cxt [in regexp.abstract.utils]
Cxt [in regexp.abstract.automata.build]
Cxt [in regexp.abstract.automata.alt]
Cxt [in regexp.abstract.automata.oneOrMore]
Cxt [in regexp.concrete.automata.alt]
Cxt [in regexp.abstract.automata.path]
Cxt [in regexp.concrete.automata.oneOrMore]
Cxt [in regexp.concrete.automata.build]
Cxt [in regexp.concrete.rule]
Cxt [in regexp.concrete.rule]
Cxt [in regexp.abstract.automata.concat]

D

DecEq [in regexp.abstract.automata]
Defn [in regexp.synthesis.clash.automata]

E

Epsilon [in regexp.concrete.automata.epsilon]
EqFun [in regexp.prelude]
Equiv [in regexp.abstract.automata]
eq.Cxt [in regexp.lang]

F

FoldMap [in regexp.concrete.function]

H

hb_instance_1.hb_instance_1 [in regexp.abstract.automata]

M

Map [in regexp.prelude]
Matrix [in regexp.concrete.relation]
Matrix [in regexp.abstract.automata.path]
Matrix [in regexp.abstract.automata.transition]
Matrix [in regexp.abstract.relation]

P

Path [in regexp.abstract.automata.path]
PathThickening [in regexp.abstract.automata.world]

S

Simulation [in regexp.abstract.automata.simulation]
Syn [in regexp.synthesis.clash.subset]
Synthesis [in regexp.synthesis.clash.relation]
Synthesis [in regexp.synthesis.clash.automata]

T

Thickening [in regexp.lang.world]
Transition [in regexp.abstract.automata.singleton]
Transition [in regexp.abstract.automata.epsilon]

Z

ZipWithMap [in regexp.concrete.function]
ZipWithMap.Right [in regexp.concrete.function]

Definition Index

A

accept [in regexp.synthesis]
accept [in regexp.abstract.automata]
accept [in regexp.concrete.automata.simulation]
accept [in regexp.abstract.automata.simulation]
accept [in regexp.concrete.automata]
accept [in regexp.synthesis.clash.automata]
access.cons [in regexp.abstract.automata.path]
access.from [in regexp.abstract.automata.path]
access.single_from [in regexp.abstract.automata.path]
access.single_to [in regexp.abstract.automata.path]
access.to [in regexp.abstract.automata.path]
alphabet [in regexp.syn]
alt [in regexp.lang]
and [in regexp.concrete.relation]
andC [in regexp.synthesis.clash.constraint]
any [in regexp.byte]
attach [in regexp.syn]
automata_NFA__canonical__eqtype_Equality [in regexp.abstract.automata]

B

between [in regexp.byte]
big.intersection [in regexp.synthesis.clash.subset]
big.intersection [in regexp.concrete.subset]
big.union [in regexp.synthesis.clash.subset]
big.union [in regexp.concrete.subset]
binary.img [in regexp.synthesis.clash.relation]
binary.t [in regexp.concrete.relation]
binary.t [in regexp.abstract.relation]
binary.t [in regexp.synthesis.clash.relation]
build [in regexp.abstract.automata.singleton]
build [in regexp.concrete.automata.concat]
build [in regexp.concrete.automata.singleton]
build [in regexp.abstract.automata.alt]
build [in regexp.abstract.automata.epsilon]
build [in regexp.abstract.automata.oneOrMore]
build [in regexp.concrete.automata.alt]
build [in regexp.concrete.automata.oneOrMore]
build [in regexp.concrete.automata.epsilon]
build [in regexp.abstract.automata.concat]

C

char [in regexp.byte]
comap [in regexp.lang]
compile [in regexp.syn]
compose [in regexp.concrete.relation]
concat [in regexp.lang]
consistent.rel [in regexp.lang.world]
constant [in regexp.concrete.function]
consume [in regexp.concrete.automata.simulation]
consume [in regexp.abstract.automata.simulation]
consume [in regexp.synthesis.clash.automata]
cover [in regexp.abstract.automata.path]
crossing [in regexp.concrete.automata.concat]
crossRel [in regexp.concrete.automata.concat]

D

deadEnd [in regexp.abstract.automata.path]
denote [in regexp.concrete.relation]
denote [in regexp.concrete.function]
denote [in regexp.concrete.subset]
denote [in regexp.syn]
denote [in regexp.concrete.universe]
denote [in regexp.concrete.automata]
diagonal [in regexp.concrete.relation]
diagonal [in regexp.abstract.automata.transition]
diagonal [in regexp.abstract.relation]
disjoint_union [in regexp.synthesis.clash.subset]
disjoint_union [in regexp.concrete.subset]

E

empty [in regexp.concrete.relation]
empty [in regexp.synthesis.clash.subset]
empty [in regexp.concrete.subset]
empty [in regexp.abstract.relation]
emptyRel [in regexp.concrete.automata.singleton]
encode [in regexp.concrete.rule]
epsilon [in regexp.lang]
eqnfa [in regexp.abstract.automata]
equiv [in regexp.abstract.automata]
eq.rel [in regexp.lang]
eval [in regexp.expr]

F

fill [in regexp.syn]
filled [in regexp.syn]
final0 [in regexp.concrete.automata.concat]
final0 [in regexp.abstract.automata.concat]
final1 [in regexp.concrete.automata.concat]
final1 [in regexp.abstract.automata.concat]
fold [in regexp.concrete.function]
foo [in regexp.syn]
from [in regexp.concrete.function]
full [in regexp.concrete.relation]
full [in regexp.synthesis.clash.subset]
full [in regexp.concrete.subset]
full [in regexp.abstract.relation]

H

hasfinal0 [in regexp.concrete.automata.concat]
hasfinal0 [in regexp.abstract.automata.concat]

I

ifeq [in regexp.concrete.function]
iLanguage [in regexp.concrete.rule]
img [in regexp.concrete.relation]
img [in regexp.abstract.relation]
img [in regexp.synthesis.clash.relation]
inhabited [in regexp.abstract.utils]
inhabited [in regexp.synthesis.clash.subset]
inhabited [in regexp.concrete.subset]
inhabitedP [in regexp.abstract.utils]
initial [in regexp.abstract.automata.singleton]
initial [in regexp.concrete.automata.concat]
initial [in regexp.concrete.automata.singleton]
initial [in regexp.abstract.automata.oneOrMore]
initial [in regexp.concrete.automata.oneOrMore]
initial [in regexp.abstract.automata.concat]
injl [in regexp.concrete.subset]
injr [in regexp.concrete.subset]
internal.alloc [in regexp.syn]
internal.compile [in regexp.syn]
internal.denote [in regexp.syn]
interpret [in regexp.concrete.rule]
intersection [in regexp.synthesis.clash.subset]
intersection [in regexp.concrete.subset]
isAlpha [in regexp.byte]
isAlphaNum [in regexp.byte]
isAscii [in regexp.byte]
isDigit [in regexp.byte]
isFinal [in regexp.synthesis]
isSmallAlpha [in regexp.byte]

L

lang [in regexp.lang]
language [in regexp.expr]
language [in regexp.concrete.rule]
lift [in regexp.synthesis.clash.universe]

M

makeRule [in regexp.syn]
many [in regexp.lang]
many [in regexp.expr]
many1 [in regexp.lang]
map [in regexp.concrete.function]
map [in regexp.expr]
mapper [in regexp.synthesis]
matcher_of [in regexp.concrete.rule]
matcher.language [in regexp.expr]
matcher.t [in regexp.expr]
matrix [in regexp.concrete.relation]
matrix [in regexp.abstract.relation]
mkTrans [in regexp.abstract.automata.singleton]
mkTrans [in regexp.concrete.automata.concat]
mkTrans [in regexp.concrete.automata.singleton]
mkTrans [in regexp.abstract.automata.oneOrMore]
mkTrans [in regexp.concrete.automata.alt]
mkTrans [in regexp.concrete.automata.oneOrMore]
mkTrans [in regexp.abstract.automata.concat]
mLanguage [in regexp.concrete.rule]

N

neighbours [in regexp.abstract.automata.transition]
next [in regexp.concrete.automata.simulation]
next [in regexp.abstract.automata.simulation]
next [in regexp.synthesis.clash.automata]
nexts [in regexp.abstract.automata.simulation]
nfaeqdec [in regexp.abstract.automata]
nilP [in regexp.abstract.automata.path]
nopathP [in regexp.abstract.automata.path]

O

oneOf [in regexp.byte]
or [in regexp.concrete.relation]

P

pow [in regexp.lang]
predlift [in regexp.synthesis.clash.universe]
prefinal0 [in regexp.abstract.automata.concat]
process [in regexp.concrete.automata.simulation]
process [in regexp.abstract.automata.simulation]
process [in regexp.synthesis.clash.automata]
proj1 [in regexp.concrete.function]
proj2 [in regexp.concrete.function]

R

reach [in regexp.abstract.automata.oneOrMore]
reachable [in regexp.abstract.automata.path]
reject [in regexp.synthesis]
rel01 [in regexp.concrete.automata.concat]
rel01 [in regexp.abstract.automata.concat]
re2nfa [in regexp.abstract.automata.build]
re2nfa [in regexp.concrete.automata.build]
runOnList [in regexp.synthesis]

S

satisfy [in regexp.lang]
scanner [in regexp.synthesis]
singleton [in regexp.lang]
singleton [in regexp.concrete.subset]
sortOf [in regexp.syn]
sort_sind [in regexp.concrete.universe]
sort_rec [in regexp.concrete.universe]
sort_ind [in regexp.concrete.universe]
sort_rect [in regexp.concrete.universe]
split [in regexp.syn]
start [in regexp.synthesis]
startBack [in regexp.abstract.automata.oneOrMore]
startBack [in regexp.concrete.automata.oneOrMore]
start0 [in regexp.concrete.automata.concat]
start0 [in regexp.abstract.automata.concat]
start1 [in regexp.concrete.automata.concat]
start1 [in regexp.abstract.automata.concat]
State [in regexp.abstract.automata.singleton]
State [in regexp.concrete.automata.concat]
State [in regexp.abstract.utils]
state [in regexp.synthesis]
State [in regexp.concrete.automata.singleton]
State [in regexp.abstract.automata.build]
State [in regexp.abstract.automata.alt]
State [in regexp.abstract.automata.epsilon]
State [in regexp.concrete.automata.alt]
State [in regexp.concrete.automata.epsilon]
State [in regexp.concrete.automata.build]
State [in regexp.abstract.automata.concat]
step [in regexp.abstract.automata.transition]
success [in regexp.concrete.automata.simulation]
success [in regexp.abstract.automata.simulation]
success [in regexp.synthesis.clash.automata]
syn [in regexp.synthesis.clash.function]
syn [in regexp.synthesis.clash.subset]
syn [in regexp.synthesis.clash.relation]
syn [in regexp.synthesis.clash.automata]
synthesize [in regexp.synthesis]

T

t [in regexp.concrete.relation]
t [in regexp.synthesis.clash.subset]
t [in regexp.abstract.automata.path]
t [in regexp.abstract.automata.transition]
t [in regexp.concrete.subset]
T [in regexp.syn]
t [in regexp.abstract.relation]
t [in regexp.synthesis.clash.relation]
terminal [in regexp.abstract.automata.singleton]
terminal [in regexp.concrete.automata.concat]
terminal [in regexp.concrete.automata.singleton]
terminal [in regexp.abstract.automata.oneOrMore]
terminal [in regexp.concrete.automata.oneOrMore]
terminal [in regexp.abstract.automata.concat]
thicken [in regexp.lang.world]
to [in regexp.concrete.function]
tr [in regexp.abstract.automata.epsilon]
tr [in regexp.abstract.automata.oneOrMore]
tr [in regexp.abstract.automata.path]
tr [in regexp.abstract.automata.transition]
tr [in regexp.concrete.automata.oneOrMore]
transition [in regexp.synthesis]
transition.denote [in regexp.concrete.automata]
transition.syn [in regexp.synthesis.clash.automata]
transition.t [in regexp.concrete.automata]
transition.t [in regexp.synthesis.clash.automata]
transpose [in regexp.concrete.function]
tr0 [in regexp.abstract.automata.concat]
tr1 [in regexp.abstract.automata.concat]
typ [in regexp.synthesis.clash.constraint]
typeOf [in regexp.concrete.universe]
t_sind [in regexp.concrete.function]
t_rec [in regexp.concrete.function]
t_ind [in regexp.concrete.function]
t_rect [in regexp.concrete.function]
t_sind [in regexp.syn]
t_rec [in regexp.syn]
t_ind [in regexp.syn]
t_rect [in regexp.syn]
t_sind [in regexp.expr]
t_rec [in regexp.expr]
t_ind [in regexp.expr]
t_rect [in regexp.expr]

U

unbind [in regexp.syn]
unconst [in regexp.concrete.function]
union [in regexp.synthesis.clash.subset]
union [in regexp.concrete.subset]
unnest [in regexp.expr]
unret [in regexp.syn]
unsum [in regexp.concrete.function]
utmatrix [in regexp.abstract.automata.transition]

V

vars [in regexp.syn]

W

wAccept [in regexp.abstract.automata.world]
wLanguage [in regexp.concrete.rule]
world [in regexp.lang.world]
wpath [in regexp.abstract.automata.world]
wreachable [in regexp.abstract.automata.world]

Z

zipWith [in regexp.concrete.function]
zipWith3 [in regexp.concrete.function]
zipWith4 [in regexp.concrete.function]

Record Index

M

machine [in regexp.synthesis]

N

NFA [in regexp.abstract.automata]
NFA [in regexp.concrete.automata]
NFA [in regexp.synthesis.clash.automata]

R

Rule [in regexp.concrete.rule]

Global Index

J

Q

X

Y

_

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

_

(29 entries)

Module Index

D

F

G

H

J

K

L

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(14 entries)

Variable Index

G

I

J

K

L

N

O

Q

R

U

V

W

X

Y

_

other

(133 entries)

Library Index

D

G

H

I

J

K

M

N

Q

V

X

Y

Z

_

other

(42 entries)

Axiom Index

A

B

D

E

G

H

J

N

O

P

Q

R

V

W

X

Y

_

other

(17 entries)

Lemma Index

J

K

O

Q

V

X

Y

_

other

(214 entries)

Constructor Index

D

F

G

H

I

J

K

L

N

O

P

Q

T

V

W

X

Y

Z

_

other

(11 entries)

Projection Index

B

C

D

E

G

H

I

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(4 entries)

Section Index

G

I

J

K

L

N

O

Q

R

U

V

W

X

Y

_

other

(45 entries)

Definition Index

G

J

K

Q

X

Y

_

other

(265 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

This page has been generated by coqdoc