Download Le Coq` Art (V8)

COQ ET BIBLIOTHÈQUES
récursion bien fondée, 320, 330,
447
récursion structurelle, 186, 194,
196, 292
Règle d’élimination de False, 120
Relations bien fondées, 261, 447
Renforcement minimal de spécification, 286, 330, 331
Scope, 32
Scopes, 203
Sections, 37, 48
Signatures, 356
Sortes, 55
Sous-buts, 67
Spécifications, 32, 55
Structures mathématiques, 178,
433
Structures quotient, 178
Substitutions, 52
Suites de réductions, 54
Tacticielles, 82
Tactics, 59
Tactiques, 19, 67
Tautologies, 224
Termes, 32
Termes de preuve, 66
Théorèmes, 67
Transparence, 80, 432, 454
Type de tête, 74, 130, 131
Type final, 74, 131, 161, 164,
216, 270, 413
Type sous-ensemble, 276
Type(i), 56, 58
Types, 32
habités, 38
Types d’ordre supérieur, 100
Types dépendants, 96, 98, 115
Types de module (signatures),
356
Types habités, 38
Univers, 56
Variables dépendantes, 131
Variables existentielles, 134
Vernaculaire, 32
Définitions de types
501
Inductifs
bool, 35
Produit dépendant, 159
Règles de typage
App, 40, 97, 103
App*, 40
Conv, 58
Lam, 43, 76, 107
Let-in, 45
Prod, 72, 98, 100, 114
Prod-Prop, 72
Prod-Set, 56
Var, 39, 73
Syntaxe
let in, 45
match, 164, 168
Tacticielles
||, 84
repeat, 145
try, 86
Tactics
cbv, 53
compute, 53
Tactiques
apply, 69, 74, 130
apply with, 130
assert, 92
assumption, 70, 73, 127
auto, 92, 215, 224, 240
with, 215
case, 170, 179, 213
cbv, 167, 214
change, 175
clear, 218, 223, 310
cut, 91, 267
destruct, 213
discriminate, 173, 433
eapply, 134, 219, 268
eauto, 215, 219, 267, 268
eexact, 135, 219
elim, 140, 144, 163, 212, 242,
265, 269