• 目录
• 索引

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

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

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

(14 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(84 entries)

Axiom 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)

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

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

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

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

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

(1 entry)

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

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

(113 entries)

---

Global Index

A

All [definition, in Typeclasses]
AMinus [constructor, in QuickChickTool]
AMult [constructor, in QuickChickTool]
ANum [constructor, in QuickChickTool]
APlus [constructor, in QuickChickTool]

B

Bar [constructor, in Typeclasses]
bar [inductive, in Typeclasses]
base [definition, in TImp]
base' [definition, in TImp]
Baz [constructor, in Typeclasses]
baz [inductive, in Typeclasses]
baz1 [instance, in Typeclasses]
baz2 [instance, in Typeclasses]
baz3 [instance, in Typeclasses]
baz4 [instance, in Typeclasses]
Bib [library]
Bind [constructor, in TImp]
bindGenOpt [definition, in TImp]
bind_deterministic [lemma, in TImp]
Blue [constructor, in Typeclasses]
Blue [constructor, in QC]
bound_to [inductive, in TImp]
Build_LabeledPoint [constructor, in Typeclasses]
Build_Point [constructor, in Typeclasses]

C

CAss [constructor, in TImp]
ceval [definition, in TImp]
CheckerPlayground1 [module, in QC]
CheckerPlayground1.Checkable [record, in QC]
CheckerPlayground1.checkableBool [instance, in QC]
CheckerPlayground1.checker [projection, in QC]
CheckerPlayground1.Checker [definition, in QC]
CheckerPlayground1.Failure [constructor, in QC]
CheckerPlayground1.Result [inductive, in QC]
CheckerPlayground1.showResult [instance, in QC]
CheckerPlayground1.Success [constructor, in QC]
CheckerPlayground2 [module, in QC]
CheckerPlayground2.checkableDec [instance, in QC]
CheckerPlayground2.c1 [axiom, in QC]
CheckerPlayground2.c2 [axiom, in QC]
CheckerPlayground3 [module, in QC]
CheckerPlayground3.forAll [definition, in QC]
CheckerPlayground4 [module, in QC]
CheckerPlayground4.Checkable [record, in QC]
CheckerPlayground4.checkableBool [instance, in QC]
CheckerPlayground4.checkableDec [instance, in QC]
CheckerPlayground4.checker [projection, in QC]
CheckerPlayground4.Checker [definition, in QC]
CheckerPlayground4.Failure [constructor, in QC]
CheckerPlayground4.forAll [definition, in QC]
CheckerPlayground4.Result [inductive, in QC]
CheckerPlayground4.showResult [instance, in QC]
CheckerPlayground4.showUnit [instance, in QC]
CheckerPlayground4.Success [constructor, in QC]
CIf [constructor, in TImp]
color [inductive, in QC]
com [inductive, in TImp]
commutativity_property [lemma, in Typeclasses]
compile [definition, in QuickChickTool]
compiles_correctly [definition, in QuickChickTool]
conditional_prop_example [axiom, in TImp]
context [definition, in TImp]
CSeq [constructor, in TImp]
CSkip [constructor, in TImp]
CWhile [constructor, in TImp]

D

dec [projection, in Typeclasses]
Dec [record, in Typeclasses]
Dec_conj [instance, in Typeclasses]
dec_well_typed_com [instance, in TImp]
dec_well_typed_state [instance, in TImp]
dec_has_type_value [instance, in TImp]
dec_has_type [instance, in TImp]
dec_bound_to [instance, in TImp]
dec_bound_to [instance, in TImp]
DefineArbitrary [module, in QC]
DefineArbitrary.Arbitrary [record, in QC]
DefineG [module, in QC]
DefineGen [module, in QC]
DefineGenSized [module, in QC]
DefineGenSized.arbitrarySized [projection, in QC]
DefineGenSized.GenOfGenSized [instance, in QC]
DefineGenSized.GenSized [record, in QC]
DefineGen.arbitrary [projection, in QC]
DefineGen.Gen [record, in QC]
DefineG.G [inductive, in QC]
DefineG.MkG [constructor, in QC]
DefineSized [module, in QC]
DefineSized.sized [definition, in QC]
direction [inductive, in QC]

E

EAnd [constructor, in TImp]
EEq [constructor, in TImp]
EFalse [constructor, in TImp]
eg₄₂ [definition, in Typeclasses]
ELe [constructor, in TImp]
EMinus [constructor, in TImp]
EMult [constructor, in TImp]
ENot [constructor, in TImp]
ENum [constructor, in TImp]
EPlus [constructor, in TImp]
Eq [record, in Typeclasses]
eqb [projection, in Typeclasses]
eqbad [projection, in Typeclasses]
eqBar [definition, in Typeclasses]
eqBool [instance, in Typeclasses]
eqb_fact [lemma, in Typeclasses]
eqb_eq [projection, in Typeclasses]
EqDec [record, in Typeclasses]
eqdecBool' [instance, in Typeclasses]
eqdecNat [instance, in Typeclasses]
EqDec__Dec [instance, in Typeclasses]
eqNat [instance, in Typeclasses]
eqPair [instance, in Typeclasses]
eq_dec_color [instance, in QC]
eq_dec_tern_tree [instance, in QC]
eq_dec_tree [instance, in QC]
eq_dec_ty [instance, in TImp]
eq_id_dec [instance, in TImp]
ETrue [constructor, in TImp]
eval [definition, in TImp]
eval [definition, in QuickChickTool]
EVar [constructor, in TImp]
every_color_is_red [axiom, in QC]
execute [definition, in QuickChickTool]
exp [inductive, in TImp]
exp [inductive, in QuickChickTool]
expression_soundness_exec' [definition, in TImp]
expression_soundness_exec_firstshrink [definition, in TImp]
expression_soundness_exec [definition, in TImp]
expression_soundness [axiom, in TImp]
e₁ [definition, in Typeclasses]
e₂ [definition, in Typeclasses]
e₃ [definition, in Typeclasses]
e₃ [definition, in Typeclasses]

