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 | (1229 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) |

Binder 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 | (755 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 | (17 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 | (115 entries) |

# Global Index

## A

acc':14 [binder, in Typeclasses]acc:11 [binder, in Typeclasses]

All [definition, in Typeclasses]

al:3 [binder, in TImp]

al:6 [binder, in TImp]

AMinus [constructor, in QuickChickTool]

AMult [constructor, in QuickChickTool]

ANum [constructor, in QuickChickTool]

APlus [constructor, in QuickChickTool]

aux:16 [binder, in QC]

A:1 [binder, in QuickChickInterface]

A:1 [binder, in Typeclasses]

A:1 [binder, in QC]

A:101 [binder, in QC]

A:103 [binder, in Typeclasses]

A:106 [binder, in QuickChickInterface]

A:107 [binder, in QC]

A:108 [binder, in Typeclasses]

A:11 [binder, in QC]

A:113 [binder, in QuickChickInterface]

A:114 [binder, in Typeclasses]

A:120 [binder, in Typeclasses]

A:120 [binder, in TImp]

A:123 [binder, in QC]

A:125 [binder, in Typeclasses]

A:126 [binder, in QC]

A:132 [binder, in Typeclasses]

A:133 [binder, in QuickChickInterface]

A:134 [binder, in QC]

A:138 [binder, in QC]

A:139 [binder, in Typeclasses]

A:141 [binder, in QC]

A:143 [binder, in QC]

A:144 [binder, in Typeclasses]

A:15 [binder, in QuickChickInterface]

A:154 [binder, in Typeclasses]

A:164 [binder, in QuickChickInterface]

A:17 [binder, in QuickChickInterface]

A:17 [binder, in Typeclasses]

A:17 [binder, in QC]

A:172 [binder, in QuickChickInterface]

A:173 [binder, in QC]

A:178 [binder, in QuickChickInterface]

A:181 [binder, in Typeclasses]

A:188 [binder, in QuickChickInterface]

a:19 [binder, in Typeclasses]

A:20 [binder, in QuickChickInterface]

A:20 [binder, in Typeclasses]

A:22 [binder, in QC]

A:232 [binder, in TImp]

A:236 [binder, in Typeclasses]

A:238 [binder, in Typeclasses]

A:24 [binder, in QuickChickInterface]

a:24 [binder, in Typeclasses]

A:241 [binder, in Typeclasses]

A:247 [binder, in Typeclasses]

a:252 [binder, in Typeclasses]

A:26 [binder, in Typeclasses]

a:27 [binder, in QuickChickInterface]

A:27 [binder, in QC]

A:29 [binder, in QuickChickInterface]

A:3 [binder, in QuickChickInterface]

A:312 [binder, in TImp]

A:32 [binder, in QuickChickInterface]

A:33 [binder, in Typeclasses]

A:34 [binder, in QuickChickInterface]

A:35 [binder, in TImp]

A:36 [binder, in QuickChickInterface]

A:36 [binder, in TImp]

A:37 [binder, in TImp]

A:38 [binder, in QuickChickInterface]

a:38 [binder, in Typeclasses]

A:38 [binder, in QC]

A:388 [binder, in TImp]

A:392 [binder, in TImp]

A:396 [binder, in TImp]

A:40 [binder, in QuickChickInterface]

A:40 [binder, in Typeclasses]

A:42 [binder, in QuickChickInterface]

A:42 [binder, in TImp]

A:44 [binder, in QuickChickInterface]

A:46 [binder, in QuickChickInterface]

A:46 [binder, in TImp]

A:47 [binder, in QC]

A:48 [binder, in QuickChickInterface]

A:50 [binder, in QuickChickInterface]

A:50 [binder, in Typeclasses]

A:50 [binder, in TImp]

A:52 [binder, in QuickChickInterface]

a:52 [binder, in QC]

A:55 [binder, in QuickChickInterface]

A:55 [binder, in Typeclasses]

a:55 [binder, in TImp]

A:56 [binder, in TImp]

A:57 [binder, in QuickChickInterface]

A:58 [binder, in Typeclasses]

A:58 [binder, in QC]

A:59 [binder, in QuickChickInterface]

A:61 [binder, in QuickChickInterface]

A:62 [binder, in Typeclasses]

A:62 [binder, in QC]

A:63 [binder, in QuickChickInterface]

A:63 [binder, in TImp]

A:67 [binder, in QuickChickInterface]

A:67 [binder, in Typeclasses]

A:7 [binder, in QuickChickInterface]

A:70 [binder, in QC]

A:71 [binder, in QuickChickInterface]

A:71 [binder, in Typeclasses]

A:73 [binder, in QuickChickInterface]

a:76 [binder, in QC]

A:77 [binder, in QuickChickInterface]

A:77 [binder, in Typeclasses]

A:79 [binder, in QuickChickInterface]

a:79 [binder, in Typeclasses]

A:8 [binder, in QC]

A:80 [binder, in Typeclasses]

A:81 [binder, in QC]

a:82 [binder, in Typeclasses]

A:83 [binder, in QuickChickInterface]

A:83 [binder, in Typeclasses]

a:85 [binder, in Typeclasses]

a:88 [binder, in Typeclasses]

A:89 [binder, in Typeclasses]

A:89 [binder, in QC]

A:9 [binder, in QuickChickInterface]

A:90 [binder, in QuickChickInterface]

A:92 [binder, in QC]

A:95 [binder, in QC]

A:98 [binder, in QuickChickInterface]

## B

Bar [constructor, in Typeclasses]bar [inductive, in Typeclasses]

base [definition, in TImp]

base' [definition, in TImp]

base:173 [binder, 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]

B:121 [binder, in TImp]

b:149 [binder, in QuickChickInterface]

B:179 [binder, in QuickChickInterface]

b:207 [binder, in TImp]

B:21 [binder, in Typeclasses]

b:213 [binder, in TImp]

b:226 [binder, in Typeclasses]

b:228 [binder, in Typeclasses]

b:230 [binder, in Typeclasses]

b:232 [binder, in Typeclasses]

B:242 [binder, in Typeclasses]

b:245 [binder, in Typeclasses]

B:248 [binder, in Typeclasses]

B:25 [binder, in QuickChickInterface]

b:25 [binder, in Typeclasses]

b:29 [binder, in Typeclasses]

B:30 [binder, in QuickChickInterface]

B:34 [binder, in Typeclasses]

b:341 [binder, in TImp]

b:345 [binder, in TImp]

b:39 [binder, in Typeclasses]

B:4 [binder, in QuickChickInterface]

b:4 [binder, in Typeclasses]

B:41 [binder, in Typeclasses]

b:41 [binder, in QC]

B:48 [binder, in QC]

B:64 [binder, in QuickChickInterface]

b:66 [binder, in QC]

B:68 [binder, in QuickChickInterface]

B:71 [binder, in QC]

B:74 [binder, in QuickChickInterface]

## 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]

c

_{1}:338 [binder, in TImp]

c

_{1}:342 [binder, in TImp]

c

_{2}:339 [binder, in TImp]

c

_{2}:343 [binder, in TImp]

c:130 [binder, in QC]

C:249 [binder, in Typeclasses]

c:30 [binder, in Typeclasses]

c:346 [binder, in TImp]

c:356 [binder, in TImp]

c:361 [binder, in TImp]

c:369 [binder, in TImp]

c:53 [binder, in QC]

c:6 [binder, in QC]

c:7 [binder, in Typeclasses]

c:79 [binder, in QC]

## 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]

domain:79 [binder, in TImp]

d:121 [binder, in QC]

d:13 [binder, in Typeclasses]

D:62 [binder, in TImp]

D:69 [binder, in TImp]

## E

EAnd [constructor, in TImp]EEq [constructor, in TImp]

EFalse [constructor, in TImp]

eg

_{42}[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':311 [binder, in TImp]

e

_{1}[definition, in Typeclasses]

e

_{1}':284 [binder, in TImp]

e

_{1}':286 [binder, in TImp]

e

_{1}':293 [binder, in TImp]

e

_{1}':295 [binder, in TImp]

e

_{1}':297 [binder, in TImp]

e

_{1}':299 [binder, in TImp]

e

_{1}':301 [binder, in TImp]

e

_{1}':303 [binder, in TImp]

e

_{1}:102 [binder, in TImp]

e

_{1}:107 [binder, in TImp]

e

_{1}:110 [binder, in TImp]

e

_{1}:115 [binder, in TImp]

e

_{1}:159 [binder, in TImp]

e

_{1}:167 [binder, in TImp]

e

_{1}:176 [binder, in TImp]

e

_{1}:178 [binder, in TImp]

e

_{1}:180 [binder, in TImp]

e

_{1}:182 [binder, in TImp]

e

_{1}:184 [binder, in TImp]

e

_{1}:186 [binder, in TImp]

e

_{1}:187 [binder, in TImp]

e

_{1}:96 [binder, in TImp]

e

_{1}:99 [binder, in TImp]

e

_{2}[definition, in Typeclasses]

e

_{2}':285 [binder, in TImp]

e

_{2}':287 [binder, in TImp]

e

_{2}':294 [binder, in TImp]

e

_{2}':296 [binder, in TImp]

e

_{2}':298 [binder, in TImp]

e

_{2}':300 [binder, in TImp]

e

_{2}':302 [binder, in TImp]

e

_{2}':304 [binder, in TImp]

e

_{2}:100 [binder, in TImp]

e

_{2}:103 [binder, in TImp]

e

_{2}:108 [binder, in TImp]

e

_{2}:111 [binder, in TImp]

e

_{2}:116 [binder, in TImp]

e

_{2}:160 [binder, in TImp]

e

_{2}:168 [binder, in TImp]

e

_{2}:177 [binder, in TImp]

e

_{2}:179 [binder, in TImp]

e

_{2}:181 [binder, in TImp]

e

_{2}:183 [binder, in TImp]

e

_{2}:185 [binder, in TImp]

e

_{2}:188 [binder, in TImp]

e

_{2}:97 [binder, in TImp]

e

_{3}[definition, in Typeclasses]

e

_{3}[definition, in Typeclasses]

e:113 [binder, in TImp]

e:117 [binder, in TImp]

e:229 [binder, in TImp]

e:237 [binder, in TImp]

e:274 [binder, in TImp]

e:277 [binder, in TImp]

e:281 [binder, in TImp]

e:289 [binder, in TImp]

e:335 [binder, in TImp]

e:34 [binder, in QuickChickTool]

e:352 [binder, in TImp]

e:37 [binder, in QuickChickTool]

e:40 [binder, in QuickChickTool]

e:46 [binder, in QuickChickTool]

e:49 [binder, in QuickChickTool]

## F

Fail [constructor, in TImp]faultyMirrorP [definition, in QC]

foo [definition, in Typeclasses]

fresh [definition, in TImp]

fuel:359 [binder, in TImp]

fuel:370 [binder, in TImp]

f:135 [binder, in QC]

f:179 [binder, in Typeclasses]

f:194 [binder, in Typeclasses]

f:202 [binder, in Typeclasses]

f:212 [binder, in Typeclasses]

f:51 [binder, in QC]

f:75 [binder, in QC]

## G

Gamma:101 [binder, in TImp]Gamma:104 [binder, in TImp]

Gamma:105 [binder, in TImp]

Gamma:106 [binder, in TImp]

Gamma:109 [binder, in TImp]

Gamma:112 [binder, in TImp]

Gamma:114 [binder, in TImp]

Gamma:118 [binder, in TImp]

Gamma:130 [binder, in TImp]

Gamma:131 [binder, in TImp]

Gamma:138 [binder, in TImp]

Gamma:139 [binder, in TImp]

Gamma:141 [binder, in TImp]

Gamma:142 [binder, in TImp]

Gamma:143 [binder, in TImp]

Gamma:147 [binder, in TImp]

Gamma:151 [binder, in TImp]

Gamma:157 [binder, in TImp]

Gamma:158 [binder, in TImp]

Gamma:162 [binder, in TImp]

Gamma:170 [binder, in TImp]

Gamma:193 [binder, in TImp]

Gamma:220 [binder, in TImp]

Gamma:221 [binder, in TImp]

Gamma:223 [binder, in TImp]

Gamma:235 [binder, in TImp]

Gamma:242 [binder, in TImp]

Gamma:269 [binder, in TImp]

Gamma:307 [binder, in TImp]

Gamma:318 [binder, in TImp]

Gamma:332 [binder, in TImp]

Gamma:333 [binder, in TImp]

Gamma:337 [binder, in TImp]

Gamma:340 [binder, in TImp]

Gamma:344 [binder, in TImp]

Gamma:347 [binder, in TImp]

Gamma:351 [binder, in TImp]

Gamma:355 [binder, in TImp]

Gamma:367 [binder, in TImp]

Gamma:57 [binder, in TImp]

Gamma:64 [binder, in TImp]

Gamma:70 [binder, in TImp]

Gamma:92 [binder, in TImp]

Gamma:93 [binder, in TImp]

Gamma:95 [binder, in TImp]

Gamma:98 [binder, in TImp]

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]

gen:102 [binder, in QuickChickInterface]

gen:87 [binder, in QuickChickInterface]

gen:94 [binder, in QuickChickInterface]

get_fresh_ids [definition, in TImp]

gma:122 [binder, in TImp]

GMonad [instance, in QC]

GMonadDef [section, in QC]

Green [constructor, in Typeclasses]

Green [constructor, in QC]

g:177 [binder, in QC]

g:18 [binder, in QuickChickInterface]

g:19 [binder, in QC]

g:21 [binder, in QuickChickInterface]

g:24 [binder, in QC]

g:26 [binder, in QuickChickInterface]

g:50 [binder, in QC]

g:74 [binder, in QC]

## H

has_type_deterministic [lemma, in TImp]has_type_value [inductive, in TImp]

has_type [inductive, in TImp]

high:197 [binder, in QC]

high:206 [binder, in QC]

high:215 [binder, in QC]

high:223 [binder, in QC]

H

_{0}:101 [binder, in QuickChickInterface]

H

_{0}:116 [binder, in Typeclasses]

H

_{0}:128 [binder, in QC]

H

_{0}:136 [binder, in QuickChickInterface]

H

_{0}:187 [binder, in QuickChickInterface]

H

_{0}:23 [binder, in Typeclasses]

H

_{0}:251 [binder, in Typeclasses]

H

_{0}:36 [binder, in Typeclasses]

H

_{0}:43 [binder, in Typeclasses]

H

_{0}:6 [binder, in QuickChickInterface]

H

_{0}:64 [binder, in Typeclasses]

H

_{0}:66 [binder, in QuickChickInterface]

H

_{0}:70 [binder, in QuickChickInterface]

H

_{0}:73 [binder, in QC]

H

_{0}:76 [binder, in QuickChickInterface]

H

_{0}:81 [binder, in QuickChickInterface]

H

_{0}:86 [binder, in QuickChickInterface]

H

_{0}:91 [binder, in Typeclasses]

H

_{0}:93 [binder, in QuickChickInterface]

H

_{1}:74 [binder, in Typeclasses]

H

_{2}:111 [binder, in QuickChickInterface]

H

_{2}:118 [binder, in QuickChickInterface]

H

_{3}:112 [binder, in QuickChickInterface]

H

_{3}:120 [binder, in QuickChickInterface]

H:10 [binder, in QuickChickInterface]

H:100 [binder, in QuickChickInterface]

H:108 [binder, in QuickChickInterface]

H:109 [binder, in Typeclasses]

H:115 [binder, in QuickChickInterface]

H:12 [binder, in QC]

H:123 [binder, in QuickChickInterface]

H:126 [binder, in QuickChickInterface]

H:127 [binder, in QC]

H:130 [binder, in QuickChickInterface]

H:134 [binder, in Typeclasses]

H:135 [binder, in QuickChickInterface]

H:140 [binder, in QuickChickInterface]

H:142 [binder, in QC]

H:144 [binder, in QC]

H:146 [binder, in Typeclasses]

H:148 [binder, in QuickChickInterface]

H:153 [binder, in QuickChickInterface]

H:155 [binder, in QuickChickInterface]

H:156 [binder, in Typeclasses]

H:158 [binder, in QuickChickInterface]

H:161 [binder, in Typeclasses]

H:162 [binder, in QuickChickInterface]

H:165 [binder, in QuickChickInterface]

H:177 [binder, in QuickChickInterface]

H:18 [binder, in Typeclasses]

H:184 [binder, in QuickChickInterface]

H:193 [binder, in QuickChickInterface]

H:2 [binder, in QuickChickInterface]

H:207 [binder, in QuickChickInterface]

H:22 [binder, in Typeclasses]

H:250 [binder, in Typeclasses]

H:35 [binder, in Typeclasses]

H:398 [binder, in TImp]

H:42 [binder, in Typeclasses]

H:43 [binder, in QC]

H:49 [binder, in QC]

H:5 [binder, in QuickChickInterface]

H:53 [binder, in QuickChickInterface]

H:56 [binder, in QuickChickInterface]

H:56 [binder, in Typeclasses]

H:58 [binder, in QuickChickInterface]

H:59 [binder, in QC]

H:60 [binder, in QuickChickInterface]

H:62 [binder, in QuickChickInterface]

H:63 [binder, in Typeclasses]

H:65 [binder, in QuickChickInterface]

H:68 [binder, in Typeclasses]

H:68 [binder, in QC]

H:69 [binder, in QuickChickInterface]

H:72 [binder, in QuickChickInterface]

H:72 [binder, in Typeclasses]

H:72 [binder, in QC]

H:75 [binder, in QuickChickInterface]

H:78 [binder, in QuickChickInterface]

H:78 [binder, in Typeclasses]

H:8 [binder, in QuickChickInterface]

H:80 [binder, in QuickChickInterface]

H:81 [binder, in Typeclasses]

H:84 [binder, in Typeclasses]

H:85 [binder, in QuickChickInterface]

H:87 [binder, in Typeclasses]

H:90 [binder, in QC]

H:92 [binder, in QuickChickInterface]

## 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]

I:159 [binder, in QuickChickInterface]

I:162 [binder, in Typeclasses]

I:163 [binder, in QuickChickInterface]

## K

k:123 [binder, in TImp]## 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]

low:196 [binder, in QC]

low:205 [binder, in QC]

low:214 [binder, in QC]

low:222 [binder, in QC]

lt [definition, in Typeclasses]

lx [projection, in Typeclasses]

ly [projection, in Typeclasses]

l':87 [binder, in QC]

l:103 [binder, in QC]

l:12 [binder, in TImp]

l:143 [binder, in QuickChickInterface]

l:145 [binder, in QuickChickInterface]

l:165 [binder, in Typeclasses]

l:180 [binder, in QC]

l:183 [binder, in Typeclasses]

l:185 [binder, in QC]

l:186 [binder, in Typeclasses]

l:189 [binder, in QC]

l:191 [binder, in QC]

l:193 [binder, in QC]

l:195 [binder, in QC]

l:2 [binder, in Introduction]

l:204 [binder, in QC]

l:52 [binder, in Typeclasses]

l:57 [binder, in Typeclasses]

l:6 [binder, in Introduction]

l:9 [binder, in Introduction]

## 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]

ma:124 [binder, in TImp]

me:195 [binder, in TImp]

me:245 [binder, in TImp]

me:272 [binder, in TImp]

me:309 [binder, in TImp]

me:321 [binder, in TImp]

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]

m:104 [binder, in QC]

m:170 [binder, in QuickChickInterface]

m:173 [binder, in QuickChickInterface]

m:178 [binder, in Typeclasses]

m:180 [binder, in QuickChickInterface]

m:189 [binder, in QuickChickInterface]

m:190 [binder, in Typeclasses]

M:191 [binder, in Typeclasses]

m:194 [binder, in QuickChickInterface]

m:196 [binder, in QuickChickInterface]

m:197 [binder, in Typeclasses]

M:198 [binder, in Typeclasses]

m:206 [binder, in Typeclasses]

M:207 [binder, in Typeclasses]

m:233 [binder, in TImp]

m:314 [binder, in TImp]

m:38 [binder, in TImp]

m:43 [binder, in TImp]

m:47 [binder, in TImp]

m:54 [binder, in TImp]

## N

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

nth_opt [definition, in Typeclasses]

num_vars:316 [binder, in TImp]

num_vars:305 [binder, in TImp]

num_vars:267 [binder, in TImp]

num_vars:240 [binder, in TImp]

num_vars:191 [binder, in TImp]

n

_{1}:217 [binder, in Typeclasses]

n

_{1}:221 [binder, in Typeclasses]

n

_{2}:218 [binder, in Typeclasses]

n

_{2}:222 [binder, in Typeclasses]

n:10 [binder, in Typeclasses]

n:11 [binder, in TImp]

n:136 [binder, in QC]

n:140 [binder, in TImp]

n:145 [binder, in QC]

n:146 [binder, in TImp]

n:150 [binder, in TImp]

n:16 [binder, in Typeclasses]

n:171 [binder, in QuickChickInterface]

n:174 [binder, in QuickChickInterface]

n:178 [binder, in QC]

n:181 [binder, in QuickChickInterface]

n:182 [binder, in Typeclasses]

n:190 [binder, in QuickChickInterface]

n:195 [binder, in QuickChickInterface]

n:197 [binder, in QuickChickInterface]

n:206 [binder, in TImp]

n:212 [binder, in TImp]

n:246 [binder, in Typeclasses]

n:78 [binder, in TImp]

n:94 [binder, in TImp]

## 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]

Ord:237 [binder, in Typeclasses]

OutOfGas [constructor, in TImp]

## P

path [definition, in QC]path_mirror [definition, in QC]

pat:226 [binder, in TImp]

pat:74 [binder, in TImp]

pat:77 [binder, in TImp]

pf:104 [binder, in QuickChickInterface]

pf:88 [binder, in QuickChickInterface]

pf:96 [binder, in QuickChickInterface]

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]

