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]

eg

_{42}[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]

e

_{1}[definition, in QC.Typeclasses]

e

_{2}[definition, in QC.Typeclasses]

e

_{3}[definition, in QC.Typeclasses]

e

_{3}[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

PostScriptPreface

## Q

QCQuickChickInterface

QuickChickTool

## T

TImpTypeclasses

# 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

eg_{42}[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]

e

_{1}[in QC.Typeclasses]

e

_{2}[in QC.Typeclasses]

e

_{3}[in QC.Typeclasses]

e

_{3}[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) |