F

Fail [constructor, in TImp]
faultyMirrorP [definition, in QC]
foo [definition, in Typeclasses]
fresh [definition, in TImp]

G

genColor [definition, in QC]
genColor' [definition, in QC]
genDirection [definition, in QC]
genPath [definition, in QC]
genSortedList [definition, in QC]
GenSTPlayground [module, in TImp]
GenSTPlayground.arbitrarySizeST [projection, in TImp]
GenSTPlayground.arbitraryST [projection, in TImp]
GenSTPlayground.GenSizedSuchThat [record, in TImp]
GenSTPlayground.GenSuchThat [record, in TImp]
GenSTPlayground.GenSuchThatOfBounded [instance, in TImp]
genST _ [notation, in TImp]
genTree [instance, in QC]
genTreeSized [definition, in QC]
genTreeSized' [definition, in QC]
gen_color [instance, in QC]
gen_well_typed_state [definition, in TImp]
gen_typed_value [definition, in TImp]
gen_typed_has_type [definition, in TImp]
gen_exp_typed_sized [definition, in TImp]
gen_has_type_3 [definition, in TImp]
gen_has_type_2 [definition, in TImp]
gen_typed_evar [definition, in TImp]
gen_context [definition, in TImp]
gen_typed_id_from_context [definition, in TImp]
get_fresh_ids [definition, in TImp]
GMonad [instance, in QC]
GMonadDef [section, in QC]
Green [constructor, in Typeclasses]
Green [constructor, in QC]

H

has_type_deterministic [lemma, in TImp]
has_type_value [inductive, in TImp]
has_type_3 [inductive, in TImp]
has_type_2 [inductive, in TImp]
has_type_1 [inductive, in TImp]
has_type [inductive, in TImp]

I

Id [constructor, in TImp]
id [inductive, in TImp]
implicit_fun1 [definition, in Typeclasses]
implicit_fun [definition, in Typeclasses]
insert [definition, in QC]
insert [definition, in Introduction]
insertBST [definition, in QC]
insertBST_spec' [definition, in QC]
insertBST_spec [definition, in QC]
insertBST' [definition, in QC]
insert_spec_sorted [definition, in QC]
insert_spec' [definition, in QC]
insert_spec [definition, in QC]
Introduction [library]
isBST [definition, in QC]
isFail [definition, in TImp]
isNone [definition, in TImp]
isRed [definition, in QC]

L

label [projection, in Typeclasses]
LabeledPoint [record, in Typeclasses]
le [projection, in Typeclasses]
Leaf [constructor, in QC]
lebad [projection, in Typeclasses]
Left [constructor, in QC]
liftM [definition, in Typeclasses]
liftM2 [definition, in Typeclasses]
liftM3 [definition, in Typeclasses]
lift_shrink [definition, in TImp]
lt [definition, in Typeclasses]
lx [projection, in Typeclasses]
ly [projection, in Typeclasses]

M

Map [definition, in TImp]
map_dom [definition, in TImp]
map_set [definition, in TImp]
map_get [definition, in TImp]
map_empty [definition, in TImp]
max [definition, in Typeclasses]
max [definition, in Typeclasses]
max_elt [definition, in TImp]
max1 [definition, in Typeclasses]
Middle [constructor, in QC]
mirror [definition, in QC]
mirrorP [definition, in QC]
mymap [projection, in Typeclasses]
MyMap [record, in Typeclasses]
MyMap_trans [instance, in Typeclasses]
MyMap1 [instance, in Typeclasses]
MyMap2 [instance, in Typeclasses]

N

natOrd [instance, in Typeclasses]
Node [constructor, in QC]
nth_opt [definition, in Typeclasses]

O

optimize [definition, in QuickChickTool]
optimize_correct_prop [definition, in QuickChickTool]
optionMonad [instance, in Typeclasses]
Ord [record, in Typeclasses]
OrdBad [record, in Typeclasses]
ordBarList [definition, in Typeclasses]
OutOfGas [constructor, in TImp]

P

path [definition, in QC]
path_mirror [definition, in QC]
Point [record, in Typeclasses]
Postscript [library]
Preface [library]
PreOrder [record, in Typeclasses]
PreOrder_Transitive [projection, in Typeclasses]
PreOrder_Reflexive [projection, in Typeclasses]
primary [inductive, in Typeclasses]
px [projection, in Typeclasses]
py [projection, in Typeclasses]

Q