prog:44 [binder, in QuickChickTool]

prop:107 [binder, in QuickChickInterface]

prop:114 [binder, in QuickChickInterface]

prop:122 [binder, in QuickChickInterface]

prop:125 [binder, in QuickChickInterface]

prop:129 [binder, in QuickChickInterface]

prop:134 [binder, in QuickChickInterface]

prop:139 [binder, in QuickChickInterface]

prop:147 [binder, in QuickChickInterface]

prop:84 [binder, in QuickChickInterface]

prop:91 [binder, in QuickChickInterface]

prop:99 [binder, in QuickChickInterface]

px [projection, in Typeclasses]

py [projection, in Typeclasses]

p1a:46 [binder, in Typeclasses]

p1b:47 [binder, in Typeclasses]

p

_{1}:44 [binder, in Typeclasses]

p2a:48 [binder, in Typeclasses]

p2b:49 [binder, in Typeclasses]

p

_{2}:45 [binder, in Typeclasses]

p:108 [binder, in QC]

P:11 [binder, in QuickChickInterface]

p:118 [binder, in QC]

p:131 [binder, in QuickChickInterface]

p:150 [binder, in QuickChickInterface]

P:151 [binder, in Typeclasses]

P:152 [binder, in QuickChickInterface]

P:154 [binder, in QuickChickInterface]

