Index

=-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

aconst?, 14, 15

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, 42, 43, 44

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, 56, 57

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, 103, 104

cases, 105

cases-construct, 106

Cases-Log, 107

check-and-display-proof, 108

classical-cterm=?, 109

classical-formula=?, 110, 111

clause, 112

Compatibility, 113

Compose, 114

compose-o-substitutions, 115

compose-substitutions, 116

compose-substitutions-wrt, 117

compose-t-substitutions, 118

composition, 119

comprehension term, 120, 121

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

default-var-name, 164, 165

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, 204, 205

eq-refl-aconst, 206

Eq-Symm, 207, 208

eq-symm-aconst, 209

Eq-to-=-1, 210

Eq-to-=-1-nat, 211

Eq-to-=-2, 212

Eq-to-=-2-nat, 213

Eq-Trans, 214, 215

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, 226, 227, 228

Ex-Elim, 229

ex-elim, 230

Ex-ExPartial, 231, 232

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, 242, 243

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, 262, 263, 264

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

formula=?, 300, 301

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

if-construct, 315, 316

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, 323, 324

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

Miller, 385, 386

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-goal, 540, 541

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

token type, 636, 637

Total, 638, 639

total-aconst, 640

Total-to-E, 641

Total-to-E-nat, 642

truth, 643

truth-aconst, 644

Truth-Axiom, 645, 646

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