QC [library]
QuickChickInterface [library]
QuickChickSig [module, in QuickChickInterface]
QuickChickSig.Applicative_G [instance, in QuickChickInterface]
QuickChickSig.ArbitraryOfGenShrink [instance, in QuickChickInterface]
QuickChickSig.Args [record, in QuickChickInterface]
QuickChickSig.backtrack [axiom, in QuickChickInterface]
QuickChickSig.bindGenOpt [axiom, in QuickChickInterface]
QuickChickSig.bindGen' [axiom, in QuickChickInterface]
QuickChickSig.chatty [projection, in QuickChickInterface]
QuickChickSig.Checker [axiom, in QuickChickInterface]
QuickChickSig.choose [axiom, in QuickChickInterface]
QuickChickSig.ChooseBool [instance, in QuickChickInterface]
QuickChickSig.ChooseNat [instance, in QuickChickInterface]
QuickChickSig.ChooseZ [instance, in QuickChickInterface]
QuickChickSig.collect [axiom, in QuickChickInterface]
QuickChickSig.conjoin [axiom, in QuickChickInterface]
QuickChickSig.Dec_string [instance, in QuickChickInterface]
QuickChickSig.Dec_ascii [instance, in QuickChickInterface]
QuickChickSig.Dec_eq_list [instance, in QuickChickInterface]
QuickChickSig.Dec_eq_prod [instance, in QuickChickInterface]
QuickChickSig.Dec_eq_opt [instance, in QuickChickInterface]
QuickChickSig.Dec_eq_nat [instance, in QuickChickInterface]
QuickChickSig.Dec_eq_bool [instance, in QuickChickInterface]
QuickChickSig.Dec_disj [instance, in QuickChickInterface]
QuickChickSig.Dec_conj [instance, in QuickChickInterface]
QuickChickSig.Dec_neg [instance, in QuickChickInterface]
QuickChickSig.disjoin [axiom, in QuickChickInterface]
QuickChickSig.elems_ [axiom, in QuickChickInterface]
QuickChickSig.Eq__Dec [instance, in QuickChickInterface]
QuickChickSig.expectFailure [axiom, in QuickChickInterface]
QuickChickSig.forAll [axiom, in QuickChickInterface]
QuickChickSig.forAllProof [axiom, in QuickChickInterface]
QuickChickSig.forAllShrink [axiom, in QuickChickInterface]
QuickChickSig.freq_ [axiom, in QuickChickInterface]
QuickChickSig.Functor_G [instance, in QuickChickInterface]
QuickChickSig.G [axiom, in QuickChickInterface]
QuickChickSig.genBoolSized [instance, in QuickChickInterface]
QuickChickSig.genList [instance, in QuickChickInterface]
QuickChickSig.genListSized [instance, in QuickChickInterface]
QuickChickSig.genNatSized [instance, in QuickChickInterface]
QuickChickSig.GenOfGenSized [instance, in QuickChickInterface]
QuickChickSig.genOption [instance, in QuickChickInterface]
QuickChickSig.genPair [instance, in QuickChickInterface]
QuickChickSig.genPairSized [instance, in QuickChickInterface]
QuickChickSig.genZSized [instance, in QuickChickInterface]
QuickChickSig.implication [axiom, in QuickChickInterface]
QuickChickSig.listOf [axiom, in QuickChickInterface]
QuickChickSig.maxDiscard [projection, in QuickChickInterface]
QuickChickSig.maxShrinks [projection, in QuickChickInterface]
QuickChickSig.maxSize [projection, in QuickChickInterface]
QuickChickSig.maxSuccess [projection, in QuickChickInterface]
QuickChickSig.MkArgs [constructor, in QuickChickInterface]
QuickChickSig.Monad_G [instance, in QuickChickInterface]
QuickChickSig.nl [definition, in QuickChickInterface]
QuickChickSig.oneOf_ [axiom, in QuickChickInterface]
QuickChickSig.OrdBool [instance, in QuickChickInterface]
QuickChickSig.OrdNat [instance, in QuickChickInterface]
QuickChickSig.OrdZ [instance, in QuickChickInterface]
QuickChickSig.QcDefaultNotation [module, in QuickChickInterface]
freq ( ( _ , _ ) ;; _ ) (qc_scope) [notation, in QuickChickInterface]
freq [ ( _ , _ ) ; _ ; .. ; _ ] (qc_scope) [notation, in QuickChickInterface]
freq [ ( _ , _ ) ; _ ] (qc_scope) [notation, in QuickChickInterface]
freq [ _ ] (qc_scope) [notation, in QuickChickInterface]
oneOf ( _ ;; _ ) (qc_scope) [notation, in QuickChickInterface]
oneOf [ _ ; _ ; .. ; _ ] (qc_scope) [notation, in QuickChickInterface]
oneOf [ _ ; _ ] (qc_scope) [notation, in QuickChickInterface]
oneOf [ _ ] (qc_scope) [notation, in QuickChickInterface]
elems ( _ ;; _ ) (qc_scope) [notation, in QuickChickInterface]
elems [ _ ; _ ; .. ; _ ] (qc_scope) [notation, in QuickChickInterface]
elems [ _ ; _ ] (qc_scope) [notation, in QuickChickInterface]
elems [ _ ] (qc_scope) [notation, in QuickChickInterface]
QuickChickSig.QcDoNotation [module, in QuickChickInterface]
doM! _ <- _ ; _ [notation, in QuickChickInterface]
do! _ <- _ ; _ [notation, in QuickChickInterface]
do\' _ <- _ ; _ [notation, in QuickChickInterface]
QuickChickSig.QcNotation [module, in QuickChickInterface]
_ ==> _ (Checker_scope) [notation, in QuickChickInterface]
QuickChickSig.RandomSeed [axiom, in QuickChickInterface]
QuickChickSig.replay [projection, in QuickChickInterface]
QuickChickSig.resize [axiom, in QuickChickInterface]
QuickChickSig.run [axiom, in QuickChickInterface]
QuickChickSig.semGen [axiom, in QuickChickInterface]
QuickChickSig.semGenSize [axiom, in QuickChickInterface]
QuickChickSig.showBool [instance, in QuickChickInterface]
QuickChickSig.showEx [instance, in QuickChickInterface]
QuickChickSig.showList [instance, in QuickChickInterface]
QuickChickSig.showNat [instance, in QuickChickInterface]
QuickChickSig.showOpt [instance, in QuickChickInterface]
QuickChickSig.showPair [instance, in QuickChickInterface]
QuickChickSig.showString [instance, in QuickChickInterface]
QuickChickSig.showZ [instance, in QuickChickInterface]
QuickChickSig.shrinkBool [instance, in QuickChickInterface]
QuickChickSig.shrinkList [instance, in QuickChickInterface]
QuickChickSig.shrinkNat [instance, in QuickChickInterface]
QuickChickSig.shrinkOption [instance, in QuickChickInterface]
QuickChickSig.shrinkPair [instance, in QuickChickInterface]
QuickChickSig.shrinkZ [instance, in QuickChickInterface]
QuickChickSig.sized [axiom, in QuickChickInterface]
QuickChickSig.suchThatMaybe [axiom, in QuickChickInterface]
QuickChickSig.suchThatMaybeOpt [axiom, in QuickChickInterface]
QuickChickSig.tag [axiom, in QuickChickInterface]
QuickChickSig.testBool [instance, in QuickChickInterface]
QuickChickSig.testDec [instance, in QuickChickInterface]
QuickChickSig.testFun [instance, in QuickChickInterface]
QuickChickSig.testPolyFun [instance, in QuickChickInterface]
QuickChickSig.testProd [instance, in QuickChickInterface]
QuickChickSig.testUnit [instance, in QuickChickInterface]
QuickChickSig.vectorOf [axiom, in QuickChickInterface]
QuickChickSig.whenFail [axiom, in QuickChickInterface]
_ ? [notation, in QuickChickInterface]
genST _ [notation, in QuickChickInterface]
QuickChickTool [library]