P:156 [binder, in QuickChickInterface]

P:159 [binder, in Typeclasses]

P:160 [binder, in QuickChickInterface]

P:164 [binder, in Typeclasses]

p:37 [binder, in Typeclasses]

P:389 [binder, in TImp]

P:393 [binder, in TImp]

P:397 [binder, in TImp]

P:42 [binder, in QC]

p:44 [binder, in QC]

P:67 [binder, in QC]

p:69 [binder, in QC]

## 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]

Q:157 [binder, in QuickChickInterface]

Q:160 [binder, in Typeclasses]

Q:161 [binder, in QuickChickInterface]

## R

r [definition, in Typeclasses]range:80 [binder, in TImp]

recs:189 [binder, in TImp]

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]

r':88 [binder, in QC]

r:105 [binder, in QC]

R:121 [binder, in Typeclasses]

R:126 [binder, in Typeclasses]

R:133 [binder, in Typeclasses]

r:137 [binder, in QC]

R:140 [binder, in Typeclasses]

R:145 [binder, in Typeclasses]

r:36 [binder, in QC]

r:365 [binder, in TImp]

r:60 [binder, in QC]

r:77 [binder, 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]

shrinker:103 [binder, in QuickChickInterface]

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]

shr:313 [binder, in TImp]

silly_fun2 [definition, in Typeclasses]

