=-to-E-1, 1
=-to-E-2, 2
=-to-Eq, 3
aconst-to-formula, 4
aconst-to-inst-formula, 5
aconst-to-kind, 6
aconst-to-name, 7
aconst-to-repro-formulas, 8
aconst-to-string, 9
aconst-to-tpsubst, 10
aconst-to-uninst-formula, 11
aconst-without-rules?, 12
aconst=?, 13
add-alg, 16
add-algebras-with-parameters, 17
add-algs, 18
add-computation-rule, 19
add-global-assumption, 20
add-ids, 21
add-new-application, 22
add-param-alg, 23
add-param-algs, 24
add-predconst-name, 25
add-program-constant, 26
add-pvar-name, 27
add-rewrite-rule, 28
add-theorem, 29
add-tvar-name, 30
add-var-name, 31
aga, 32
alg-form-to-name, 33
alg-form-to-types, 34
alg-form?, 35
alg-name-to-arity, 36
alg-name-to-simalg-names, 37
alg-name-to-token-types, 38
alg-name-to-tvars, 39
alg-name-to-typed-constr-names, 40
alg?, 41
all-allpartial-aconst, 45
All-AllPartial-nat, 46
all-form-to-kernel, 47
all-form-to-var, 48
all-form-to-vars-and..., 49
all-form?, 50
all-formula-to-cases-aconst, 51
all-formulas-to-ind-aconst, 52
allnc-form-to-kernel, 53
allnc-form-to-var, 54
allnc-form?, 55
allpartial-all-aconst, 58
AllPartial-All-nat,, 59
and-form-to-left, 60
and-form-to-right, 61
and-form?, 62
animate, 63
animation, 64
arity
of a predicate variable, 65
of a program constant, 66
arity-to-string, 67
arity-to-types, 68
arrow-form-to-arg-type, 69
arrow-form-to-arg-types, 70
arrow-form-to-final-val-type, 71
arrow-form-to-val-type, 72
arrow-form?, 73
arrow-types-to-rec-const, 74
assume, 75
assumption constant, 76
asubst, 77
Atom-False, 78
atom-form-to-kernel, 79
atom-form?, 80
Atom-True, 81
atr-arb-definite-proof, 82
atr-arb-goal-proof, 83
atr-definite?, 84
atr-goal?, 85
atr-goals-to-x-proof, 86
atr-irrel-goal-proof, 87
atr-min-...-to-intuit-ex-proof, 88
atr-min-excl-proof-to-x-proof, 89
atr-rel-definite-proof, 90
atr-relevant?, 91
avar-proof-equal?, 92
avar-to-formula, 93
avar-to-index, 94
avar-to-name, 95
avar=?, 96
avar=?, 97
avar?, 98
Berger, 99
bottom, 100
by-assume-with, 101
by-exnc-assume-with, 102
cases, 105
cases-construct, 106
Cases-Log, 107
check-and-display-proof, 108
classical-cterm=?, 109
clause, 112
Compatibility, 113
Compose, 114
compose-o-substitutions, 115
compose-substitutions, 116
compose-substitutions-wrt, 117
compose-t-substitutions, 118
composition, 119
computation rule, 122
computation rules, 123
consistent-substitutions-wrt?, 124
const-to-arrow-types-or..., 125
const-to-kind, 126
const-to-name, 127
const-to-object-or-arity, 128
const-to-t-deg, 129
const-to-token-type, 130
const-to-tsubst, 131
const-to-tvars, 132
const-to-type, 133
const-to-uninst-type, 134
const=?, 135
const?, 136
constant scheme, 137
constr-name-and-tsubst..., 138
constr-name-to-constr, 139
constr-name?, 140
Constr-Total, 141
Constr-Total-Args, 142
constructor, 143
constructor pattern, 144
context, 145
context-to-avars, 146
context-to-vars, 147
context=?, 148
conversion relation, 149
Coquand, 150
cterm-subst, 151
cterm-substitute, 152
cterm-to-formula, 153
cterm-to-free, 154
cterm-to-string, 155
cterm-to-vars, 156
cterm=?, 157
cterm?, 158
current-goal, 159
current-proof, 160
cut, 161
Cvind-with-measure-11, 162
deanimate, 163
degree of totality, 166
display-constructors, 167
display-current-goal, 168
display-current-goal-with..., 169
display-current-num-goals..., 170
display-global-assumptions, 171
display-normalized-proof, 172
display-normalized-proof-expr, 173
display-normalized-pterm, 174
display-p-substitution, 175
display-program-constants, 176
display-proof, 177
display-proof-expr, 178
display-pterm, 179
display-substitution, 180
display-t-substitution, 181
display-theorems, 182
dnp, 183
dnpe, 184
dnpt, 185
cdp, 186
dp, 187
dpe, 188
dpt, 189
drop, 190
E, 191
E-to-Total, 192
E-to-Total-nat, 193
Efq, 194
Efq-Atom, 195
Efq-Log, 196
Elim, 197
elim, 198
empty-subst, 199
Eq, 200
Eq-Compat, 201
eq-compat-aconst, 202
Eq-Ext, 203
eq-refl-aconst, 206
eq-symm-aconst, 209
Eq-to-=-1, 210
Eq-to-=-1-nat, 211
Eq-to-=-2, 212
Eq-to-=-2-nat, 213
eq-trans-aconst, 216
equal-pvars?, 217
=-Refl-nat, 218
=-Symm-nat, 219
=-Trans-nat, 220
equality, 221
=-to-E-1-nat, 222
=-to-E-2-nat, 223
=-to-Eq-nat, 224
evaluation, 225
Ex-Elim, 229
ex-elim, 230
ex-expartial-aconst, 233
Ex-ExPartial-nat, 234
ex-form-to-kernel, 235
ex-form-to-var, 236
ex-form-to-vars-and..., 237
ex-form?, 238
ex-for...-to-ex-elim-const, 239, 240
ex-formula-to-ex-intro-aconst, 241
Ex-Intro, 244
ex-intro, 245
exc-elim, 246
exc-intro, 247
exca, 248
exca-form-to-kernel, 249
exca-form-to-var, 250
exca-form?, 251
excl, 252
excl-form-to-kernel, 253
excl-form-to-var, 254
excl-form?, 255
exnc-elim, 256
exnc-form-to-kernel, 257
exnc-form-to-var, 258
exnc-form?, 259
exnc-intro, 260
expand-theorems, 261
expartial-ex-aconst, 265
ExPartial-Ex-nat, 266
ext-aconst, 267
Extensionality, 268
extracted program, 269
extracted term, 270
falsity, 271
falsity-log, 272
Filliatre, 273
finalg-to-=-const, 274
finalg-to-=-to-e-1-aconst, 275
finalg-to-=-to-e-2-aconst, 276
finalg-to-=-to-eq-aconst, 277
finalg-to-all-allpartial-aconst, 278
finalg-to-e-const, 279
finalg-to-e-to-total-aconst, 280
finalg-to-eq-to-=-1-aconst, 281
finalg-to-eq-to-=-2-aconst, 282
finalg-to-expartial-ex-aconst, 283
finalg-to-total-to-e-aconst, 284
finalg?, 285
fold-cterm, 286
fold-formula, 287
formula
definite, 288
folded, 289
goal, 290
prime, 291
relevant, 292
unfolded, 293
formula-subst, 294
formula-substitute, 295
formula-to-et-type, 296
formula-to-free, 297
formula-to-prime-subformulas, 298
formula-to-string, 299
get, 302
global assumption, 303
global-assdots-name-to-aconst, 304
goal, 305
goal-subst, 306
goal-to-context, 307
goal-to-formula, 308
goal-to-goalvar, 309
goal=?, 310
ground-type?, 311
Harrop degree, 312
Harrop formula, 313
Huet, 314
imp-form-to-conclusion, 317
imp-form-to-final-conclusion, 318
imp-form-to-premise, 319
imp-form-to-premises, 320
imp-form?, 321
imp-formulas-to-elim-aconst, 322
Ind, 325
ind, 326
induction, 327
inst-with, 328
inst-with-to, 329
Intro, 330
intro, 331
intro-search, 332
Letouzey, 333
lexical analysis, 334
make-=, 335
make-aconst, 336
make-alg, 337
make-all, 338
make-allnc, 339
make-and, 340
make-arity, 341
make-arrow, 342
make-atomic-formula, 343
make-avar, 344
make-const, 345
make-cterm, 346
make-e, 347
make-eq, 348
make-ex, 349
make-exca, 350
make-excl, 351
make-exnc, 352
make-imp, 353
make-inhabited, 354
make-predconst, 355
make-predicate-formula, 356
make-proof-in-aconst-form, 357
make-proof-in-all-elim-form, 358
make-proof-in-all-intro-form, 359
make-proof-in-and-elim-l..., 360
make-proof-in-and-elim-r..., 361
make-proof-in-and-intro-form, 362
make-proof-in-avar-form, 363
make-proof-in-cases-form, 364
make-proof-in-ex-intro-form, 365
make-proof-in-imp-elim-form, 366
make-proof-in-imp-intro-form, 367
make-pvar, 368
make-quant-formula, 369
make-star, 370
make-subst, 371
make-subst-wrt, 372
make-substitution, 373
make-substitution-wrt, 374
make-tensor, 375
make-term-in-abst-form, 376
make-term-in-app-form, 377
make-term-in-const-form, 378
make-term-in-if-form, 379
make-term-in-lcomp-form, 380
make-term-in-pair-form, 381
make-term-in-rcomp-form, 382
make-term-in-var-form, 383
make-total, 384
min-pr, 387
Minpr-with-measure-l11, 388
mk-all, 389
mk-allnc, 390
mk-and, 391
mk-arrow, 392
mk-ex, 393
mk-exca, 394
mk-excl, 395
mk-exnc, 396
mk-imp, 397
mk-neg, 398
mk-neg-log, 399
mk-proof-in-and-intro-form, 400
mk-proof-in-elim-form, 401
mk-proof-in-ex-intro-form, 402
mk-proof-in-intro-form, 403
mk-quant, 404
mk-tensor, 405
mk-term-in-abst-form, 406
mk-term-in-app-form, 407
mk-var, 408
name-hyp, 409
nbe-constr-value-to-constr, 410
nbe-constr-value-to-name, 411
nbe-constr-value?, 412
nbe-constructor-pattern?, 413
nbe-extract, 414
nbe-fam-value?, 415
nbe-formula-to-type, 416
nbe-genargs, 417
nbe-inst?, 418
nbe-make-constr-value, 419
nbe-make-object, 420
nbe-match, 421
nbe-normalize-proof, 422
nbe-normalize-term, 423
nbe-object-app, 424
nbe-object-apply, 425
nbe-object-compose, 426
nbe-object-to-type, 427
nbe-object-to-value, 428
nbe-object?, 429
nbe-pconst-...-to-object, 430
nbe-reflect, 431
nbe-reify, 432
nbe-term-to-object, 433
new-tvar, 434
nf, 435
ng, 436
Nipkow, 437
normalize-formula, 438
normalize-goal, 439
np, 440
nf, 441
nt, 442
number-and-idpredconst-to-intro-aconst, 443
numerated-var-to-index, 444
numerated-var, 445
object-type?, 446
osubst, 447
p-substitution-to-string, 448
pair-elim, 449
parsing, 450
pattern-unify, 451
Paulin-Mohring, 452
Paulson, 453
pconst-name-to-comprules, 454
pconst-name-to-inst-objs, 455
pconst-name-to-object, 456
pconst-name-to-pconst, 457
pconst-name-to-rewrules, 458
pf, 459
pproof-state-to-formula, 460
pproof-state-to-proof, 461
predconst-name-to-arity, 462
predconst-name?, 463
predconst-to-index, 464
predconst-to-name, 465
predconst-to-string, 466
predconst-to-tsubst, 467
predconst-to-uninst-arity, 468
predconst?, 469
predicate constant, 470
predicate-form-to-args, 471
predicate-form-to-predicate, 472
predicate-form?, 473
prename, 474
Presburger, 475
prime-form?, 476
proof-in-aconst-form-to-aconst, 477
proof-in-aconst-form?, 478
proof-in-all-elim-form-to-arg, 479
proof-in-all-elim-form-to-op, 480
proof-in-all-elim-form?, 481
pr...all-intro-form-to-kernel, 482
pr...all-intro-form-to-var, 483
proof-in-all-intro-form?, 484
proof-in-and-elim..., 485
proof-in-and-elim-left-form?, 486
proof-in-and-elim..., 487
proof-in-and-elim-right-form?, 488
pr...and-intro-form-to-left, 489
pr...and-intro-form-to-right, 490
proof-in-and-intro-form?, 491
proof-in-avar-form-to-avar, 492
proof-in-avar-form?, 493
proof-in-cases-form-to-alts, 494
proof-in-cases-form-to-rest, 495
proof-in-cases-form-to-test, 496
proof-in-cases-form?, 497
proof-in-elim-form-to-args, 498
pr...elim-form-to-final-op, 499
proof-in-imp-elim-form-to-arg, 500
proof-in-imp-elim-form-to-op, 501
proof-in-imp-elim-form?, 502
proof-in-imp-intro-form-to-avar, 503
pr...-imp-intro-form-to-kernel, 504
proof-in-imp-intro-form?, 505
proof-in-intro-form-to..., 506
proof-of-efq-at, 507
proof-of-efq-log-at, 508
proof-of-stab-at, 509
proof-of-stab-log-at, 510
proof-subst, 511
proof-substitute, 512
proof-to-aconsts, 513
proof-to-aconsts-without-rules, 514
proof-to-bound-avars, 515
proof-to-context, 516
proof-to-expr, 517
proof-to-extracted-term, 518
proof-to-formula, 519
proof-to-free, 520
proof-to-free-and-bound-avars, 521
proof-to-free-avars, 522
proof-to-soundness-proof, 523
proof=?, 524
proof?, 525
proofs=?, 526
psubst, 527
pt, 528
pv, 529
pvar-cterm-equal?, 530
pvar-name-to-arity, 531
pvar-name?, 532
pvar-to-arity, 533
pvar-to-h-deg, 534
pvar-to-index, 535
pvar-to-name, 536
pvar?, 537
py, 538
Q-clause, 539
Q-sequent, 542
Q-substitution, 543
Q-term, 544
quant-form-to-kernel, 545
quant-form-to-quant, 546
quant-form-to-vars, 547
quant-form?, 548
quant-free?, 549
quant-prime-form?, 550
Rec, 551
Rec, 552
recursion, 553
recursion operator, 554
reduce-efq-and-stab, 555
remove-alg-name, 556
remove-computation-rules-for, 557
remove-global-assumption, 558
remove-predconst-name, 559
remove-program-constant, 560
remove-pvar-name, 561
remove-rewrite-rules-for, 562
remove-theorem, 563
remove-tvar-name, 564
remove-var-name, 565
rename, 566
restrict-substitution-to-args, 567
restrict-substitution-wrt, 568
rewrite rule, 569
rm-exc, 570
save, 571
search, 572
select, 573
semantical model, 574
set-goal, 575
simind, 576
simp, 577
simp-with, 578
special form, 579
split, 580
Stab, 581
Stab-Atom, 582
Stab-Log, 583
star-form-to-left-type, 584
star-form-to-right-type, 585
star-form?, 586
strip, 587
strong elimination, 588
subst-item-equal-wrt?, 589
substitution-equal-wrt?, 590
substitution-equal?, 591
substitution-to-string, 592
synt-total?, 593
tensor-form-to-left, 594
tensor-form-to-parts, 595
tensor-form-to-right, 596
tensor-form?, 597
term-in-abst-form-to-kernel, 598
term-in-abst-form-to-var, 599
term-in-abst-form?, 600
term-in-app-form-to-arg, 601
term-in-app-form-to-args, 602
term-in-app-form-to-final-op, 603
term-in-app-form-to-op, 604
term-in-app-form?, 605
term-in-const-form-to-const, 606
term-in-const-form?, 607
term-in-if-form-to-alts, 608
term-in-if-form-to-rest, 609
term-in-if-form-to-test, 610
term-in-if-form?, 611
term-in-lcomp-form-to-kernel, 612
term-in-lcomp-form?, 613
term-in-pair-form-to-left, 614
term-in-pair-form-to-right, 615
term-in-pair-form?, 616
term-in-rcomp-form-to-kernel, 617
term-in-rcomp-form?, 618
term-in-var-form-to-var, 619
term-in-var-form?, 620
term-subst, 621
term-substitute, 622
term-to-bound, 623
term-to-free, 624
term-to-string, 625
term-to-t-deg, 626
term-to-type, 627
term=?, 628
term?, 629
terms=?, 630
theorem-name-to-aconst, 631, 632
theorem-name-to-inst-proof, 633
theorem-name-to-proof, 634
token, 635
total-aconst, 640
Total-to-E, 641
Total-to-E-nat, 642
truth, 643
truth-aconst, 644
tsubst, 647
tvar-to-index, 648
tvar-to-name, 649
tvar?, 650
type constant, 651
type substitutions, 652
type variable, 653
type-subst, 654
type-substitute, 655
type-to-new-partial-var, 656
type-to-new-var, 657
type-to-string, 658
type?, 659
undo, 660
unfold-cterm, 661
unfold-formula, 662
use, 663
use-with, 664
var-form?, 665
var-term-equal?, 666
var-to-index, 667
var-to-name, 668
var-to-new-var, 669
var-to-t-deg, 670
var-to-type, 671
var?, 672
vector notation, 673