R

r [definition, in Typeclasses]
Red [constructor, in Typeclasses]
Red [constructor, in QC]
Reflexive [record, in Typeclasses]
reflexivity [projection, in Typeclasses]
remove [definition, in Introduction]
removeP [axiom, in Introduction]
result [inductive, in TImp]
Right [constructor, in QC]

S

show [projection, in Typeclasses]
Show [record, in Typeclasses]
showBool [instance, in Typeclasses]
showDirection [instance, in QC]
showList [instance, in Typeclasses]
showListAux [definition, in Typeclasses]
showNat [instance, in Typeclasses]
showOne [definition, in Typeclasses]
showOne1 [definition, in Typeclasses]
showOne2 [definition, in Typeclasses]
showOne3 [definition, in Typeclasses]
showOne4 [definition, in Typeclasses]
showPair [instance, in Typeclasses]
showPath [instance, in QC]
showPrimary [instance, in Typeclasses]
showTree [instance, in QC]
showTwo [definition, in Typeclasses]
show_color [instance, in QC]
show_id [instance, in TImp]
shrinkColor [instance, in QC]
shrinkDirection [instance, in QC]
shrinkId [instance, in TImp]
shrinkPath [instance, in QC]
shrinkTree [instance, in QC]
shrinkTreeAux [definition, in QC]
shrink_typed_has_type [definition, in TImp]
shrink_exp_typed [definition, in TImp]
shrink_rec [definition, in TImp]
shrink_evar [definition, in TImp]
shrink_base [definition, in TImp]
silly_fun2 [definition, in Typeclasses]
silly_fun1 [definition, in Typeclasses]
sinstr [inductive, in QuickChickTool]
size [definition, in QC]
SMinus [constructor, in QuickChickTool]
SMult [constructor, in QuickChickTool]
sorted [definition, in QC]
SPlus [constructor, in QuickChickTool]
SPush [constructor, in QuickChickTool]
state [definition, in TImp]
string_of_nat [definition, in Typeclasses]
string_of_nat_aux [definition, in Typeclasses]
Success [constructor, in TImp]
sum3 [definition, in Typeclasses]
sum3opt [definition, in Typeclasses]
sum3opt' [definition, in Typeclasses]

T

TAss [constructor, in TImp]
TBool [constructor, in TImp]
TernaryTree [inductive, in QC]
tern_mirror_path_flip [definition, in QC]
tern_mirror [definition, in QC]
TIf [constructor, in TImp]
TImp [library]
TLeaf [constructor, in QC]
TNat [constructor, in TImp]
TNode [constructor, in QC]
Transitive [record, in Typeclasses]
transitivity [projection, in Typeclasses]
trans3 [lemma, in Typeclasses]
trans3_pre [lemma, in Typeclasses]
traverse_path [definition, in QC]
traverse_node [definition, in QC]
Tree [inductive, in QC]
treeProp [definition, in QC]
TSeq [constructor, in TImp]
TSkip [constructor, in TImp]
TS_Elem [constructor, in TImp]
TS_Empty [constructor, in TImp]
TWhile [constructor, in TImp]
ty [inductive, in TImp]
Typeclasses [library]
TyVBool [constructor, in TImp]
TyVNat [constructor, in TImp]
Ty_Plus3 [constructor, in TImp]
Ty_Var3 [constructor, in TImp]
Ty_False2 [constructor, in TImp]
Ty_True2 [constructor, in TImp]
Ty_Num2 [constructor, in TImp]
Ty_Var2 [constructor, in TImp]
Ty_Var1 [constructor, in TImp]
Ty_And [constructor, in TImp]
Ty_Not [constructor, in TImp]
Ty_Le [constructor, in TImp]
Ty_Eq [constructor, in TImp]
Ty_False [constructor, in TImp]
Ty_True [constructor, in TImp]
Ty_Mult [constructor, in TImp]
Ty_Minus [constructor, in TImp]
Ty_Plus [constructor, in TImp]
Ty_Num [constructor, in TImp]
Ty_Var [constructor, in TImp]