silly_fun1 [definition, in Typeclasses]

sinstr [inductive, in QuickChickTool]

size [definition, in QC]

size':174 [binder, in TImp]

size:161 [binder, in TImp]

size:169 [binder, in TImp]

size:198 [binder, in QC]

size:22 [binder, in QuickChickInterface]

SMinus [constructor, in QuickChickTool]

SMult [constructor, in QuickChickTool]

sorted [definition, in QC]

SPlus [constructor, in QuickChickTool]

SPush [constructor, in QuickChickTool]

stack:43 [binder, in QuickChickTool]

state [definition, in TImp]

string_of_nat [definition, in Typeclasses]

string_of_nat_aux [definition, in Typeclasses]

str:127 [binder, in QuickChickInterface]

st:219 [binder, in TImp]

st:222 [binder, in TImp]

st:228 [binder, in TImp]

st:236 [binder, in TImp]

st:243 [binder, in TImp]

st:270 [binder, in TImp]

st:319 [binder, in TImp]

st:360 [binder, in TImp]

st:368 [binder, in TImp]

Success [constructor, in TImp]

sum3 [definition, in Typeclasses]

sum3opt [definition, in Typeclasses]

sum3opt' [definition, in Typeclasses]

sz:18 [binder, in QC]

sz:23 [binder, in QC]

s:51 [binder, in Typeclasses]

s:82 [binder, in QC]

## 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]

test_insert_spec' [definition, in QC]

test_insert_spec [definition, in QC]

TIf [constructor, in TImp]

time:9 [binder, in Typeclasses]

TImp [library]

TLeaf [constructor, in QC]

TNat [constructor, in TImp]

TNode [constructor, in QC]

top_level_size:317 [binder, in TImp]

top_level_size:306 [binder, in TImp]

top_level_size:268 [binder, in TImp]

top_level_size:241 [binder, in TImp]

top_level_size:192 [binder, in TImp]

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]

TypePlayground1 [module, in TImp]

TypePlayground1.has_type [inductive, in TImp]

TypePlayground1.Ty_Var [constructor, in TImp]

TypePlayground2 [module, in TImp]

TypePlayground2.has_type [inductive, in TImp]

TypePlayground2.Ty_False [constructor, in TImp]

TypePlayground2.Ty_True [constructor, in TImp]

TypePlayground2.Ty_Num [constructor, in TImp]

TypePlayground2.Ty_Var [constructor, in TImp]

TypePlayground3 [module, in TImp]

TypePlayground3.has_type [inductive, in TImp]

TypePlayground3.Ty_Plus [constructor, in TImp]

TypePlayground3.Ty_Var [constructor, in TImp]

TyVBool [constructor, in TImp]

TyVNat [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]

T':72 [binder, in TImp]

T':75 [binder, in TImp]

t

_{1}:115 [binder, in QC]

t

_{1}:31 [binder, in QC]

T

_{1}:349 [binder, in TImp]

T

_{1}:353 [binder, in TImp]

t

_{2}:116 [binder, in QC]

t

_{2}:32 [binder, in QC]

T

_{2}:350 [binder, in TImp]

T

_{2}:354 [binder, in TImp]

t:102 [binder, in QC]

t:109 [binder, in QC]

t:113 [binder, in QC]

t:117 [binder, in QC]

T:119 [binder, in TImp]

T:124 [binder, in QuickChickInterface]

T:129 [binder, in TImp]

t:13 [binder, in QC]

T:132 [binder, in TImp]

T:137 [binder, in TImp]

t:141 [binder, in QuickChickInterface]

T:144 [binder, in TImp]

T:148 [binder, in TImp]

T:152 [binder, in TImp]

T:156 [binder, in TImp]

T:163 [binder, in Typeclasses]

T:163 [binder, in TImp]

T:171 [binder, in TImp]

T:174 [binder, in Typeclasses]

t:174 [binder, in QC]

T:176 [binder, in Typeclasses]

t:179 [binder, in QC]

T:192 [binder, in Typeclasses]

T:194 [binder, in TImp]

T:199 [binder, in Typeclasses]

t:207 [binder, in QC]

T:208 [binder, in Typeclasses]

T:209 [binder, in TImp]

T:210 [binder, in TImp]

t:211 [binder, in QC]

t:217 [binder, in QC]

T:218 [binder, in TImp]

t:219 [binder, in QC]

T:224 [binder, in TImp]

t:225 [binder, in QC]

T:238 [binder, in TImp]

T:244 [binder, in TImp]

T:271 [binder, in TImp]

T:276 [binder, in TImp]

t:28 [binder, in QC]

T:280 [binder, in TImp]

T:288 [binder, in TImp]

T:308 [binder, in TImp]

T:320 [binder, in TImp]

t:33 [binder, in QC]

T:336 [binder, in TImp]

t:55 [binder, in QC]

T:59 [binder, in TImp]

T:66 [binder, in TImp]

T:71 [binder, in TImp]

t:83 [binder, in QC]

T:91 [binder, in TImp]

t:96 [binder, in QC]

## U

U:177 [binder, in Typeclasses]U:193 [binder, in Typeclasses]

U:200 [binder, in Typeclasses]

U:209 [binder, in Typeclasses]

u:65 [binder, in QC]

## V

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

VNat [constructor, in TImp]

V:201 [binder, in Typeclasses]

v:208 [binder, in TImp]

V:210 [binder, in Typeclasses]

v:217 [binder, in TImp]

v:227 [binder, in TImp]

v:45 [binder, in TImp]

## W

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

well_typed_state [inductive, in TImp]

W:211 [binder, in Typeclasses]

## X

xs:202 [binder, in QC]x':86 [binder, in QC]

x

_{0}:187 [binder, in Typeclasses]

x

_{1}:188 [binder, in Typeclasses]

x

_{1}:219 [binder, in Typeclasses]

x

_{1}:7 [binder, in TImp]

x

_{2}:189 [binder, in Typeclasses]

x

_{2}:220 [binder, in Typeclasses]

x

_{2}:8 [binder, in TImp]

x:1 [binder, in Introduction]

