|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Bertot Y., Castéran P. — Interactive Theorem Proving and Program Development: Coq'ArtiThe Calculus of Inductive Constructions |
|
|
|
| Предметный указатель |
Plain definitions, eq_dec 255
Plain definitions, example_codomain 387
Plain definitions, excluded_middle 123
Plain definitions, F_Infinite 374
Plain definitions, G_Infinite 374
Plain definitions, implies_to_or 123
Plain definitions, insert_spec 314 343
Plain definitions, isEmpty 351
Plain definitions, is_prime 205
Plain definitions, leibniz 131
Plain definitions, Lexico.A 338
Plain definitions, Lexico.le 338
Plain definitions, list2tree_spec 319
Plain definitions, LKey.A 333
Plain definitions, long 76
Plain definitions, More_Dec_Orders.A 336
Plain definitions, More_Dec_Orders.le 336
Plain definitions, More_Dec_Orders.lt 336
Plain definitions, my_and 133
Plain definitions, my_ex 133
Plain definitions, my_False 130
Plain definitions, my_le 134
Plain definitions, my_not 131
Plain definitions, my_or 133
Plain definitions, my_True 130
Plain definitions, Nats.data 342
Plain definitions, nat_fun_to_Z_fun 41
Plain definitions, Nat_Order.A 338
Plain definitions, Nat_Order.le 338
Plain definitions, Nat_Order.lt 338
Plain definitions, neutral_left 107
Plain definitions, occ_dec 315
Plain definitions, occ_dec_spec 313 343
Plain definitions, PairKey.A 333
Plain definitions, peirce 123
Plain definitions, rich_minus 395
Plain definitions, rmax_sig 322
Plain definitions, rmax_spec 322
Plain definitions, rm_spec 314
Plain definitions, satisfies 372
Plain definitions, short 76
Plain definitions, stronger_prime_test 264
Plain definitions, TDict.data 343
Plain definitions, TDict.dict 344
Plain definitions, TDict.key 343
Plain definitions, TrivialDict.data 341
Plain definitions, TrivialDict.dict 341
Plain definitions, TrivialDict.key 341
Plain definitions, ZKey.A 329
Plain definitions, Z_bin 40
Syntax, cofix 352
Syntax, fix 190 284
Syntax, let in 27
Syntax, match 142 145
Tacticals, orelse 63
Tacticals, repeat 123
Tacticals, try 64
Tactics, apply 48 53 108 139 141
Tactics, apply, apply with 110
Tactics, assert 68
Tactics, assoc_eq 444
Tactics, assoc_eq_nat 441
Tactics, assumption 49 52 105
Tactics, auto 139 149 200 215
Tactics, auto, with 190
Tactics, autoAfter 202
Tactics, autoClear 202
Tactics, autorewrite 194 360 362
Tactics, case 160 188
Tactics, caseEq 160
Tactics, cbv 36 189 435
Tactics, change 152 154 188
Tactics, check_It_not_divides 205
Tactics, check_not_divides 203
Tactics, clear 70 193 202 284
Tactics, clear_all 206
Tactics, cofix 364
Tactics, comm_eq 447
Tactics, compute 36 278
Tactics, compute_rank 444
Tactics, constructor 227
Tactics, contrapose 204
Tactics, cut 68 242
Tactics, dependent rewrite 221
Tactics, destruct 188
Tactics, discriminate 151
Tactics, div_bin_tac 280
Tactics, eapply 111 194 243
Tactics, eauto 194 242 243
Tactics, eexact 112 194
Tactics, elim 118 121 141 160 217 241 244
Tactics, elim, using 270 430
Tactics, elim, with 141
Tactics, exact 52 105
Tactics, exists 123 227
Tactics, fail 64
Tactics, field 199
Tactics, fold 190 280
Tactics, fourier 200
Tactics, generalize 157 248 275
Tactics, idtac 64
Tactics, induction 142 187 227 229
Tactics, injection 153 249
Tactics, intro 106 139
Tactics, intros 48 225
Tactics, intuition 122 201
Tactics, inversion 247
Tactics, lazy 189 280 435
Tactics, left 219 227
Tactics, le_S_star 202
Tactics, LList_unfold 360
Tactics, model 441
Tactics, model_A 444
Tactics, model_aux 444
Tactics, omega 198 260
Tactics, pattern 127 139 159 160 245 248
Tactics, refine 265 282 315
Tactics, reflexivity 124
Tactics, rewrite 125 207 220 225
Tactics, rewrite in 126
Tactics, rewrite, rewrite <- 126
Tactics, right 219 227
Tactics, ring 125 196
Tactics, ring_nat 198 417
Tactics, simpl 144 188 267 435
Tactics, simpl at  189
Tactics, simpl_on 210
Tactics, split 227
Tactics, subst 195
Tactics, S_to_plus_simpl 207
Tactics, tauto 122 200
Tactics, term_list 444
Tactics, trivial 71
Tactics, unfold 115
Theorems, absurd 119
Theorems, all_imp_dist 110
Theorems, all_perm 97
Theorems, and_commutes 121
Theorems, any_height_inj2 221
Theorems, apply_example 54
Theorems, at_least_28 148
Theorems, bad_get_primediv_ok 263
Theorems, bdiv_aux_correctl 408
Theorems, bicycle_eq_seats 153
Theorems, compose_example 63
Theorems, cond_rewrite_example 128
Theorems, conj3 100
Theorems, conj3’ 121
Theorems, contrap 120
Theorems, conv_example 105
| Theorems, cut_example 69
Theorems, delta 53
Theorems, diff_of_squares 125
Theorems, disj4_3 100
Theorems, disj4_3’ 121
Theorems, div it_correct 1 426
Theorems, div2_le 267 268
Theorems, divides_refl 262
Theorems, div_bin_eq 281
Theorems, div_bin_rem_lt 280
Theorems, div_it_fix_eqn 425
Theorems, double_neg_i 119
Theorems, double_neg_i’ 120
Theorems, elim_example 245
Theorems, eq_sym’ 125
Theorems, eq_trans 129
Theorems, Eventually_of_LAppend 373
Theorems, example_contrapose 204
Theorems, example_for_field 199
Theorems, example_for_Fourier 200
Theorems, example_for_subst 195
Theorems, example_intuition 201
Theorems, ex_imp_ex 123
Theorems, fact_def_pos 235
Theorems, Finite_of_LCons 362
Theorems, flatten_aux_valid 440
Theorems, flatten_aux_valid_A 443
Theorems, flatten_valid 440
Theorems, flatten_valid_2 440
Theorems, flatten_valid_A 443
Theorems, flatten_valid_A_2 443
Theorems, from_Infinite 364
Theorems, from_Infinite_V0 364
Theorems, get_primediv_ok 264
Theorems, greater_values_sum 402
Theorems, HoareWhileRule 240
Theorems, imp_dist 54 65
Theorems, imp_trans 47 51 107
Theorems, inject_c2 155
Theorems, insert_is_f 446
Theorems, K 56
Theorems, keep_length 223
Theorems, LAppend_assoc 370
Theorems, LAppend_LCons 357 360
Theorems, LAppend_LNil 360
Theorems, LAppend_of_Finite 362
Theorems, lazy_example 190
Theorems, leibniz_sym 132
Theorems, length_february 144
Theorems, le_0_mult 113
Theorems, le_0_mult_R 113
Theorems, le_2_n_not_zero 259
Theorems, le_2_n_pred 259
Theorems, le_2_n_pred’ 259
Theorems, le_5_25 202
Theorems, le_i_SSi 86 109
Theorems, le_mult_mult 110
Theorems, le_mult_mult’ 111
Theorems, le_plus_minus’ 188
Theorems, LList_decomposition_lemma 358
Theorems, LNil_not_Infinite 367
Theorems, log2_domain_invert 429
Theorems, log_domain_non_0 428
Theorems, lt_Acc 412
Theorems, lt_le 229
Theorems, lt_S 115
Theorems, lt_wf 412
Theorems, max 1_correct 425
Theorems, max2_correct 425
Theorems, modus_ponens 120
Theorems, month_equal 139
Theorems, More_Dec_Orders .le_trans 336
Theorems, More_Dec_Orders. It_ir reflexive 336
Theorems, More_Dec_Orders.lt_intro 336
Theorems, my_False_ind 131
Theorems, my_I 131
Theorems, nat_2_ind 270
Theorems, nat_not_strange 185
Theorems, Nat_Order.It_diff 338
Theorems, Nat_Order.le_lt_or_eq 338
Theorems, Nat_Order.le_lt_weak 338
Theorems, Nat_Order.ordered 338
Theorems, next_august_then_july 151
Theorems, Next_example 373
Theorems, next_march_shorter 157
Theorems, not_decreasing 415
Theorems, not_even_l 248
Theorems, not_January_eq_February 152
Theorems, not_l_even 246
Theorems, not_l_even’ 247
Theorems, obtain_I 194
Theorems, omega_example1 198
Theorems, omega_example2 198
Theorems, omega_example3 199
Theorems, omega_example4 199
Theorems, omega_of_Finite 362
Theorems, one_neutral_left 107
Theorems, orelse_example 63
Theorems, or_commutes 122
Theorems, pfact3 235
Theorems, plus_2_even_inv 247
Theorems, plus_2_even_inv’ 249
Theorems, plus_assoc 162 433
Theorems, plus_assoc’ 172
Theorems, plus_comm 273
Theorems, plus_n_Sm 272
Theorems, plus_plus’ 274
Theorems, plus’_comm 274
Theorems, plus”_Sn_m 275
Theorems, pow_log_le 430
Theorems, pred_strong2_thl 260
Theorems, pred_thl 260
Theorems, prime37 205
Theorems, prime61 205
Theorems, prime_2333 437
Theorems, reflection_test 438
Theorems, reflection_test3 445
Theorems, reflection_test4 447
Theorems, reflection_test’ 441
Theorems, reflection_test” 442
Theorems, refl_equal 98
Theorems, regroup 127
Theorems, rem_even_ge_interval 279
Theorems, rem_even_lt_interval 279
Theorems, rem_l_even_interval 278
Theorems, rem_l_l_interval 277
Theorems, rem_l_odd_interval 279
Theorems, rem_odd_ge_interval 279
Theorems, rem_odd_lt_interval 279
Theorems, resolution 97
Theorems, ring_example2 197
Theorems, ring_example3 197
Theorems, ring_example4 197
Theorems, ring_example5 207
Theorems, ring_example6 207
Theorems, ring_example7 208
Theorems, ring_examplel 197
Theorems, Rpos_div2_wf 413
Theorems, simpl_on_example 210
Theorems, simpl_pattern_example 189
Theorems, sorted2_inv 216
Theorems, sortedl_inv 216
Theorems, sorted_nat_123 215
Theorems, sort_eq 447
Theorems, sort_eq_2 447
Theorems, sqr_01 244
Theorems, strange_empty 184
Theorems, structured_intro_example2 226
Theorems, structured_intro_examplel 226
Theorems, sum_even 227
|
|
|
| Реклама |
|
|
|
|
|
О проекте