V

value [inductive, in TImp]
VBool [constructor, in TImp]
VNat [constructor, in TImp]

W

well_typed_state_never_stuck [axiom, in TImp]
well_typed_com [inductive, in TImp]
well_typed_state [inductive, in TImp]

Y

Yellow [constructor, in QC]

other

_ ? [notation, in Typeclasses]
_ =? _ [notation, in Typeclasses]
_ ;;; _ [notation, in TImp]
_ ::= _ [notation, in TImp]
_ |⊢ _ \IN _ [notation, in TImp]
SKIP [notation, in TImp]
TEST _ THEN _ ELSE _ FI [notation, in TImp]
WHILE _ DO _ END [notation, in TImp]

---

Notation Index

G

genST _ [in TImp]

Q

freq ( ( _ , _ ) ;; _ ) (qc_scope) [in QuickChickInterface]
freq [ ( _ , _ ) ; _ ; .. ; _ ] (qc_scope) [in QuickChickInterface]
freq [ ( _ , _ ) ; _ ] (qc_scope) [in QuickChickInterface]
freq [ _ ] (qc_scope) [in QuickChickInterface]
oneOf ( _ ;; _ ) (qc_scope) [in QuickChickInterface]
oneOf [ _ ; _ ; .. ; _ ] (qc_scope) [in QuickChickInterface]
oneOf [ _ ; _ ] (qc_scope) [in QuickChickInterface]
oneOf [ _ ] (qc_scope) [in QuickChickInterface]
elems ( _ ;; _ ) (qc_scope) [in QuickChickInterface]
elems [ _ ; _ ; .. ; _ ] (qc_scope) [in QuickChickInterface]
elems [ _ ; _ ] (qc_scope) [in QuickChickInterface]
elems [ _ ] (qc_scope) [in QuickChickInterface]
doM! _ <- _ ; _ [in QuickChickInterface]
do! _ <- _ ; _ [in QuickChickInterface]
do\' _ <- _ ; _ [in QuickChickInterface]
_ ==> _ (Checker_scope) [in QuickChickInterface]
_ ? [in QuickChickInterface]
genST _ [in QuickChickInterface]

other

_ ? [in Typeclasses]
_ =? _ [in Typeclasses]
_ ;;; _ [in TImp]
_ ::= _ [in TImp]
_ |⊢ _ \IN _ [in TImp]
SKIP [in TImp]
TEST _ THEN _ ELSE _ FI [in TImp]
WHILE _ DO _ END [in TImp]

---

Module Index

C

CheckerPlayground1 [in QC]
CheckerPlayground2 [in QC]
CheckerPlayground3 [in QC]
CheckerPlayground4 [in QC]

D

DefineArbitrary [in QC]
DefineG [in QC]
DefineGen [in QC]
DefineGenSized [in QC]
DefineSized [in QC]

G

GenSTPlayground [in TImp]

Q

QuickChickSig [in QuickChickInterface]
QuickChickSig.QcDefaultNotation [in QuickChickInterface]
QuickChickSig.QcDoNotation [in QuickChickInterface]
QuickChickSig.QcNotation [in QuickChickInterface]

---

Library Index

B

Bib

I

Introduction

P

Postscript
Preface

Q

QC
QuickChickInterface
QuickChickTool

T

TImp
Typeclasses

---

Constructor Index

A

AMinus [in QuickChickTool]
AMult [in QuickChickTool]
ANum [in QuickChickTool]
APlus [in QuickChickTool]

B

Bar [in Typeclasses]
Baz [in Typeclasses]
Bind [in TImp]
Blue [in Typeclasses]
Blue [in QC]
Build_LabeledPoint [in Typeclasses]
Build_Point [in Typeclasses]

C

CAss [in TImp]
CheckerPlayground1.Failure [in QC]
CheckerPlayground1.Success [in QC]
CheckerPlayground4.Failure [in QC]
CheckerPlayground4.Success [in QC]
CIf [in TImp]
CSeq [in TImp]
CSkip [in TImp]
CWhile [in TImp]

D

DefineG.MkG [in QC]

E

EAnd [in TImp]
EEq [in TImp]
EFalse [in TImp]
ELe [in TImp]
EMinus [in TImp]
EMult [in TImp]
ENot [in TImp]
ENum [in TImp]
EPlus [in TImp]
ETrue [in TImp]
EVar [in TImp]

F

Fail [in TImp]

G

Green [in Typeclasses]
Green [in QC]

I

Id [in TImp]

L

Leaf [in QC]
Left [in QC]

M