x:111 [binder, in Typeclasses]

x:117 [binder, in Typeclasses]

x:119 [binder, in QuickChickInterface]

x:119 [binder, in QC]

x:12 [binder, in QuickChickInterface]

x:121 [binder, in QuickChickInterface]

x:123 [binder, in Typeclasses]

x:128 [binder, in Typeclasses]

x:128 [binder, in TImp]

x:132 [binder, in QC]

x:133 [binder, in TImp]

x:136 [binder, in TImp]

x:137 [binder, in QuickChickInterface]

x:15 [binder, in TImp]

x:155 [binder, in TImp]

x:157 [binder, in Typeclasses]

x:166 [binder, in QuickChickInterface]

x:168 [binder, in QuickChickInterface]

x:168 [binder, in Typeclasses]

x:171 [binder, in Typeclasses]

x:175 [binder, in QuickChickInterface]

x:175 [binder, in Typeclasses]

x:182 [binder, in QuickChickInterface]

x:184 [binder, in QC]

x:185 [binder, in QuickChickInterface]

x:188 [binder, in QC]

x:190 [binder, in QC]

x:191 [binder, in QuickChickInterface]

x:192 [binder, in QC]

x:194 [binder, in QC]

x:195 [binder, in Typeclasses]

x:196 [binder, in Typeclasses]

x:201 [binder, in QC]

x:203 [binder, in Typeclasses]

x:203 [binder, in QC]

X:205 [binder, in QuickChickInterface]

x:205 [binder, in Typeclasses]

X:206 [binder, in QuickChickInterface]

X:208 [binder, in QuickChickInterface]

x:210 [binder, in QC]

x:213 [binder, in Typeclasses]

x:216 [binder, in Typeclasses]

x:216 [binder, in QC]

x:216 [binder, in TImp]

x:218 [binder, in QC]

x:223 [binder, in Typeclasses]

x:224 [binder, in QC]

x:225 [binder, in TImp]

x:239 [binder, in Typeclasses]

x:33 [binder, in TImp]

x:334 [binder, in TImp]

x:348 [binder, in TImp]

x:39 [binder, in TImp]

x:399 [binder, in TImp]

x:44 [binder, in TImp]

x:5 [binder, in Introduction]

x:53 [binder, in TImp]

x:58 [binder, in TImp]

x:60 [binder, in TImp]

x:65 [binder, in Typeclasses]

x:65 [binder, in TImp]

x:67 [binder, in TImp]

x:73 [binder, in TImp]

x:75 [binder, in Typeclasses]

x:76 [binder, in TImp]

x:8 [binder, in Introduction]

x:9 [binder, in TImp]

x:90 [binder, in TImp]

x:91 [binder, in QC]

x:92 [binder, in Typeclasses]

x:95 [binder, in QuickChickInterface]

## Y

Yellow [constructor, in QC]y:112 [binder, in Typeclasses]

y:118 [binder, in Typeclasses]

y:129 [binder, in Typeclasses]

y:133 [binder, in QC]

y:158 [binder, in Typeclasses]

y:167 [binder, in QuickChickInterface]

y:169 [binder, in QuickChickInterface]

y:169 [binder, in Typeclasses]

y:172 [binder, in Typeclasses]

y:176 [binder, in QuickChickInterface]

y:183 [binder, in QuickChickInterface]

y:186 [binder, in QuickChickInterface]

y:192 [binder, in QuickChickInterface]

y:204 [binder, in Typeclasses]

y:214 [binder, in Typeclasses]

y:240 [binder, in Typeclasses]

y:34 [binder, in TImp]

y:400 [binder, in TImp]

y:61 [binder, in TImp]

y:66 [binder, in Typeclasses]

y:68 [binder, in TImp]

y:76 [binder, in Typeclasses]

y:93 [binder, in Typeclasses]

## Z

z:119 [binder, in Typeclasses]z:130 [binder, in Typeclasses]

z:170 [binder, in Typeclasses]

z:173 [binder, in Typeclasses]

z:215 [binder, in Typeclasses]

## 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]

# Binder Index

## A

acc':14 [in Typeclasses]acc:11 [in Typeclasses]

al:3 [in TImp]

al:6 [in TImp]

aux:16 [in QC]

A:1 [in QuickChickInterface]

A:1 [in Typeclasses]

A:1 [in QC]

A:101 [in QC]

A:103 [in Typeclasses]

A:106 [in QuickChickInterface]

A:107 [in QC]

A:108 [in Typeclasses]

A:11 [in QC]

A:113 [in QuickChickInterface]

A:114 [in Typeclasses]

A:120 [in Typeclasses]

A:120 [in TImp]

A:123 [in QC]

A:125 [in Typeclasses]

A:126 [in QC]

A:132 [in Typeclasses]

A:133 [in QuickChickInterface]

A:134 [in QC]

A:138 [in QC]

A:139 [in Typeclasses]

A:141 [in QC]

A:143 [in QC]

A:144 [in Typeclasses]

A:15 [in QuickChickInterface]

A:154 [in Typeclasses]

A:164 [in QuickChickInterface]

A:17 [in QuickChickInterface]

A:17 [in Typeclasses]

A:17 [in QC]

A:172 [in QuickChickInterface]

A:173 [in QC]

A:178 [in QuickChickInterface]

A:181 [in Typeclasses]

A:188 [in QuickChickInterface]

a:19 [in Typeclasses]

A:20 [in QuickChickInterface]

A:20 [in Typeclasses]

A:22 [in QC]

A:232 [in TImp]

A:236 [in Typeclasses]

A:238 [in Typeclasses]

A:24 [in QuickChickInterface]

a:24 [in Typeclasses]

A:241 [in Typeclasses]

A:247 [in Typeclasses]

a:252 [in Typeclasses]

A:26 [in Typeclasses]

a:27 [in QuickChickInterface]

A:27 [in QC]

A:29 [in QuickChickInterface]

A:3 [in QuickChickInterface]

A:312 [in TImp]

A:32 [in QuickChickInterface]

A:33 [in Typeclasses]

A:34 [in QuickChickInterface]

A:35 [in TImp]

A:36 [in QuickChickInterface]

A:36 [in TImp]

A:37 [in TImp]

A:38 [in QuickChickInterface]

a:38 [in Typeclasses]

A:38 [in QC]

A:388 [in TImp]

A:392 [in TImp]

A:396 [in TImp]

A:40 [in QuickChickInterface]

A:40 [in Typeclasses]

A:42 [in QuickChickInterface]

A:42 [in TImp]

A:44 [in QuickChickInterface]

A:46 [in QuickChickInterface]

A:46 [in TImp]

A:47 [in QC]

A:48 [in QuickChickInterface]

A:50 [in QuickChickInterface]

A:50 [in Typeclasses]

A:50 [in TImp]

A:52 [in QuickChickInterface]

a:52 [in QC]

A:55 [in QuickChickInterface]

A:55 [in Typeclasses]

a:55 [in TImp]

A:56 [in TImp]

A:57 [in QuickChickInterface]

A:58 [in Typeclasses]

A:58 [in QC]

A:59 [in QuickChickInterface]

A:61 [in QuickChickInterface]

A:62 [in Typeclasses]

A:62 [in QC]

A:63 [in QuickChickInterface]

A:63 [in TImp]

A:67 [in QuickChickInterface]

A:67 [in Typeclasses]

A:7 [in QuickChickInterface]

A:70 [in QC]

A:71 [in QuickChickInterface]

A:71 [in Typeclasses]

A:73 [in QuickChickInterface]

a:76 [in QC]

A:77 [in QuickChickInterface]

A:77 [in Typeclasses]

A:79 [in QuickChickInterface]

a:79 [in Typeclasses]

A:8 [in QC]

