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 : _ (470 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 : _ (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 _ (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 _ (9 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 _ (36 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 _ (84 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 _ (6 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 _ (26 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 _ (29 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 _ (105 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 _ (1 entry)
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 _ (113 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (20 entries)

Global Index

A

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


B

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


C

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


D

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


E

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


F

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


G

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


H

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


I

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


L

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


M

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


N

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


O

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


P

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


Q

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


R

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


S

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


T

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


V

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


W

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


Y

Yellow [constructor, in QC.QC]


:

::x_'::='_x [notation, in QC.TImp]
::x_';;;'_x [notation, in QC.TImp]
::x_'=?'_x [notation, in QC.Typeclasses]
::x_'?' [notation, in QC.Typeclasses]
::x_'||-'_x_'\IN'_x [notation, in QC.TImp]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in QC.TImp]
::'SKIP' [notation, in QC.TImp]
::'WHILE'_x_'DO'_x_'END' [notation, in QC.TImp]



Notation Index

G

GenSTPlayground.::'genST'_x [in QC.TImp]


Q

QuickChickSig.QcDefaultNotation.:qc_scope:'elems'_'('_x_';;'_x_')' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'elems'_'['_x_';'_x_';'_'..'_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'elems'_'['_x_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'elems'_'['_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'freq'_'('_'('_x_','_x_')'_';;'_x_')' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'freq'_'['_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'freq'_'['_'('_x_','_x_')'_';'_x_';'_'..'_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'freq'_'['_'('_x_','_x_')'_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'oneOf'_'('_x_';;'_x_')' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'oneOf'_'['_x_';'_x_';'_'..'_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'oneOf'_'['_x_';'_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDefaultNotation.:qc_scope:'oneOf'_'['_x_']' [in QC.QuickChickInterface]
QuickChickSig.QcDoNotation.::'doM!'_x_'<-'_x_';'_x [in QC.QuickChickInterface]
QuickChickSig.QcDoNotation.::'do!'_x_'<-'_x_';'_x [in QC.QuickChickInterface]
QuickChickSig.QcDoNotation.::'do\'''_x_'<-'_x_';'_x [in QC.QuickChickInterface]
QuickChickSig.QcNotation.:Checker_scope:x_'==>'_x [in QC.QuickChickInterface]
QuickChickSig.::x_'?' [in QC.QuickChickInterface]
QuickChickSig.::'genST'_x [in QC.QuickChickInterface]


:

::x_'::='_x [in QC.TImp]
::x_';;;'_x [in QC.TImp]
::x_'=?'_x [in QC.Typeclasses]
::x_'?' [in QC.Typeclasses]
::x_'||-'_x_'\IN'_x [in QC.TImp]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in QC.TImp]
::'SKIP' [in QC.TImp]
::'WHILE'_x_'DO'_x_'END' [in QC.TImp]



Module Index

C

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


D

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


G

GenSTPlayground [in QC.TImp]


Q

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



Library Index

B

Bib


I

Introduction


P

PostScript
Preface


Q

QC
QuickChickInterface
QuickChickTool


T

TImp
Typeclasses



Axiom Index

C

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


E

every_color_is_red [in QC.QC]
expression_soundness [in QC.TImp]


Q

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


R

removeP [in QC.Introduction]


W

well_typed_state_never_stuck [in QC.TImp]



Constructor Index

A

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


B

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


C

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


D

DefineG.MkG [in QC.QC]


E

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


F

Fail [in QC.TImp]


G

Green [in QC.Typeclasses]
Green [in QC.QC]


I

Id [in QC.TImp]


L

Leaf [in QC.QC]
Left [in QC.QC]


M

Middle [in QC.QC]


N

Node [in QC.QC]


O

OutOfGas [in QC.TImp]


Q

QuickChickSig.MkArgs [in QC.QuickChickInterface]


R

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


S

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


T

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


V

VBool [in QC.TImp]
VNat [in QC.TImp]


Y

Yellow [in QC.QC]



Lemma Index

B

bind_deterministic [in QC.TImp]


C

commutativity_property [in QC.Typeclasses]


E

eqb_fact [in QC.Typeclasses]


H

has_type_deterministic [in QC.TImp]


T

trans3 [in QC.Typeclasses]
trans3_pre [in QC.Typeclasses]



Inductive Index

B

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


C

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


D

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


E

exp [in QC.QuickChickTool]
exp [in QC.TImp]


H

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


I

id [in QC.TImp]


P

primary [in QC.Typeclasses]


R

result [in QC.TImp]


S

sinstr [in QC.QuickChickTool]


T

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


V

value [in QC.TImp]


W

well_typed_com [in QC.TImp]
well_typed_state [in QC.TImp]



Projection Index

C

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


D

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


E

eqb [in QC.Typeclasses]
eqbad [in QC.Typeclasses]
eqb_eq [in QC.Typeclasses]


G

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


L

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


M

mymap [in QC.Typeclasses]


P

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


Q

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


R

reflexivity [in QC.Typeclasses]


S

show [in QC.Typeclasses]


T

transitivity [in QC.Typeclasses]



Instance Index

B

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


C

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


D

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


E

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


G

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


M

MyMap1 [in QC.Typeclasses]
MyMap2 [in QC.Typeclasses]
MyMap_trans [in QC.Typeclasses]


N

natOrd [in QC.Typeclasses]


O

optionMonad [in QC.Typeclasses]


Q

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


S

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



Section Index

G

GMonadDef [in QC.QC]



Definition Index

A

All [in QC.Typeclasses]


B

base [in QC.TImp]
base' [in QC.TImp]
bindGenOpt [in QC.TImp]


C

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


D

DefineSized.sized [in QC.QC]


E

eg42 [in QC.Typeclasses]
eqBar [in QC.Typeclasses]
eval [in QC.TImp]
eval [in QC.QuickChickTool]
execute [in QC.QuickChickTool]
expression_soundness_exec [in QC.TImp]
expression_soundness_exec' [in QC.TImp]
expression_soundness_exec_firstshrink [in QC.TImp]
e1 [in QC.Typeclasses]
e2 [in QC.Typeclasses]
e3 [in QC.Typeclasses]
e3 [in QC.Typeclasses]


F

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


G

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


I

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


L

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


M

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


N

nth_opt [in QC.Typeclasses]


O

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


P

path [in QC.QC]
path_mirror [in QC.QC]


Q

QuickChickSig.nl [in QC.QuickChickInterface]


R

r [in QC.Typeclasses]
remove [in QC.Introduction]


S

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


T

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



Record Index

C

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


D

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


E

Eq [in QC.Typeclasses]
EqDec [in QC.Typeclasses]


G

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


L

LabeledPoint [in QC.Typeclasses]


M

MyMap [in QC.Typeclasses]


O

Ord [in QC.Typeclasses]
OrdBad [in QC.Typeclasses]


P

Point [in QC.Typeclasses]
PreOrder [in QC.Typeclasses]


Q

QuickChickSig.Args [in QC.QuickChickInterface]


R

Reflexive [in QC.Typeclasses]


S

Show [in QC.Typeclasses]


T

Transitive [in QC.Typeclasses]



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 : _ (470 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 : _ (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 _ (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 _ (9 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 _ (36 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 _ (84 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 _ (6 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 _ (26 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 _ (29 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 _ (105 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 _ (1 entry)
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 _ (113 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (20 entries)