Middle [in QC]

N

Node [in QC]

O

OutOfGas [in TImp]

Q

QuickChickSig.MkArgs [in QuickChickInterface]

R

Red [in Typeclasses]
Red [in QC]
Right [in QC]

S

SMinus [in QuickChickTool]
SMult [in QuickChickTool]
SPlus [in QuickChickTool]
SPush [in QuickChickTool]
Success [in TImp]

T

TAss [in TImp]
TBool [in TImp]
TIf [in TImp]
TLeaf [in QC]
TNat [in TImp]
TNode [in QC]
TSeq [in TImp]
TSkip [in TImp]
TS_Elem [in TImp]
TS_Empty [in TImp]
TWhile [in TImp]
TyVBool [in TImp]
TyVNat [in TImp]
Ty_Plus3 [in TImp]
Ty_Var3 [in TImp]
Ty_False2 [in TImp]
Ty_True2 [in TImp]
Ty_Num2 [in TImp]
Ty_Var2 [in TImp]
Ty_Var1 [in TImp]
Ty_And [in TImp]
Ty_Not [in TImp]
Ty_Le [in TImp]
Ty_Eq [in TImp]
Ty_False [in TImp]
Ty_True [in TImp]
Ty_Mult [in TImp]
Ty_Minus [in TImp]
Ty_Plus [in TImp]
Ty_Num [in TImp]
Ty_Var [in TImp]

V

VBool [in TImp]
VNat [in TImp]

Y

Yellow [in QC]

---

Axiom Index

C

CheckerPlayground2.c1 [in QC]
CheckerPlayground2.c2 [in QC]
conditional_prop_example [in TImp]

E

every_color_is_red [in QC]
expression_soundness [in TImp]

Q

QuickChickSig.backtrack [in QuickChickInterface]
QuickChickSig.bindGenOpt [in QuickChickInterface]
QuickChickSig.bindGen' [in QuickChickInterface]
QuickChickSig.Checker [in QuickChickInterface]
QuickChickSig.choose [in QuickChickInterface]
QuickChickSig.collect [in QuickChickInterface]
QuickChickSig.conjoin [in QuickChickInterface]
QuickChickSig.disjoin [in QuickChickInterface]
QuickChickSig.elems_ [in QuickChickInterface]
QuickChickSig.expectFailure [in QuickChickInterface]
QuickChickSig.forAll [in QuickChickInterface]
QuickChickSig.forAllProof [in QuickChickInterface]
QuickChickSig.forAllShrink [in QuickChickInterface]
QuickChickSig.freq_ [in QuickChickInterface]
QuickChickSig.G [in QuickChickInterface]
QuickChickSig.implication [in QuickChickInterface]
QuickChickSig.listOf [in QuickChickInterface]
QuickChickSig.oneOf_ [in QuickChickInterface]
QuickChickSig.RandomSeed [in QuickChickInterface]
QuickChickSig.resize [in QuickChickInterface]
QuickChickSig.run [in QuickChickInterface]
QuickChickSig.semGen [in QuickChickInterface]
QuickChickSig.semGenSize [in QuickChickInterface]
QuickChickSig.sized [in QuickChickInterface]
QuickChickSig.suchThatMaybe [in QuickChickInterface]
QuickChickSig.suchThatMaybeOpt [in QuickChickInterface]
QuickChickSig.tag [in QuickChickInterface]
QuickChickSig.vectorOf [in QuickChickInterface]
QuickChickSig.whenFail [in QuickChickInterface]

R

removeP [in Introduction]

W

well_typed_state_never_stuck [in TImp]

---

Lemma Index

B

bind_deterministic [in TImp]

C

commutativity_property [in Typeclasses]

E

eqb_fact [in Typeclasses]

H

has_type_deterministic [in TImp]

T

trans3 [in Typeclasses]
trans3_pre [in Typeclasses]

---

Projection Index

C

CheckerPlayground1.checker [in QC]
CheckerPlayground4.checker [in QC]

D

dec [in Typeclasses]
DefineGenSized.arbitrarySized [in QC]
DefineGen.arbitrary [in QC]

E

eqb [in Typeclasses]
eqbad [in Typeclasses]
eqb_eq [in Typeclasses]

G

GenSTPlayground.arbitrarySizeST [in TImp]
GenSTPlayground.arbitraryST [in TImp]

L

label [in Typeclasses]
le [in Typeclasses]
lebad [in Typeclasses]
lx [in Typeclasses]
ly [in Typeclasses]

M

mymap [in Typeclasses]

P

PreOrder_Transitive [in Typeclasses]
PreOrder_Reflexive [in Typeclasses]
px [in Typeclasses]
py [in Typeclasses]

Q

QuickChickSig.chatty [in QuickChickInterface]
QuickChickSig.maxDiscard [in QuickChickInterface]
QuickChickSig.maxShrinks [in QuickChickInterface]
QuickChickSig.maxSize [in QuickChickInterface]
QuickChickSig.maxSuccess [in QuickChickInterface]
QuickChickSig.replay [in QuickChickInterface]

R

reflexivity [in Typeclasses]

S

show [in Typeclasses]

T

transitivity [in Typeclasses]

---

Inductive Index

B

bar [in Typeclasses]
baz [in Typeclasses]
bound_to [in TImp]

C

CheckerPlayground1.Result [in QC]
CheckerPlayground4.Result [in QC]
color [in QC]
com [in TImp]

D