A:80 [in Typeclasses]

A:81 [in QC]

a:82 [in Typeclasses]

A:83 [in QuickChickInterface]

A:83 [in Typeclasses]

a:85 [in Typeclasses]

a:88 [in Typeclasses]

A:89 [in Typeclasses]

A:89 [in QC]

A:9 [in QuickChickInterface]

A:90 [in QuickChickInterface]

A:92 [in QC]

A:95 [in QC]

A:98 [in QuickChickInterface]

## B

base:173 [in TImp]B:121 [in TImp]

b:149 [in QuickChickInterface]

B:179 [in QuickChickInterface]

b:207 [in TImp]

B:21 [in Typeclasses]

b:213 [in TImp]

b:226 [in Typeclasses]

b:228 [in Typeclasses]

b:230 [in Typeclasses]

b:232 [in Typeclasses]

B:242 [in Typeclasses]

b:245 [in Typeclasses]

B:248 [in Typeclasses]

B:25 [in QuickChickInterface]

b:25 [in Typeclasses]

b:29 [in Typeclasses]

B:30 [in QuickChickInterface]

B:34 [in Typeclasses]

b:341 [in TImp]

b:345 [in TImp]

b:39 [in Typeclasses]

B:4 [in QuickChickInterface]

b:4 [in Typeclasses]

B:41 [in Typeclasses]

b:41 [in QC]

B:48 [in QC]

B:64 [in QuickChickInterface]

b:66 [in QC]

B:68 [in QuickChickInterface]

B:71 [in QC]

B:74 [in QuickChickInterface]

## C

c_{1}:338 [in TImp]

c

_{1}:342 [in TImp]

c

_{2}:339 [in TImp]

c

_{2}:343 [in TImp]

c:130 [in QC]

C:249 [in Typeclasses]

c:30 [in Typeclasses]

c:346 [in TImp]

c:356 [in TImp]

c:361 [in TImp]

c:369 [in TImp]

c:53 [in QC]

c:6 [in QC]

c:7 [in Typeclasses]

c:79 [in QC]

## D

domain:79 [in TImp]d:121 [in QC]

d:13 [in Typeclasses]

D:62 [in TImp]

D:69 [in TImp]

## E

e':311 [in TImp]e

_{1}':284 [in TImp]

e

_{1}':286 [in TImp]

e

_{1}':293 [in TImp]

e

_{1}':295 [in TImp]

e

_{1}':297 [in TImp]

e

_{1}':299 [in TImp]

e

_{1}':301 [in TImp]

e

_{1}':303 [in TImp]

e

_{1}:102 [in TImp]

e

_{1}:107 [in TImp]

e

_{1}:110 [in TImp]

e

_{1}:115 [in TImp]

e

_{1}:159 [in TImp]

e

_{1}:167 [in TImp]

e

_{1}:176 [in TImp]

e

_{1}:178 [in TImp]

e

_{1}:180 [in TImp]

e

_{1}:182 [in TImp]

e

_{1}:184 [in TImp]

e

_{1}:186 [in TImp]

e

_{1}:187 [in TImp]

e

_{1}:96 [in TImp]

e

_{1}:99 [in TImp]

e

_{2}':285 [in TImp]

e

_{2}':287 [in TImp]

e

_{2}':294 [in TImp]

e

_{2}':296 [in TImp]

e

_{2}':298 [in TImp]

e

_{2}':300 [in TImp]

e

_{2}':302 [in TImp]

e

_{2}':304 [in TImp]

e

_{2}:100 [in TImp]

e

_{2}:103 [in TImp]

e

_{2}:108 [in TImp]

e

_{2}:111 [in TImp]

e

_{2}:116 [in TImp]

e

_{2}:160 [in TImp]

e

_{2}:168 [in TImp]

e

_{2}:177 [in TImp]

e

_{2}:179 [in TImp]

e

_{2}:181 [in TImp]

e

_{2}:183 [in TImp]

e

_{2}:185 [in TImp]

e

_{2}:188 [in TImp]

e

_{2}:97 [in TImp]

e:113 [in TImp]

e:117 [in TImp]

e:229 [in TImp]

e:237 [in TImp]

e:274 [in TImp]

e:277 [in TImp]

e:281 [in TImp]

e:289 [in TImp]

e:335 [in TImp]

e:34 [in QuickChickTool]

e:352 [in TImp]

e:37 [in QuickChickTool]

e:40 [in QuickChickTool]

e:46 [in QuickChickTool]

e:49 [in QuickChickTool]

## F

fuel:359 [in TImp]fuel:370 [in TImp]

f:135 [in QC]

f:179 [in Typeclasses]

f:194 [in Typeclasses]

f:202 [in Typeclasses]

f:212 [in Typeclasses]

f:51 [in QC]

f:75 [in QC]

## G

Gamma:101 [in TImp]Gamma:104 [in TImp]

Gamma:105 [in TImp]

Gamma:106 [in TImp]

Gamma:109 [in TImp]

Gamma:112 [in TImp]

Gamma:114 [in TImp]

Gamma:118 [in TImp]

Gamma:130 [in TImp]

Gamma:131 [in TImp]

Gamma:138 [in TImp]

Gamma:139 [in TImp]

Gamma:141 [in TImp]

Gamma:142 [in TImp]

Gamma:143 [in TImp]

Gamma:147 [in TImp]

Gamma:151 [in TImp]

Gamma:157 [in TImp]

Gamma:158 [in TImp]

Gamma:162 [in TImp]

Gamma:170 [in TImp]

Gamma:193 [in TImp]

Gamma:220 [in TImp]

Gamma:221 [in TImp]

Gamma:223 [in TImp]

Gamma:235 [in TImp]

Gamma:242 [in TImp]

Gamma:269 [in TImp]

Gamma:307 [in TImp]

Gamma:318 [in TImp]

Gamma:332 [in TImp]

Gamma:333 [in TImp]

Gamma:337 [in TImp]

Gamma:340 [in TImp]

Gamma:344 [in TImp]

Gamma:347 [in TImp]

Gamma:351 [in TImp]

Gamma:355 [in TImp]

Gamma:367 [in TImp]

Gamma:57 [in TImp]

Gamma:64 [in TImp]

Gamma:70 [in TImp]

Gamma:92 [in TImp]

Gamma:93 [in TImp]

Gamma:95 [in TImp]

Gamma:98 [in TImp]

gen:102 [in QuickChickInterface]

gen:87 [in QuickChickInterface]

gen:94 [in QuickChickInterface]

gma:122 [in TImp]

g:177 [in QC]

g:18 [in QuickChickInterface]

g:19 [in QC]

g:21 [in QuickChickInterface]

g:24 [in QC]

g:26 [in QuickChickInterface]

g:50 [in QC]

g:74 [in QC]

## H

high:197 [in QC]high:206 [in QC]

high:215 [in QC]

high:223 [in QC]

H

_{0}:101 [in QuickChickInterface]

H

_{0}:116 [in Typeclasses]

H

_{0}:128 [in QC]

H

_{0}:136 [in QuickChickInterface]

H

_{0}:187 [in QuickChickInterface]

H

_{0}:23 [in Typeclasses]

H

_{0}:251 [in Typeclasses]

H

_{0}:36 [in Typeclasses]

H

_{0}:43 [in Typeclasses]

H

_{0}:6 [in QuickChickInterface]

H

_{0}:64 [in Typeclasses]

H

_{0}:66 [in QuickChickInterface]

H

_{0}:70 [in QuickChickInterface]

H

_{0}:73 [in QC]

H

_{0}:76 [in QuickChickInterface]

H

_{0}:81 [in QuickChickInterface]

H

_{0}:86 [in QuickChickInterface]

H

_{0}:91 [in Typeclasses]

H

