| 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 | (1212 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 | (23 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 | (747 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 | (16 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) |
| 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 | (35 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 | (81 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 | (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 | _ | 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 | (114 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 QuickChickInterface]
A:101 [binder, in QC]
A:103 [binder, in Typeclasses]
A:107 [binder, in QC]
A:108 [binder, in QuickChickInterface]
A:108 [binder, in Typeclasses]
A:11 [binder, in QC]
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:128 [binder, in QuickChickInterface]
A:132 [binder, in Typeclasses]
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:159 [binder, in QuickChickInterface]
A:167 [binder, in QuickChickInterface]
A:17 [binder, in QuickChickInterface]
A:17 [binder, in Typeclasses]
A:17 [binder, in QC]
A:173 [binder, in QuickChickInterface]
A:173 [binder, in QC]
A:181 [binder, in Typeclasses]
A:183 [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:31 [binder, in QuickChickInterface]
A:312 [binder, in TImp]
A:33 [binder, in QuickChickInterface]
A:33 [binder, in Typeclasses]
A:35 [binder, in QuickChickInterface]
A:35 [binder, in TImp]
A:36 [binder, in TImp]
A:37 [binder, in QuickChickInterface]
A:37 [binder, in TImp]
a:38 [binder, in Typeclasses]
A:38 [binder, in QC]
A:39 [binder, in QuickChickInterface]
A:40 [binder, in Typeclasses]
A:41 [binder, in QuickChickInterface]
A:411 [binder, in TImp]
A:415 [binder, in TImp]
A:419 [binder, in TImp]
A:42 [binder, in TImp]
A:43 [binder, in QuickChickInterface]
A:45 [binder, in QuickChickInterface]
A:46 [binder, in TImp]
A:47 [binder, in QuickChickInterface]
A:47 [binder, in QC]
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:54 [binder, in QuickChickInterface]
A:55 [binder, in Typeclasses]
a:55 [binder, in TImp]
A:56 [binder, in QuickChickInterface]
A:56 [binder, in TImp]
A:58 [binder, in QuickChickInterface]
A:58 [binder, in Typeclasses]
A:58 [binder, in QC]
A:62 [binder, in QuickChickInterface]
A:62 [binder, in Typeclasses]
A:62 [binder, in QC]
A:63 [binder, in TImp]
A:66 [binder, in QuickChickInterface]
A:67 [binder, in Typeclasses]
A:68 [binder, in QuickChickInterface]
A:7 [binder, in QuickChickInterface]
A:70 [binder, in QC]
A:71 [binder, in Typeclasses]
A:72 [binder, in QuickChickInterface]
A:74 [binder, in QuickChickInterface]
a:76 [binder, in QC]
A:77 [binder, in Typeclasses]
A:78 [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 Typeclasses]
A:85 [binder, in QuickChickInterface]
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:92 [binder, in QC]
A:93 [binder, in QuickChickInterface]
A:95 [binder, in QC]
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]
B:121 [binder, in TImp]
b:144 [binder, in QuickChickInterface]
B:174 [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: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:59 [binder, in QuickChickInterface]
B:63 [binder, in QuickChickInterface]
b:66 [binder, in QC]
B:69 [binder, in QuickChickInterface]
B:71 [binder, in QC]
C
CAsgn [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]
c1:338 [binder, in TImp]
c1:342 [binder, in TImp]
c2:339 [binder, in TImp]
c2: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]
eg42 [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]
e1 [definition, in Typeclasses]
e1':284 [binder, in TImp]
e1':286 [binder, in TImp]
e1':293 [binder, in TImp]
e1':295 [binder, in TImp]
e1':297 [binder, in TImp]
e1':299 [binder, in TImp]
e1':301 [binder, in TImp]
e1':303 [binder, in TImp]
e1:102 [binder, in TImp]
e1:107 [binder, in TImp]
e1:110 [binder, in TImp]
e1:115 [binder, in TImp]
e1:159 [binder, in TImp]
e1:167 [binder, in TImp]
e1:176 [binder, in TImp]
e1:178 [binder, in TImp]
e1:180 [binder, in TImp]
e1:182 [binder, in TImp]
e1:184 [binder, in TImp]
e1:186 [binder, in TImp]
e1:187 [binder, in TImp]
e1:96 [binder, in TImp]
e1:99 [binder, in TImp]
e2 [definition, in Typeclasses]
e2':285 [binder, in TImp]
e2':287 [binder, in TImp]
e2':294 [binder, in TImp]
e2':296 [binder, in TImp]
e2':298 [binder, in TImp]
e2':300 [binder, in TImp]
e2':302 [binder, in TImp]
e2':304 [binder, in TImp]
e2:100 [binder, in TImp]
e2:103 [binder, in TImp]
e2:108 [binder, in TImp]
e2:111 [binder, in TImp]
e2:116 [binder, in TImp]
e2:160 [binder, in TImp]
e2:168 [binder, in TImp]
e2:177 [binder, in TImp]
e2:179 [binder, in TImp]
e2:181 [binder, in TImp]
e2:183 [binder, in TImp]
e2:185 [binder, in TImp]
e2:188 [binder, in TImp]
e2:97 [binder, in TImp]
e3 [definition, in Typeclasses]
e3 [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 [instance, 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]
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:82 [binder, in QuickChickInterface]
gen:89 [binder, in QuickChickInterface]
gen:97 [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: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]
H0:116 [binder, in Typeclasses]
H0:128 [binder, in QC]
H0:131 [binder, in QuickChickInterface]
H0:182 [binder, in QuickChickInterface]
H0:23 [binder, in Typeclasses]
H0:251 [binder, in Typeclasses]
H0:36 [binder, in Typeclasses]
H0:43 [binder, in Typeclasses]
H0:6 [binder, in QuickChickInterface]
H0:61 [binder, in QuickChickInterface]
H0:64 [binder, in Typeclasses]
H0:65 [binder, in QuickChickInterface]
H0:71 [binder, in QuickChickInterface]
H0:73 [binder, in QC]
H0:76 [binder, in QuickChickInterface]
H0:81 [binder, in QuickChickInterface]
H0:88 [binder, in QuickChickInterface]
H0:91 [binder, in Typeclasses]
H0:96 [binder, in QuickChickInterface]
H1:74 [binder, in Typeclasses]
H2:106 [binder, in QuickChickInterface]
H2:113 [binder, in QuickChickInterface]
H3:107 [binder, in QuickChickInterface]
H3:115 [binder, in QuickChickInterface]
H:10 [binder, in QuickChickInterface]
H:103 [binder, in QuickChickInterface]
H:109 [binder, in Typeclasses]
H:110 [binder, in QuickChickInterface]
H:118 [binder, in QuickChickInterface]
H:12 [binder, in QC]
H:121 [binder, in QuickChickInterface]
H:125 [binder, in QuickChickInterface]
H:127 [binder, in QC]
H:130 [binder, in QuickChickInterface]
H:134 [binder, in Typeclasses]
H:135 [binder, in QuickChickInterface]
H:142 [binder, in QC]
H:143 [binder, in QuickChickInterface]
H:144 [binder, in QC]
H:146 [binder, in Typeclasses]
H:148 [binder, in QuickChickInterface]
H:150 [binder, in QuickChickInterface]
H:153 [binder, in QuickChickInterface]
H:156 [binder, in Typeclasses]
H:157 [binder, in QuickChickInterface]
H:160 [binder, in QuickChickInterface]
H:161 [binder, in Typeclasses]
H:172 [binder, in QuickChickInterface]
H:179 [binder, in QuickChickInterface]
H:18 [binder, in Typeclasses]
H:188 [binder, in QuickChickInterface]
H:2 [binder, in QuickChickInterface]
H:22 [binder, in Typeclasses]
H:250 [binder, in Typeclasses]
H:35 [binder, in Typeclasses]
H:42 [binder, in Typeclasses]
H:421 [binder, in TImp]
H:43 [binder, in QC]
H:48 [binder, in QuickChickInterface]
H:49 [binder, in QC]
H:5 [binder, in QuickChickInterface]
H:51 [binder, in QuickChickInterface]
H:53 [binder, in QuickChickInterface]
H:55 [binder, in QuickChickInterface]
H:56 [binder, in Typeclasses]
H:57 [binder, in QuickChickInterface]
H:59 [binder, in QC]
H:60 [binder, in QuickChickInterface]
H:63 [binder, in Typeclasses]
H:64 [binder, in QuickChickInterface]
H:67 [binder, in QuickChickInterface]
H:68 [binder, in Typeclasses]
H:68 [binder, in QC]
H:70 [binder, in QuickChickInterface]
H:72 [binder, in Typeclasses]
H:72 [binder, in QC]
H:73 [binder, in QuickChickInterface]
H:75 [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:87 [binder, in QuickChickInterface]
H:87 [binder, in Typeclasses]
H:90 [binder, in QC]
H:95 [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:154 [binder, in QuickChickInterface]
I:158 [binder, in QuickChickInterface]
I:162 [binder, in Typeclasses]
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:138 [binder, in QuickChickInterface]
l:140 [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:165 [binder, in QuickChickInterface]
m:168 [binder, in QuickChickInterface]
m:175 [binder, in QuickChickInterface]
m:178 [binder, in Typeclasses]
m:184 [binder, in QuickChickInterface]
m:189 [binder, in QuickChickInterface]
m:190 [binder, in Typeclasses]
m:191 [binder, in QuickChickInterface]
M:191 [binder, in Typeclasses]
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]
n1:217 [binder, in Typeclasses]
n1:221 [binder, in Typeclasses]
n2:218 [binder, in Typeclasses]
n2: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:166 [binder, in QuickChickInterface]
n:169 [binder, in QuickChickInterface]
n:176 [binder, in QuickChickInterface]
n:178 [binder, in QC]
n:182 [binder, in Typeclasses]
n:185 [binder, in QuickChickInterface]
n:190 [binder, in QuickChickInterface]
n:192 [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:83 [binder, in QuickChickInterface]
pf:91 [binder, in QuickChickInterface]
pf:99 [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:102 [binder, in QuickChickInterface]
prop:109 [binder, in QuickChickInterface]
prop:117 [binder, in QuickChickInterface]
prop:120 [binder, in QuickChickInterface]
prop:124 [binder, in QuickChickInterface]
prop:129 [binder, in QuickChickInterface]
prop:134 [binder, in QuickChickInterface]
prop:142 [binder, in QuickChickInterface]
prop:79 [binder, in QuickChickInterface]
prop:86 [binder, in QuickChickInterface]
prop:94 [binder, in QuickChickInterface]
px [projection, in Typeclasses]
py [projection, in Typeclasses]
p1a:46 [binder, in Typeclasses]
p1b:47 [binder, in Typeclasses]
p1:44 [binder, in Typeclasses]
p2a:48 [binder, in Typeclasses]
p2b:49 [binder, in Typeclasses]
p2:45 [binder, in Typeclasses]
p:108 [binder, in QC]
P:11 [binder, in QuickChickInterface]
p:118 [binder, in QC]
p:126 [binder, in QuickChickInterface]
p:145 [binder, in QuickChickInterface]
P:147 [binder, in QuickChickInterface]
P:149 [binder, in QuickChickInterface]
P:151 [binder, in QuickChickInterface]
P:151 [binder, in Typeclasses]
P:155 [binder, in QuickChickInterface]
P:159 [binder, in Typeclasses]
P:164 [binder, in Typeclasses]
p:37 [binder, in Typeclasses]
P:412 [binder, in TImp]
P:416 [binder, in TImp]
P:42 [binder, in QC]
P:420 [binder, in TImp]
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.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.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.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]
QuickChickTool [library]
Q:152 [binder, in QuickChickInterface]
Q:156 [binder, in QuickChickInterface]
Q:160 [binder, in Typeclasses]
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:98 [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:122 [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
TAsgn [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]
t1:115 [binder, in QC]
t1:31 [binder, in QC]
T1:349 [binder, in TImp]
T1:353 [binder, in TImp]
t2:116 [binder, in QC]
t2:32 [binder, in QC]
T2:350 [binder, in TImp]
T2: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 QuickChickInterface]
T:119 [binder, in TImp]
T:129 [binder, in TImp]
t:13 [binder, in QC]
T:132 [binder, in TImp]
t:136 [binder, in QuickChickInterface]
T:137 [binder, in TImp]
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]
x0:187 [binder, in Typeclasses]
x1:188 [binder, in Typeclasses]
x1:219 [binder, in Typeclasses]
x1:7 [binder, in TImp]
x2:189 [binder, in Typeclasses]
x2:220 [binder, in Typeclasses]
x2:8 [binder, in TImp]
x:1 [binder, in Introduction]
x:111 [binder, in Typeclasses]
x:114 [binder, in QuickChickInterface]
x:116 [binder, in QuickChickInterface]
x:117 [binder, in Typeclasses]
x:119 [binder, in QC]
x:12 [binder, in QuickChickInterface]
x:123 [binder, in Typeclasses]
x:128 [binder, in Typeclasses]
x:128 [binder, in TImp]
x:132 [binder, in QuickChickInterface]
x:132 [binder, in QC]
x:133 [binder, in TImp]
x:136 [binder, in TImp]
x:15 [binder, in TImp]
x:155 [binder, in TImp]
x:157 [binder, in Typeclasses]
x:161 [binder, in QuickChickInterface]
x:163 [binder, in QuickChickInterface]
x:168 [binder, in Typeclasses]
x:170 [binder, in QuickChickInterface]
x:171 [binder, in Typeclasses]
x:175 [binder, in Typeclasses]
x:177 [binder, in QuickChickInterface]
x:180 [binder, in QuickChickInterface]
x:184 [binder, in QC]
x:186 [binder, in QuickChickInterface]
x:188 [binder, in QC]
x:190 [binder, in QC]
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 Typeclasses]
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:422 [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 QuickChickInterface]
x:90 [binder, in TImp]
x:91 [binder, in QC]
x:92 [binder, in Typeclasses]
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:162 [binder, in QuickChickInterface]
y:164 [binder, in QuickChickInterface]
y:169 [binder, in Typeclasses]
y:171 [binder, in QuickChickInterface]
y:172 [binder, in Typeclasses]
y:178 [binder, in QuickChickInterface]
y:181 [binder, in QuickChickInterface]
y:187 [binder, in QuickChickInterface]
y:204 [binder, in Typeclasses]
y:214 [binder, in Typeclasses]
y:240 [binder, in Typeclasses]
y:34 [binder, in TImp]
y:423 [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 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
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]
_ ==> _ (Checker_scope) [in QuickChickInterface]
_ ? [in QuickChickInterface]
other
_ ? [in Typeclasses]_ <=? _ [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 QuickChickInterface]
A:101 [in QC]
A:103 [in Typeclasses]
A:107 [in QC]
A:108 [in QuickChickInterface]
A:108 [in Typeclasses]
A:11 [in QC]
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:128 [in QuickChickInterface]
A:132 [in Typeclasses]
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:159 [in QuickChickInterface]
A:167 [in QuickChickInterface]
A:17 [in QuickChickInterface]
A:17 [in Typeclasses]
A:17 [in QC]
A:173 [in QuickChickInterface]
A:173 [in QC]
A:181 [in Typeclasses]
A:183 [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:31 [in QuickChickInterface]
A:312 [in TImp]
A:33 [in QuickChickInterface]
A:33 [in Typeclasses]
A:35 [in QuickChickInterface]
A:35 [in TImp]
A:36 [in TImp]
A:37 [in QuickChickInterface]
A:37 [in TImp]
a:38 [in Typeclasses]
A:38 [in QC]
A:39 [in QuickChickInterface]
A:40 [in Typeclasses]
A:41 [in QuickChickInterface]
A:411 [in TImp]
A:415 [in TImp]
A:419 [in TImp]
A:42 [in TImp]
A:43 [in QuickChickInterface]
A:45 [in QuickChickInterface]
A:46 [in TImp]
A:47 [in QuickChickInterface]
A:47 [in QC]
A:50 [in QuickChickInterface]
A:50 [in Typeclasses]
A:50 [in TImp]
A:52 [in QuickChickInterface]
a:52 [in QC]
A:54 [in QuickChickInterface]
A:55 [in Typeclasses]
a:55 [in TImp]
A:56 [in QuickChickInterface]
A:56 [in TImp]
A:58 [in QuickChickInterface]
A:58 [in Typeclasses]
A:58 [in QC]
A:62 [in QuickChickInterface]
A:62 [in Typeclasses]
A:62 [in QC]
A:63 [in TImp]
A:66 [in QuickChickInterface]
A:67 [in Typeclasses]
A:68 [in QuickChickInterface]
A:7 [in QuickChickInterface]
A:70 [in QC]
A:71 [in Typeclasses]
A:72 [in QuickChickInterface]
A:74 [in QuickChickInterface]
a:76 [in QC]
A:77 [in Typeclasses]
A:78 [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 Typeclasses]
A:85 [in QuickChickInterface]
a:85 [in Typeclasses]
a:88 [in Typeclasses]
A:89 [in Typeclasses]
A:89 [in QC]
A:9 [in QuickChickInterface]
A:92 [in QC]
A:93 [in QuickChickInterface]
A:95 [in QC]
B
base:173 [in TImp]B:121 [in TImp]
b:144 [in QuickChickInterface]
B:174 [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: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:59 [in QuickChickInterface]
B:63 [in QuickChickInterface]
b:66 [in QC]
B:69 [in QuickChickInterface]
B:71 [in QC]
C
c1:338 [in TImp]c1:342 [in TImp]
c2:339 [in TImp]
c2: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]e1':284 [in TImp]
e1':286 [in TImp]
e1':293 [in TImp]
e1':295 [in TImp]
e1':297 [in TImp]
e1':299 [in TImp]
e1':301 [in TImp]
e1':303 [in TImp]
e1:102 [in TImp]
e1:107 [in TImp]
e1:110 [in TImp]
e1:115 [in TImp]
e1:159 [in TImp]
e1:167 [in TImp]
e1:176 [in TImp]
e1:178 [in TImp]
e1:180 [in TImp]
e1:182 [in TImp]
e1:184 [in TImp]
e1:186 [in TImp]
e1:187 [in TImp]
e1:96 [in TImp]
e1:99 [in TImp]
e2':285 [in TImp]
e2':287 [in TImp]
e2':294 [in TImp]
e2':296 [in TImp]
e2':298 [in TImp]
e2':300 [in TImp]
e2':302 [in TImp]
e2':304 [in TImp]
e2:100 [in TImp]
e2:103 [in TImp]
e2:108 [in TImp]
e2:111 [in TImp]
e2:116 [in TImp]
e2:160 [in TImp]
e2:168 [in TImp]
e2:177 [in TImp]
e2:179 [in TImp]
e2:181 [in TImp]
e2:183 [in TImp]
e2:185 [in TImp]
e2:188 [in TImp]
e2: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:82 [in QuickChickInterface]
gen:89 [in QuickChickInterface]
gen:97 [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:50 [in QC]
g:74 [in QC]
H
high:197 [in QC]high:206 [in QC]
high:215 [in QC]
high:223 [in QC]
H0:116 [in Typeclasses]
H0:128 [in QC]
H0:131 [in QuickChickInterface]
H0:182 [in QuickChickInterface]
H0:23 [in Typeclasses]
H0:251 [in Typeclasses]
H0:36 [in Typeclasses]
H0:43 [in Typeclasses]
H0:6 [in QuickChickInterface]
H0:61 [in QuickChickInterface]
H0:64 [in Typeclasses]
H0:65 [in QuickChickInterface]
H0:71 [in QuickChickInterface]
H0:73 [in QC]
H0:76 [in QuickChickInterface]
H0:81 [in QuickChickInterface]
H0:88 [in QuickChickInterface]
H0:91 [in Typeclasses]
H0:96 [in QuickChickInterface]
H1:74 [in Typeclasses]
H2:106 [in QuickChickInterface]
H2:113 [in QuickChickInterface]
H3:107 [in QuickChickInterface]
H3:115 [in QuickChickInterface]
H:10 [in QuickChickInterface]
H:103 [in QuickChickInterface]
H:109 [in Typeclasses]
H:110 [in QuickChickInterface]
H:118 [in QuickChickInterface]
H:12 [in QC]
H:121 [in QuickChickInterface]
H:125 [in QuickChickInterface]
H:127 [in QC]
H:130 [in QuickChickInterface]
H:134 [in Typeclasses]
H:135 [in QuickChickInterface]
H:142 [in QC]
H:143 [in QuickChickInterface]
H:144 [in QC]
H:146 [in Typeclasses]
H:148 [in QuickChickInterface]
H:150 [in QuickChickInterface]
H:153 [in QuickChickInterface]
H:156 [in Typeclasses]
H:157 [in QuickChickInterface]
H:160 [in QuickChickInterface]
H:161 [in Typeclasses]
H:172 [in QuickChickInterface]
H:179 [in QuickChickInterface]
H:18 [in Typeclasses]
H:188 [in QuickChickInterface]
H:2 [in QuickChickInterface]
H:22 [in Typeclasses]
H:250 [in Typeclasses]
H:35 [in Typeclasses]
H:42 [in Typeclasses]
H:421 [in TImp]
H:43 [in QC]
H:48 [in QuickChickInterface]
H:49 [in QC]
H:5 [in QuickChickInterface]
H:51 [in QuickChickInterface]
H:53 [in QuickChickInterface]
H:55 [in QuickChickInterface]
H:56 [in Typeclasses]
H:57 [in QuickChickInterface]
H:59 [in QC]
H:60 [in QuickChickInterface]
H:63 [in Typeclasses]
H:64 [in QuickChickInterface]
H:67 [in QuickChickInterface]
H:68 [in Typeclasses]
H:68 [in QC]
H:70 [in QuickChickInterface]
H:72 [in Typeclasses]
H:72 [in QC]
H:73 [in QuickChickInterface]
H:75 [in QuickChickInterface]
H:78 [in Typeclasses]
H:8 [in QuickChickInterface]
H:80 [in QuickChickInterface]
H:81 [in Typeclasses]
H:84 [in Typeclasses]
H:87 [in QuickChickInterface]
H:87 [in Typeclasses]
H:90 [in QC]
H:95 [in QuickChickInterface]
I
I:154 [in QuickChickInterface]I:158 [in QuickChickInterface]
I:162 [in Typeclasses]
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:138 [in QuickChickInterface]
l:140 [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:165 [in QuickChickInterface]
m:168 [in QuickChickInterface]
m:175 [in QuickChickInterface]
m:178 [in Typeclasses]
m:184 [in QuickChickInterface]
m:189 [in QuickChickInterface]
m:190 [in Typeclasses]
m:191 [in QuickChickInterface]
M:191 [in Typeclasses]
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]
n1:217 [in Typeclasses]
n1:221 [in Typeclasses]
n2:218 [in Typeclasses]
n2: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:166 [in QuickChickInterface]
n:169 [in QuickChickInterface]
n:176 [in QuickChickInterface]
n:178 [in QC]
n:182 [in Typeclasses]
n:185 [in QuickChickInterface]
n:190 [in QuickChickInterface]
n:192 [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:83 [in QuickChickInterface]
pf:91 [in QuickChickInterface]
pf:99 [in QuickChickInterface]
prog:44 [in QuickChickTool]
prop:102 [in QuickChickInterface]
prop:109 [in QuickChickInterface]
prop:117 [in QuickChickInterface]
prop:120 [in QuickChickInterface]
prop:124 [in QuickChickInterface]
prop:129 [in QuickChickInterface]
prop:134 [in QuickChickInterface]
prop:142 [in QuickChickInterface]
prop:79 [in QuickChickInterface]
prop:86 [in QuickChickInterface]
prop:94 [in QuickChickInterface]
p1a:46 [in Typeclasses]
p1b:47 [in Typeclasses]
p1:44 [in Typeclasses]
p2a:48 [in Typeclasses]
p2b:49 [in Typeclasses]
p2:45 [in Typeclasses]
p:108 [in QC]
P:11 [in QuickChickInterface]
p:118 [in QC]
p:126 [in QuickChickInterface]
p:145 [in QuickChickInterface]
P:147 [in QuickChickInterface]
P:149 [in QuickChickInterface]
P:151 [in QuickChickInterface]
P:151 [in Typeclasses]
P:155 [in QuickChickInterface]
P:159 [in Typeclasses]
P:164 [in Typeclasses]
p:37 [in Typeclasses]
P:412 [in TImp]
P:416 [in TImp]
P:42 [in QC]
P:420 [in TImp]
p:44 [in QC]
P:67 [in QC]
p:69 [in QC]
Q
Q:152 [in QuickChickInterface]Q:156 [in QuickChickInterface]
Q:160 [in Typeclasses]
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:98 [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:122 [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]
t1:115 [in QC]
t1:31 [in QC]
T1:349 [in TImp]
T1:353 [in TImp]
t2:116 [in QC]
t2:32 [in QC]
T2:350 [in TImp]
T2:354 [in TImp]
t:102 [in QC]
t:109 [in QC]
t:113 [in QC]
t:117 [in QC]
T:119 [in QuickChickInterface]
T:119 [in TImp]
T:129 [in TImp]
t:13 [in QC]
T:132 [in TImp]
t:136 [in QuickChickInterface]
T:137 [in TImp]
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]
x0:187 [in Typeclasses]
x1:188 [in Typeclasses]
x1:219 [in Typeclasses]
x1:7 [in TImp]
x2:189 [in Typeclasses]
x2:220 [in Typeclasses]
x2:8 [in TImp]
x:1 [in Introduction]
x:111 [in Typeclasses]
x:114 [in QuickChickInterface]
x:116 [in QuickChickInterface]
x:117 [in Typeclasses]
x:119 [in QC]
x:12 [in QuickChickInterface]
x:123 [in Typeclasses]
x:128 [in Typeclasses]
x:128 [in TImp]
x:132 [in QuickChickInterface]
x:132 [in QC]
x:133 [in TImp]
x:136 [in TImp]
x:15 [in TImp]
x:155 [in TImp]
x:157 [in Typeclasses]
x:161 [in QuickChickInterface]
x:163 [in QuickChickInterface]
x:168 [in Typeclasses]
x:170 [in QuickChickInterface]
x:171 [in Typeclasses]
x:175 [in Typeclasses]
x:177 [in QuickChickInterface]
x:180 [in QuickChickInterface]
x:184 [in QC]
x:186 [in QuickChickInterface]
x:188 [in QC]
x:190 [in QC]
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 Typeclasses]
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:422 [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 QuickChickInterface]
x:90 [in TImp]
x:91 [in QC]
x:92 [in Typeclasses]
Y
y:112 [in Typeclasses]y:118 [in Typeclasses]
y:129 [in Typeclasses]
y:133 [in QC]
y:158 [in Typeclasses]
y:162 [in QuickChickInterface]
y:164 [in QuickChickInterface]
y:169 [in Typeclasses]
y:171 [in QuickChickInterface]
y:172 [in Typeclasses]
y:178 [in QuickChickInterface]
y:181 [in QuickChickInterface]
y:187 [in QuickChickInterface]
y:204 [in Typeclasses]
y:214 [in Typeclasses]
y:240 [in Typeclasses]
y:34 [in TImp]
y:423 [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.QcNotation [in QuickChickInterface]
T
TypePlayground1 [in TImp]TypePlayground2 [in TImp]
TypePlayground3 [in TImp]
Library Index
B
BibI
IntroductionP
PostscriptPreface
Q
QCQuickChickInterface
QuickChickTool
T
TImpTypeclasses
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.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]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]
C
CAsgn [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]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
TAsgn [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]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
genPath [in QC]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
eg42 [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]
e1 [in Typeclasses]
e2 [in Typeclasses]
e3 [in Typeclasses]
e3 [in Typeclasses]
F
faultyMirrorP [in QC]foo [in Typeclasses]
fresh [in TImp]
G
genColor [in QC]genColor' [in QC]
genDirection [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 | (1212 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 | (23 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 | (747 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 | (16 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) |
| 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 | (35 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 | (81 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 | (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 | _ | 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 | (114 entries) |
This page has been generated by coqdoc