DefineG.G [in QC]
direction [in QC]

E

exp [in TImp]
exp [in QuickChickTool]

H

has_type_value [in TImp]
has_type_3 [in TImp]
has_type_2 [in TImp]
has_type_1 [in TImp]
has_type [in TImp]

I

id [in TImp]

P

primary [in Typeclasses]

R

result [in TImp]

S

sinstr [in QuickChickTool]

T

TernaryTree [in QC]
Tree [in QC]
ty [in TImp]

V

value [in TImp]

W

well_typed_com [in TImp]
well_typed_state [in TImp]

---

Instance Index

B

baz1 [in Typeclasses]
baz2 [in Typeclasses]
baz3 [in Typeclasses]
baz4 [in Typeclasses]

C

CheckerPlayground1.checkableBool [in QC]
CheckerPlayground1.showResult [in QC]
CheckerPlayground2.checkableDec [in QC]
CheckerPlayground4.checkableBool [in QC]
CheckerPlayground4.checkableDec [in QC]
CheckerPlayground4.showResult [in QC]
CheckerPlayground4.showUnit [in QC]

D

Dec_conj [in Typeclasses]
dec_well_typed_com [in TImp]
dec_well_typed_state [in TImp]
dec_has_type_value [in TImp]
dec_has_type [in TImp]
dec_bound_to [in TImp]
dec_bound_to [in TImp]
DefineGenSized.GenOfGenSized [in QC]

E

eqBool [in Typeclasses]
eqdecBool' [in Typeclasses]
eqdecNat [in Typeclasses]
EqDec__Dec [in Typeclasses]
eqNat [in Typeclasses]
eqPair [in Typeclasses]
eq_dec_color [in QC]
eq_dec_tern_tree [in QC]
eq_dec_tree [in QC]
eq_dec_ty [in TImp]
eq_id_dec [in TImp]

G

GenSTPlayground.GenSuchThatOfBounded [in TImp]
genTree [in QC]
gen_color [in QC]
GMonad [in QC]

M

MyMap_trans [in Typeclasses]
MyMap1 [in Typeclasses]
MyMap2 [in Typeclasses]

N

natOrd [in Typeclasses]

O

optionMonad [in Typeclasses]

Q

QuickChickSig.Applicative_G [in QuickChickInterface]
QuickChickSig.ArbitraryOfGenShrink [in QuickChickInterface]
QuickChickSig.ChooseBool [in QuickChickInterface]
QuickChickSig.ChooseNat [in QuickChickInterface]
QuickChickSig.ChooseZ [in QuickChickInterface]
QuickChickSig.Dec_string [in QuickChickInterface]
QuickChickSig.Dec_ascii [in QuickChickInterface]
QuickChickSig.Dec_eq_list [in QuickChickInterface]
QuickChickSig.Dec_eq_prod [in QuickChickInterface]
QuickChickSig.Dec_eq_opt [in QuickChickInterface]
QuickChickSig.Dec_eq_nat [in QuickChickInterface]
QuickChickSig.Dec_eq_bool [in QuickChickInterface]
QuickChickSig.Dec_disj [in QuickChickInterface]
QuickChickSig.Dec_conj [in QuickChickInterface]
QuickChickSig.Dec_neg [in QuickChickInterface]
QuickChickSig.Eq__Dec [in QuickChickInterface]
QuickChickSig.Functor_G [in QuickChickInterface]
QuickChickSig.genBoolSized [in QuickChickInterface]
QuickChickSig.genList [in QuickChickInterface]
QuickChickSig.genListSized [in QuickChickInterface]
QuickChickSig.genNatSized [in QuickChickInterface]
QuickChickSig.GenOfGenSized [in QuickChickInterface]
QuickChickSig.genOption [in QuickChickInterface]
QuickChickSig.genPair [in QuickChickInterface]
QuickChickSig.genPairSized [in QuickChickInterface]
QuickChickSig.genZSized [in QuickChickInterface]
QuickChickSig.Monad_G [in QuickChickInterface]
QuickChickSig.OrdBool [in QuickChickInterface]
QuickChickSig.OrdNat [in QuickChickInterface]
QuickChickSig.OrdZ [in QuickChickInterface]
QuickChickSig.showBool [in QuickChickInterface]
QuickChickSig.showEx [in QuickChickInterface]
QuickChickSig.showList [in QuickChickInterface]
QuickChickSig.showNat [in QuickChickInterface]
QuickChickSig.showOpt [in QuickChickInterface]
QuickChickSig.showPair [in QuickChickInterface]
QuickChickSig.showString [in QuickChickInterface]
QuickChickSig.showZ [in QuickChickInterface]
QuickChickSig.shrinkBool [in QuickChickInterface]
QuickChickSig.shrinkList [in QuickChickInterface]
QuickChickSig.shrinkNat [in QuickChickInterface]
QuickChickSig.shrinkOption [in QuickChickInterface]
QuickChickSig.shrinkPair [in QuickChickInterface]
QuickChickSig.shrinkZ [in QuickChickInterface]
QuickChickSig.testBool [in QuickChickInterface]
QuickChickSig.testDec [in QuickChickInterface]
QuickChickSig.testFun [in QuickChickInterface]
QuickChickSig.testPolyFun [in QuickChickInterface]
QuickChickSig.testProd [in QuickChickInterface]
QuickChickSig.testUnit [in QuickChickInterface]

S