_{0}:93 [in QuickChickInterface]

H

_{1}:74 [in Typeclasses]

H

_{2}:111 [in QuickChickInterface]

H

_{2}:118 [in QuickChickInterface]

H

_{3}:112 [in QuickChickInterface]

H

_{3}:120 [in QuickChickInterface]

H:10 [in QuickChickInterface]

H:100 [in QuickChickInterface]

H:108 [in QuickChickInterface]

H:109 [in Typeclasses]

H:115 [in QuickChickInterface]

H:12 [in QC]

H:123 [in QuickChickInterface]

H:126 [in QuickChickInterface]

H:127 [in QC]

H:130 [in QuickChickInterface]

H:134 [in Typeclasses]

H:135 [in QuickChickInterface]

H:140 [in QuickChickInterface]

H:142 [in QC]

H:144 [in QC]

H:146 [in Typeclasses]

H:148 [in QuickChickInterface]

H:153 [in QuickChickInterface]

H:155 [in QuickChickInterface]

H:156 [in Typeclasses]

H:158 [in QuickChickInterface]

H:161 [in Typeclasses]

H:162 [in QuickChickInterface]

H:165 [in QuickChickInterface]

H:177 [in QuickChickInterface]

H:18 [in Typeclasses]

H:184 [in QuickChickInterface]

H:193 [in QuickChickInterface]

H:2 [in QuickChickInterface]

H:207 [in QuickChickInterface]

H:22 [in Typeclasses]

H:250 [in Typeclasses]

H:35 [in Typeclasses]

H:398 [in TImp]

H:42 [in Typeclasses]

H:43 [in QC]

H:49 [in QC]

H:5 [in QuickChickInterface]

H:53 [in QuickChickInterface]

H:56 [in QuickChickInterface]

H:56 [in Typeclasses]

H:58 [in QuickChickInterface]

H:59 [in QC]

H:60 [in QuickChickInterface]

H:62 [in QuickChickInterface]

H:63 [in Typeclasses]

H:65 [in QuickChickInterface]

H:68 [in Typeclasses]

H:68 [in QC]

H:69 [in QuickChickInterface]

H:72 [in QuickChickInterface]

H:72 [in Typeclasses]

H:72 [in QC]

H:75 [in QuickChickInterface]

H:78 [in QuickChickInterface]

H:78 [in Typeclasses]

H:8 [in QuickChickInterface]

H:80 [in QuickChickInterface]

H:81 [in Typeclasses]

H:84 [in Typeclasses]

H:85 [in QuickChickInterface]

H:87 [in Typeclasses]

H:90 [in QC]

H:92 [in QuickChickInterface]

## I

I:159 [in QuickChickInterface]I:162 [in Typeclasses]

I:163 [in QuickChickInterface]

## K

k:123 [in TImp]## L

low:196 [in QC]low:205 [in QC]

low:214 [in QC]

low:222 [in QC]

l':87 [in QC]

l:103 [in QC]

l:12 [in TImp]

l:143 [in QuickChickInterface]

l:145 [in QuickChickInterface]

l:165 [in Typeclasses]

l:180 [in QC]

l:183 [in Typeclasses]

l:185 [in QC]

l:186 [in Typeclasses]

l:189 [in QC]

l:191 [in QC]

l:193 [in QC]

l:195 [in QC]

l:2 [in Introduction]

l:204 [in QC]

l:52 [in Typeclasses]

l:57 [in Typeclasses]

l:6 [in Introduction]

l:9 [in Introduction]

## M

ma:124 [in TImp]me:195 [in TImp]

me:245 [in TImp]

me:272 [in TImp]

me:309 [in TImp]

me:321 [in TImp]

m:104 [in QC]

m:170 [in QuickChickInterface]

m:173 [in QuickChickInterface]

m:178 [in Typeclasses]

m:180 [in QuickChickInterface]

m:189 [in QuickChickInterface]

m:190 [in Typeclasses]

M:191 [in Typeclasses]

m:194 [in QuickChickInterface]

m:196 [in QuickChickInterface]

m:197 [in Typeclasses]

M:198 [in Typeclasses]

m:206 [in Typeclasses]

M:207 [in Typeclasses]

m:233 [in TImp]

m:314 [in TImp]

m:38 [in TImp]

m:43 [in TImp]

m:47 [in TImp]

m:54 [in TImp]

## N

num_vars:316 [in TImp]num_vars:305 [in TImp]

num_vars:267 [in TImp]

num_vars:240 [in TImp]

num_vars:191 [in TImp]

n

_{1}:217 [in Typeclasses]

n

_{1}:221 [in Typeclasses]

n

_{2}:218 [in Typeclasses]

n

_{2}:222 [in Typeclasses]

n:10 [in Typeclasses]

n:11 [in TImp]

n:136 [in QC]

n:140 [in TImp]

n:145 [in QC]

n:146 [in TImp]

n:150 [in TImp]

n:16 [in Typeclasses]

n:171 [in QuickChickInterface]

n:174 [in QuickChickInterface]

n:178 [in QC]

n:181 [in QuickChickInterface]

n:182 [in Typeclasses]

n:190 [in QuickChickInterface]

n:195 [in QuickChickInterface]

n:197 [in QuickChickInterface]

n:206 [in TImp]

n:212 [in TImp]

n:246 [in Typeclasses]

n:78 [in TImp]

n:94 [in TImp]

## O

Ord:237 [in Typeclasses]## P

pat:226 [in TImp]pat:74 [in TImp]

pat:77 [in TImp]

pf:104 [in QuickChickInterface]

pf:88 [in QuickChickInterface]

pf:96 [in QuickChickInterface]

prog:44 [in QuickChickTool]

prop:107 [in QuickChickInterface]

prop:114 [in QuickChickInterface]

prop:122 [in QuickChickInterface]

prop:125 [in QuickChickInterface]

prop:129 [in QuickChickInterface]

prop:134 [in QuickChickInterface]

prop:139 [in QuickChickInterface]

prop:147 [in QuickChickInterface]

prop:84 [in QuickChickInterface]

prop:91 [in QuickChickInterface]

prop:99 [in QuickChickInterface]

p1a:46 [in Typeclasses]

p1b:47 [in Typeclasses]

p

_{1}:44 [in Typeclasses]

p2a:48 [in Typeclasses]

p2b:49 [in Typeclasses]

p

_{2}:45 [in Typeclasses]

p:108 [in QC]

P:11 [in QuickChickInterface]

p:118 [in QC]

p:131 [in QuickChickInterface]

p:150 [in QuickChickInterface]

P:151 [in Typeclasses]

P:152 [in QuickChickInterface]

P:154 [in QuickChickInterface]

P:156 [in QuickChickInterface]

P:159 [in Typeclasses]

P:160 [in QuickChickInterface]

P:164 [in Typeclasses]

p:37 [in Typeclasses]

P:389 [in TImp]

P:393 [in TImp]

P:397 [in TImp]

P:42 [in QC]

p:44 [in QC]

P:67 [in QC]

p:69 [in QC]

## Q

Q:157 [in QuickChickInterface]Q:160 [in Typeclasses]

Q:161 [in QuickChickInterface]

## R

range:80 [in TImp]recs:189 [in TImp]

r':88 [in QC]

r:105 [in QC]

R:121 [in Typeclasses]

R:126 [in Typeclasses]

R:133 [in Typeclasses]

r:137 [in QC]

R:140 [in Typeclasses]

R:145 [in Typeclasses]

r:36 [in QC]

r:365 [in TImp]

r:60 [in QC]

r:77 [in QC]

## S

shrinker:103 [in QuickChickInterface]shr:313 [in TImp]

size':174 [in TImp]

size:161 [in TImp]

size:169 [in TImp]

size:198 [in QC]