showBool [in Typeclasses]
showDirection [in QC]
showList [in Typeclasses]
showNat [in Typeclasses]
showPair [in Typeclasses]
showPath [in QC]
showPrimary [in Typeclasses]
showTree [in QC]
show_color [in QC]
show_id [in TImp]
shrinkColor [in QC]
shrinkDirection [in QC]
shrinkId [in TImp]
shrinkPath [in QC]
shrinkTree [in QC]

---

Section Index

G

GMonadDef [in QC]

---

Record Index

C

CheckerPlayground1.Checkable [in QC]
CheckerPlayground4.Checkable [in QC]

D

Dec [in Typeclasses]
DefineArbitrary.Arbitrary [in QC]
DefineGenSized.GenSized [in QC]
DefineGen.Gen [in QC]

E

Eq [in Typeclasses]
EqDec [in Typeclasses]

G

GenSTPlayground.GenSizedSuchThat [in TImp]
GenSTPlayground.GenSuchThat [in TImp]

L

LabeledPoint [in Typeclasses]

M

MyMap [in Typeclasses]

O

Ord [in Typeclasses]
OrdBad [in Typeclasses]

P

Point [in Typeclasses]
PreOrder [in Typeclasses]

Q

QuickChickSig.Args [in QuickChickInterface]

R

Reflexive [in Typeclasses]

S

Show [in Typeclasses]

T

Transitive [in Typeclasses]

---

Definition Index

A

All [in Typeclasses]

B

base [in TImp]
base' [in TImp]
bindGenOpt [in TImp]

C

ceval [in TImp]
CheckerPlayground1.Checker [in QC]
CheckerPlayground3.forAll [in QC]
CheckerPlayground4.Checker [in QC]
CheckerPlayground4.forAll [in QC]
compile [in QuickChickTool]
compiles_correctly [in QuickChickTool]
context [in TImp]

D

DefineSized.sized [in QC]

E

eg₄₂ [in Typeclasses]
eqBar [in Typeclasses]
eval [in TImp]
eval [in QuickChickTool]
execute [in QuickChickTool]
expression_soundness_exec' [in TImp]
expression_soundness_exec_firstshrink [in TImp]
expression_soundness_exec [in TImp]
e₁ [in Typeclasses]
e₂ [in Typeclasses]
e₃ [in Typeclasses]
e₃ [in Typeclasses]

F

faultyMirrorP [in QC]
foo [in Typeclasses]
fresh [in TImp]

G

genColor [in QC]
genColor' [in QC]
genDirection [in QC]
genPath [in QC]
genSortedList [in QC]
genTreeSized [in QC]
genTreeSized' [in QC]
gen_well_typed_state [in TImp]
gen_typed_value [in TImp]
gen_typed_has_type [in TImp]
gen_exp_typed_sized [in TImp]
gen_has_type_3 [in TImp]
gen_has_type_2 [in TImp]
gen_typed_evar [in TImp]
gen_context [in TImp]
gen_typed_id_from_context [in TImp]
get_fresh_ids [in TImp]

I

implicit_fun1 [in Typeclasses]
implicit_fun [in Typeclasses]
insert [in QC]
insert [in Introduction]
insertBST [in QC]
insertBST_spec' [in QC]
insertBST_spec [in QC]
insertBST' [in QC]
insert_spec_sorted [in QC]
insert_spec' [in QC]
insert_spec [in QC]
isBST [in QC]
isFail [in TImp]
isNone [in TImp]
isRed [in QC]

L

liftM [in Typeclasses]
liftM2 [in Typeclasses]
liftM3 [in Typeclasses]
lift_shrink [in TImp]
lt [in Typeclasses]

M

Map [in TImp]
map_dom [in TImp]
map_set [in TImp]
map_get [in TImp]
map_empty [in TImp]
max [in Typeclasses]
max [in Typeclasses]
max_elt [in TImp]
max1 [in Typeclasses]
mirror [in QC]
mirrorP [in QC]

N

nth_opt [in Typeclasses]

O

optimize [in QuickChickTool]
optimize_correct_prop [in QuickChickTool]
ordBarList [in Typeclasses]

P

path [in QC]
path_mirror [in QC]

Q

QuickChickSig.nl [in QuickChickInterface]

R

r [in Typeclasses]
remove [in Introduction]

S

showListAux [in Typeclasses]
showOne [in Typeclasses]
showOne1 [in Typeclasses]
showOne2 [in Typeclasses]
showOne3 [in Typeclasses]
showOne4 [in Typeclasses]
showTwo [in Typeclasses]
shrinkTreeAux [in QC]
shrink_typed_has_type [in TImp]
shrink_exp_typed [in TImp]
shrink_rec [in TImp]
shrink_evar [in TImp]
shrink_base [in TImp]
silly_fun2 [in Typeclasses]
silly_fun1 [in Typeclasses]
size [in QC]
sorted [in QC]
state [in TImp]
string_of_nat [in Typeclasses]
string_of_nat_aux [in Typeclasses]
sum3 [in Typeclasses]
sum3opt [in Typeclasses]
sum3opt' [in Typeclasses]

T

tern_mirror_path_flip [in QC]
tern_mirror [in QC]
traverse_path [in QC]
traverse_node [in QC]
treeProp [in QC]

---

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

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

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

(14 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(84 entries)

Axiom 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)

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

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

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

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

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

(1 entry)

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

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

(113 entries)

---

This page has been generated by coqdoc