size:22 [in QuickChickInterface]

stack:43 [in QuickChickTool]

str:127 [in QuickChickInterface]

st:219 [in TImp]

st:222 [in TImp]

st:228 [in TImp]

st:236 [in TImp]

st:243 [in TImp]

st:270 [in TImp]

st:319 [in TImp]

st:360 [in TImp]

st:368 [in TImp]

sz:18 [in QC]

sz:23 [in QC]

s:51 [in Typeclasses]

s:82 [in QC]

## T

time:9 [in Typeclasses]top_level_size:317 [in TImp]

top_level_size:306 [in TImp]

top_level_size:268 [in TImp]

top_level_size:241 [in TImp]

top_level_size:192 [in TImp]

T':72 [in TImp]

T':75 [in TImp]

t

_{1}:115 [in QC]

t

_{1}:31 [in QC]

T

_{1}:349 [in TImp]

T

_{1}:353 [in TImp]

t

_{2}:116 [in QC]

t

_{2}:32 [in QC]

T

_{2}:350 [in TImp]

T

_{2}:354 [in TImp]

t:102 [in QC]

t:109 [in QC]

t:113 [in QC]

t:117 [in QC]

T:119 [in TImp]

T:124 [in QuickChickInterface]

T:129 [in TImp]

t:13 [in QC]

T:132 [in TImp]

T:137 [in TImp]

t:141 [in QuickChickInterface]

T:144 [in TImp]

T:148 [in TImp]

T:152 [in TImp]

T:156 [in TImp]

T:163 [in Typeclasses]

T:163 [in TImp]

T:171 [in TImp]

T:174 [in Typeclasses]

t:174 [in QC]

T:176 [in Typeclasses]

t:179 [in QC]

T:192 [in Typeclasses]

T:194 [in TImp]

T:199 [in Typeclasses]

t:207 [in QC]

T:208 [in Typeclasses]

T:209 [in TImp]

T:210 [in TImp]

t:211 [in QC]

t:217 [in QC]

T:218 [in TImp]

t:219 [in QC]

T:224 [in TImp]

t:225 [in QC]

T:238 [in TImp]

T:244 [in TImp]

T:271 [in TImp]

T:276 [in TImp]

t:28 [in QC]

T:280 [in TImp]

T:288 [in TImp]

T:308 [in TImp]

T:320 [in TImp]

t:33 [in QC]

T:336 [in TImp]

t:55 [in QC]

T:59 [in TImp]

T:66 [in TImp]

T:71 [in TImp]

t:83 [in QC]

T:91 [in TImp]

t:96 [in QC]

## U

U:177 [in Typeclasses]U:193 [in Typeclasses]

U:200 [in Typeclasses]

U:209 [in Typeclasses]

u:65 [in QC]

## V

V:201 [in Typeclasses]v:208 [in TImp]

V:210 [in Typeclasses]

v:217 [in TImp]

v:227 [in TImp]

v:45 [in TImp]

## W

W:211 [in Typeclasses]## X

xs:202 [in QC]x':86 [in QC]

x

_{0}:187 [in Typeclasses]

x

_{1}:188 [in Typeclasses]

x

_{1}:219 [in Typeclasses]

x

_{1}:7 [in TImp]

x

_{2}:189 [in Typeclasses]

x

_{2}:220 [in Typeclasses]

x

_{2}:8 [in TImp]

x:1 [in Introduction]

x:111 [in Typeclasses]

x:117 [in Typeclasses]

x:119 [in QuickChickInterface]

x:119 [in QC]

x:12 [in QuickChickInterface]

x:121 [in QuickChickInterface]

x:123 [in Typeclasses]

x:128 [in Typeclasses]

x:128 [in TImp]

x:132 [in QC]

x:133 [in TImp]

x:136 [in TImp]

x:137 [in QuickChickInterface]

x:15 [in TImp]

x:155 [in TImp]

x:157 [in Typeclasses]

x:166 [in QuickChickInterface]

x:168 [in QuickChickInterface]

x:168 [in Typeclasses]

x:171 [in Typeclasses]

x:175 [in QuickChickInterface]

x:175 [in Typeclasses]

x:182 [in QuickChickInterface]

x:184 [in QC]

x:185 [in QuickChickInterface]

x:188 [in QC]

x:190 [in QC]

x:191 [in QuickChickInterface]

x:192 [in QC]

x:194 [in QC]

x:195 [in Typeclasses]

x:196 [in Typeclasses]

x:201 [in QC]

x:203 [in Typeclasses]

x:203 [in QC]

X:205 [in QuickChickInterface]

x:205 [in Typeclasses]

X:206 [in QuickChickInterface]

X:208 [in QuickChickInterface]

x:210 [in QC]

x:213 [in Typeclasses]

x:216 [in Typeclasses]

x:216 [in QC]

x:216 [in TImp]

x:218 [in QC]

x:223 [in Typeclasses]

x:224 [in QC]

x:225 [in TImp]

x:239 [in Typeclasses]

x:33 [in TImp]

x:334 [in TImp]

x:348 [in TImp]

x:39 [in TImp]

x:399 [in TImp]

x:44 [in TImp]

x:5 [in Introduction]

x:53 [in TImp]

x:58 [in TImp]

x:60 [in TImp]

x:65 [in Typeclasses]

x:65 [in TImp]

x:67 [in TImp]

x:73 [in TImp]

x:75 [in Typeclasses]

x:76 [in TImp]

x:8 [in Introduction]

x:9 [in TImp]

x:90 [in TImp]

x:91 [in QC]

x:92 [in Typeclasses]

x:95 [in QuickChickInterface]

## Y

y:112 [in Typeclasses]y:118 [in Typeclasses]

y:129 [in Typeclasses]

y:133 [in QC]

y:158 [in Typeclasses]

y:167 [in QuickChickInterface]

y:169 [in QuickChickInterface]

y:169 [in Typeclasses]

y:172 [in Typeclasses]

y:176 [in QuickChickInterface]

y:183 [in QuickChickInterface]

y:186 [in QuickChickInterface]

y:192 [in QuickChickInterface]

y:204 [in Typeclasses]

y:214 [in Typeclasses]

y:240 [in Typeclasses]

y:34 [in TImp]

y:400 [in TImp]

y:61 [in TImp]

y:66 [in Typeclasses]

y:68 [in TImp]

y:76 [in Typeclasses]

y:93 [in Typeclasses]

## Z

z:119 [in Typeclasses]z:130 [in Typeclasses]

z:170 [in Typeclasses]

z:173 [in Typeclasses]

z:215 [in Typeclasses]

# 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]

## T

TypePlayground1 [in TImp]TypePlayground2 [in TImp]

TypePlayground3 [in TImp]

# Library Index

## B

Bib## I

Introduction## P

PostscriptPreface

## Q

QCQuickChickInterface

QuickChickTool

## T

TImpTypeclasses

# 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]

TypePlayground1.Ty_Var [in TImp]

TypePlayground2.Ty_False [in TImp]

TypePlayground2.Ty_True [in TImp]

TypePlayground2.Ty_Num [in TImp]

TypePlayground2.Ty_Var [in TImp]

TypePlayground3.Ty_Plus [in TImp]

TypePlayground3.Ty_Var [in TImp]

TyVBool [in TImp]

TyVNat [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 [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]

TypePlayground1.has_type [in TImp]

TypePlayground2.has_type [in TImp]

TypePlayground3.has_type [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_{42}[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

_{1}[in Typeclasses]

e

_{2}[in Typeclasses]

e

_{3}[in Typeclasses]

e

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

test_insert_spec' [in QC]

test_insert_spec [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 | (1229 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) |

Binder 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 | (755 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 | (17 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 | (115 entries) |

This page has been generated by coqdoc