The bourbaki Reference Manual

Table of Contents

Next: , Previous: , Up: (dir)   [Contents][Index]

The bourbaki Reference Manual

This is the bourbaki Reference Manual, version 3.5, generated automatically by Declt version 2.3 "Robert April" on Wed Mar 14 03:00:00 2018 GMT+0.


Next: , Previous: , Up: Top   [Contents][Index]

1 Systems

The main system appears first, followed by any subsystem dependency.


Previous: , Up: Systems   [Contents][Index]

1.1 bourbaki

Version

3.5

Source

bourbaki.asd (file)

Component

bourbaki (module)


Next: , Previous: , Up: Top   [Contents][Index]

2 Modules

Modules are listed depth-first from the system components tree.


Previous: , Up: Modules   [Contents][Index]

2.1 bourbaki/bourbaki

Parent

bourbaki (system)

Location

Components

Next: , Previous: , Up: Top   [Contents][Index]

3 Files

Files are sorted by type and then listed depth-first from the systems components trees.


Previous: , Up: Files   [Contents][Index]

3.1 Lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.1 bourbaki.asd

Location

bourbaki.asd

Systems

bourbaki (system)

Packages

bourbaki-system


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.2 bourbaki/bourbaki/package.lisp

Parent

bourbaki (module)

Location

package.lisp

Packages

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.3 bourbaki/bourbaki/types.lisp

Dependency

package.lisp (file)

Parent

bourbaki (module)

Location

types.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.4 bourbaki/bourbaki/variables.lisp

Dependency

types.lisp (file)

Parent

bourbaki (module)

Location

variables.lisp

Exported Definitions
Internal Definitions

mkrootctx (function)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.5 bourbaki/bourbaki/symbol.lisp

Dependency

types.lisp (file)

Parent

bourbaki (module)

Location

symbol.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.6 bourbaki/bourbaki/util.lisp

Dependency

variables.lisp (file)

Parent

bourbaki (module)

Location

util.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.7 bourbaki/bourbaki/symref.lisp

Dependencies
Parent

bourbaki (module)

Location

symref.lisp

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.8 bourbaki/bourbaki/pattern.lisp

Dependencies
Parent

bourbaki (module)

Location

pattern.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.9 bourbaki/bourbaki/proof.lisp

Dependency

pattern.lisp (file)

Parent

bourbaki (module)

Location

proof.lisp

Exported Definitions

provenp (function)

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.10 bourbaki/bourbaki/print.lisp

Dependencies
Parent

bourbaki (module)

Location

print.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.11 bourbaki/bourbaki/distinct.lisp

Dependencies
Parent

bourbaki (module)

Location

distinct.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.12 bourbaki/bourbaki/symtree.lisp

Dependencies
Parent

bourbaki (module)

Location

symtree.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.13 bourbaki/bourbaki/context.lisp

Dependencies
Parent

bourbaki (module)

Location

context.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.14 bourbaki/bourbaki/verify.lisp

Dependencies
Parent

bourbaki (module)

Location

verify.lisp

Exported Definitions

verify (function)

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.15 bourbaki/bourbaki/stats.lisp

Dependency

verify.lisp (file)

Parent

bourbaki (module)

Location

stats.lisp

Exported Definitions
Internal Definitions

collect-stats-thr (function)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.16 bourbaki/bourbaki/parse.lisp

Dependencies
Parent

bourbaki (module)

Location

parse.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.17 bourbaki/bourbaki/define.lisp

Dependency

parse.lisp (file)

Parent

bourbaki (module)

Location

define.lisp

Exported Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.18 bourbaki/bourbaki/read.lisp

Dependency

package.lisp (file)

Parent

bourbaki (module)

Location

read.lisp

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.19 bourbaki/bourbaki/metatheorem.lisp

Dependency

context.lisp (file)

Parent

bourbaki (module)

Location

metatheorem.lisp

Exported Definitions

Previous: , Up: Lisp files   [Contents][Index]

3.1.20 bourbaki/bourbaki/parse-proof.lisp

Dependencies
Parent

bourbaki (module)

Location

parse-proof.lisp

Exported Definitions

Next: , Previous: , Up: Top   [Contents][Index]

4 Packages

Packages are listed by definition order.


Next: , Previous: , Up: Packages   [Contents][Index]

4.1 bourbaki-system

Source

bourbaki.asd

Use List

Next: , Previous: , Up: Packages   [Contents][Index]

4.2 bourbaki-user

Source

package.lisp (file)

Use List

Previous: , Up: Packages   [Contents][Index]

4.3 bourbaki

Source

package.lisp (file)

Use List

common-lisp

Used By List

bourbaki-user

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

5 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.


Next: , Previous: , Up: Definitions   [Contents][Index]

5.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.1 Special variables

Special Variable: *bourbaki-debug*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *bourbaki-library-path*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *bourbaki-version*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *current-context*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *current-proof*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *meta-context*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *root-context*
Package

bourbaki

Source

variables.lisp (file)

Special Variable: *theorem-patterns*
Package

bourbaki

Source

variables.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.2 Macros

Macro: acond &body CONDS
Package

bourbaki

Source

util.lisp (file)

Macro: aif TEST THEN &optional ELSE
Package

bourbaki

Source

util.lisp (file)

Macro: alias ALIAS-NAME VARS RHS
Package

bourbaki

Source

define.lisp (file)

Macro: ass &rest LST

Axiom or theorem assertion

Package

bourbaki

Source

parse.lisp (file)

Macro: ax NAME VARS &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: collecting &body FORMS

Collect things into a list forwards. Within the body of this macro
The form ‘(COLLECT THING)’ will collect THING into the list returned by COLLECTING. Uses a tail pointer -> efficient.

Package

bourbaki

Source

util.lisp (file)

Macro: copy-th THR SUFFIX ITEMS &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: def DF-NAME SYM-TYPE SYM-NAME VARS DUMMY RHS &body BODY
Package

bourbaki

Source

define.lisp (file)

Macro: defcontext CLASS NAME VARS &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: dist &rest LST

Distinct variable conditions

Package

bourbaki

Source

parse.lisp (file)

Macro: extend-metath REF ARGS &body BODY
Package

bourbaki

Source

metatheorem.lisp (file)

Macro: hypo &rest LST

Axiom or theorem hypotheses

Package

bourbaki

Source

parse.lisp (file)

Macro: if-match PAT EXPR THEN &optional ELSE
Package

bourbaki

Source

pattern.lisp (file)

Macro: in-context REF &body BODY

Enter an existing context

Package

bourbaki

Source

parse.lisp (file)

Macro: let-once (VAR EXPR) &body BODY
Package

bourbaki

Source

pattern.lisp (file)

Macro: linear-subproof HYP ASS &body LINES
Package

bourbaki

Source

parse-proof.lisp (file)

Macro: loc &rest VARSPEC
Package

bourbaki

Source

parse.lisp (file)

Macro: local NAME &body BODY

Enter a subcontext, creating it if it did not already exist

Package

bourbaki

Source

parse.lisp (file)

Macro: match-case EXPR &body CASES
Package

bourbaki

Source

pattern.lisp (file)

Macro: meta &rest SPECS
Package

bourbaki

Source

parse.lisp (file)

Macro: metath NAME ARGS &body BODY
Package

bourbaki

Source

metatheorem.lisp (file)

Macro: module NAME &body BODY

Enter a top-level context, creating it if it did not already exist

Package

bourbaki

Source

parse.lisp (file)

Macro: parse-vars VARLIST &optional CLASS
Package

bourbaki

Source

parse.lisp (file)

Macro: pattern VARS RHS
Package

bourbaki

Source

define.lisp (file)

Macro: prim TYPE NAME VARS &body BODY

A primitive symbol

Package

bourbaki

Source

parse.lisp (file)

Macro: proof &body LINES
Package

bourbaki

Source

parse-proof.lisp (file)

Macro: providing CTX &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: set-symkind-eq-op KIND OP
Package

bourbaki

Source

parse.lisp (file)

Macro: subproof (&key HYPO ASSERT) &body BODY
Package

bourbaki

Source

parse-proof.lisp (file)

Macro: symkind NAME &key SUPER
Package

bourbaki

Source

parse.lisp (file)

Macro: th NAME VARS &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: th-pattern REF
Package

bourbaki

Source

parse.lisp (file)

Macro: theory NAME VARS &body BODY
Package

bourbaki

Source

parse.lisp (file)

Macro: var TYPE CLASS
Package

bourbaki

Source

parse.lisp (file)

Macro: var2 TYPE NAME CLASS
Package

bourbaki

Source

parse.lisp (file)

Macro: virtual-metath NAME ARGS &body BODY
Package

bourbaki

Source

metatheorem.lisp (file)

Macro: with-gensyms SYMS &body BODY
Package

bourbaki

Source

util.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.3 Functions

Function: collect-stats REF
Package

bourbaki

Source

stats.lisp (file)

Function: context-assert INSTANCE
Function: (setf context-assert) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-class INSTANCE
Function: (setf context-class) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-distinct INSTANCE
Function: (setf context-distinct) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-exports INSTANCE
Function: (setf context-exports) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-hypo INSTANCE
Function: (setf context-hypo) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-imports INSTANCE
Function: (setf context-imports) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-meta INSTANCE
Function: (setf context-meta) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-name INSTANCE
Function: (setf context-name) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-proof INSTANCE
Function: (setf context-proof) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-syms INSTANCE
Function: (setf context-syms) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-type INSTANCE
Function: (setf context-type) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: context-vars INSTANCE
Function: (setf context-vars) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: create-context &key NAME TYPE PARENT CLASS

Create a subcontext of ‘parent’ with specified type

Package

bourbaki

Source

context.lisp (file)

Function: dvc-list LST THR
Package

bourbaki

Source

distinct.lisp (file)

Function: dvc-var VAR THR
Package

bourbaki

Source

distinct.lisp (file)

Function: export STR &key PROOF
Package

bourbaki

Source

parse.lisp (file)

Function: flatten LST
Package

bourbaki

Source

util.lisp (file)

Function: flush ()
Package

bourbaki

Source

context.lisp (file)

Function: import STR &key PROOF
Package

bourbaki

Source

parse.lisp (file)

Function: in-tree TREE WFF
Package

bourbaki

Source

pattern.lisp (file)

Function: insert-export TARGET &key WHERE PROOF
Package

bourbaki

Source

context.lisp (file)

Function: insert-import TARGET &key WHERE PROOF
Package

bourbaki

Source

context.lisp (file)

Function: insert-pat TREE REF
Package

bourbaki

Source

pattern.lisp (file)

Function: insert-sym REF &optional CONTEXT NAME
Package

bourbaki

Source

context.lisp (file)

Function: insert-wff TREE WFF &optional VAL
Package

bourbaki

Source

pattern.lisp (file)

Function: load-aux FILENAME &optional TYPE
Package

bourbaki

Source

util.lisp (file)

Function: make-context &key (SYMS SYMS) (IMPORTS IMPORTS) (EXPORTS EXPORTS) (TYPE TYPE) (CLASS CLASS) (META META) (NAME NAME) (VARS VARS) (DISTINCT DISTINCT) (HYPO HYPO) (ASSERT ASSERT) (PROOF PROOF)
Package

bourbaki

Source

types.lisp (file)

Function: make-pattern-tree &key (SYMS SYMS) (REF REF)
Package

bourbaki

Source

types.lisp (file)

Function: make-subproof &key (REF REF) (HYPO HYPO) (ASSERT ASSERT) (PREV PREV) (SUB SUB)
Package

bourbaki

Source

types.lisp (file)

Function: make-symref &key (TARGET TARGET) (ARGS-NEEDED ARGS-NEEDED) (FN FN) (CLASS CLASS) (PROOF PROOF)
Package

bourbaki

Source

types.lisp (file)

Function: makevarlist THR
Package

bourbaki

Source

symtree.lisp (file)

Function: match-tree TREE WFF
Package

bourbaki

Source

pattern.lisp (file)

Function: mkcontext REF
Package

bourbaki

Source

context.lisp (file)

Function: mklist X
Package

bourbaki

Source

util.lisp (file)

Function: mkvar TYPE CLASS &key NAME BOUND

Create a symbol of specified type

Package

bourbaki

Source

symbol.lisp (file)

Function: parse-subproof ITEM
Package

bourbaki

Source

parse-proof.lisp (file)

Function: pattern-tree-ref INSTANCE
Function: (setf pattern-tree-ref) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: pattern-tree-syms INSTANCE
Function: (setf pattern-tree-syms) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: print-symtree TREE &optional STREAM MODE
Package

bourbaki

Source

print.lisp (file)

Function: print-theorem REF &optional MODE
Package

bourbaki

Source

print.lisp (file)

Function: provenp WFF
Package

bourbaki

Source

proof.lisp (file)

Function: replace-vars STR SMAP

Substitute some variables in a wff

Package

bourbaki

Source

symtree.lisp (file)

Function: require NAME MODULE &key PROVIDE
Package

bourbaki

Source

context.lisp (file)

Function: seek-create-ctx NAME &optional CLASS CONTEXT
Package

bourbaki

Source

context.lisp (file)

Function: seek-sym MODE NAME1 &rest NAMES

Seeks for a theorem or context or symbol.

Package

bourbaki

Source

context.lisp (file)

Function: show-proof REF &optional MODE
Package

bourbaki

Source

print.lisp (file)

Function: show-stats REF
Package

bourbaki

Source

stats.lisp (file)

Function: show-unused REF
Package

bourbaki

Source

stats.lisp (file)

Function: smap THR EXPR
Package

bourbaki

Source

symtree.lisp (file)

Function: subkindp TYPE1 TYPE2
Package

bourbaki

Source

symbol.lisp (file)

Function: subproof-assert INSTANCE
Function: (setf subproof-assert) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: subproof-hypo INSTANCE
Function: (setf subproof-hypo) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: subproof-prev INSTANCE
Function: (setf subproof-prev) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: subproof-ref INSTANCE
Function: (setf subproof-ref) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: subproof-sub INSTANCE
Function: (setf subproof-sub) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-args-needed INSTANCE
Function: (setf symref-args-needed) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-fn INSTANCE
Function: (setf symref-fn) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-proof INSTANCE
Function: (setf symref-proof) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-target INSTANCE
Function: (setf symref-target) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symtree-parse STR

Parse an expression returned by symstr-reader

Package

bourbaki

Source

context.lisp (file)

Function: verify REF &optional NESTED
Package

bourbaki

Source

verify.lisp (file)

Function: wff-equal LHS RHS

Check if two symtrees are equal

Package

bourbaki

Source

symtree.lisp (file)

Function: wff-type STR

Type of a symtree

Package

bourbaki

Source

symtree.lisp (file)

Function: wffp STR

Check if str is a well-formed symtree

Package

bourbaki

Source

symtree.lisp (file)

Function: wrap-ctx CTX &optional NVARS
Package

bourbaki

Source

context.lisp (file)


Previous: , Up: Exported definitions   [Contents][Index]

5.1.4 Structures

Structure: context ()

Symbol, theorem or context

Package

bourbaki

Source

types.lisp (file)

Direct superclasses

structure-object (structure)

Direct methods

print-object (method)

Direct slots
Slot: syms
Initform

(make-hash-table :test (quote equal))

Readers

context-syms (function)

Writers

(setf context-syms) (function)

Slot: imports
Readers

context-imports (function)

Writers

(setf context-imports) (function)

Slot: exports
Readers

context-exports (function)

Writers

(setf context-exports) (function)

Slot: type
Readers

context-type (function)

Writers

(setf context-type) (function)

Slot: class
Readers

context-class (function)

Writers

(setf context-class) (function)

Slot: meta
Initform

(make-hash-table :test (quote eq))

Readers

context-meta (function)

Writers

(setf context-meta) (function)

Slot: name
Readers

context-name (function)

Writers

(setf context-name) (function)

Slot: vars
Readers

context-vars (function)

Writers

(setf context-vars) (function)

Slot: distinct
Readers

context-distinct (function)

Writers

(setf context-distinct) (function)

Slot: hypo
Readers

context-hypo (function)

Writers

(setf context-hypo) (function)

Slot: assert
Readers

context-assert (function)

Writers

(setf context-assert) (function)

Slot: proof
Readers

context-proof (function)

Writers

(setf context-proof) (function)

Structure: pattern-tree ()
Package

bourbaki

Source

types.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: syms
Initform

(make-hash-table :test (quote eq))

Readers

pattern-tree-syms (function)

Writers

(setf pattern-tree-syms) (function)

Slot: ref
Readers

pattern-tree-ref (function)

Writers

(setf pattern-tree-ref) (function)

Structure: subproof ()
Package

bourbaki

Source

types.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: ref
Readers

subproof-ref (function)

Writers

(setf subproof-ref) (function)

Slot: hypo
Readers

subproof-hypo (function)

Writers

(setf subproof-hypo) (function)

Slot: assert
Readers

subproof-assert (function)

Writers

(setf subproof-assert) (function)

Slot: prev
Readers

subproof-prev (function)

Writers

(setf subproof-prev) (function)

Slot: sub
Readers

subproof-sub (function)

Writers

(setf subproof-sub) (function)

Structure: symkind ()

A symbol type

Package

bourbaki

Source

types.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: name
Initform

""

Readers

symkind-name (function)

Writers

(setf symkind-name) (function)

Slot: eq-op
Readers

symkind-eq-op (function)

Writers

(setf symkind-eq-op) (function)

Slot: meta
Initform

(make-hash-table :test (quote eq))

Readers

symkind-meta (function)

Writers

(setf symkind-meta) (function)

Slot: super
Readers

symkind-super (function)

Writers

(setf symkind-super) (function)

Structure: symref ()

Reference to a symbol or context

Package

bourbaki

Source

types.lisp (file)

Direct superclasses

structure-object (structure)

Direct methods

print-object (method)

Direct slots
Slot: target
Readers

symref-target (function)

Writers

(setf symref-target) (function)

Slot: args-needed
Readers

symref-args-needed (function)

Writers

(setf symref-args-needed) (function)

Slot: fn
Readers

symref-fn (function)

Writers

(setf symref-fn) (function)

Slot: class
Readers

symref-class (function)

Writers

(setf symref-class) (function)

Slot: proof
Readers

symref-proof (function)

Writers

(setf symref-proof) (function)


Previous: , Up: Definitions   [Contents][Index]

5.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.1 Special variables

Special Variable: *mkvar-counter*
Package

bourbaki

Source

symbol.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.2 Macros

Macro: do-proof (VAR PF) &body BODY
Package

bourbaki

Source

proof.lisp (file)


Previous: , Up: Internal definitions   [Contents][Index]

5.2.3 Functions

Function: apply-ref REF ARGS
Package

bourbaki

Source

symref.lisp (file)

Function: apply-ref-proof REF ARGS
Package

bourbaki

Source

symref.lisp (file)

Function: args X
Package

bourbaki

Source

util.lisp (file)

Function: bsym-reader STREAM ALT
Package

bourbaki

Source

read.lisp (file)

Function: cartesian-product VARS1 VARS2

Cartesian product of two lists

Package

bourbaki

Source

util.lisp (file)

Function: collect-stats-thr THR
Package

bourbaki

Source

stats.lisp (file)

Function: collect-vars STR VARLIST

The list of symbols from varlist that occur in str

Package

bourbaki

Source

symtree.lisp (file)

Function: compose-proof LHS RHS
Package

bourbaki

Source

symref.lisp (file)

Function: compose-ref LHS RHS

Helper function for seek-sym.
Creates a composed symref from a context and a symref.

Package

bourbaki

Source

symref.lisp (file)

Function: context-p OBJECT
Package

bourbaki

Source

types.lisp (file)

Function: context-printer OBJ STREAM
Package

bourbaki

Source

types.lisp (file)

Function: copy-context INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: copy-items LST FROM
Package

bourbaki

Source

parse.lisp (file)

Function: copy-pattern-tree INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: copy-subproof INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: copy-symkind INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: copy-symref INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: dvc LIST1 LIST2 THR
Package

bourbaki

Source

distinct.lisp (file)

Function: dvc-1 CND THR
Package

bourbaki

Source

distinct.lisp (file)

Function: dvc-satisfied THREF SMAP CONDLIST VARLIST

Check that distinct variable conditions are satisfied in a proof step.

Package

bourbaki

Source

distinct.lisp (file)

Function: flatten-1 WFF
Package

bourbaki

Source

util.lisp (file)

Function: get-symkind SYM
Package

bourbaki

Source

parse.lisp (file)

Function: highest-number-in TREE
Package

bourbaki

Source

util.lisp (file)

Function: int-list N
Package

bourbaki

Source

util.lisp (file)

Function: lib-path-name FILENAME &optional TYPE
Package

bourbaki

Source

util.lisp (file)

Function: make-symkind &key (NAME NAME) (EQ-OP EQ-OP) (META META) (SUPER SUPER)
Package

bourbaki

Source

types.lisp (file)

Function: makevarlist-r THR
Package

bourbaki

Source

symtree.lisp (file)

Function: matcher-fn PAT
Package

bourbaki

Source

pattern.lisp (file)

Function: mkrootctx ()
Package

bourbaki

Source

variables.lisp (file)

Function: op X
Package

bourbaki

Source

util.lisp (file)

Function: pair-eq LHS RHS

Equality of unordered pairs

Package

bourbaki

Source

util.lisp (file)

Function: parse-thr-ref TREE &optional REF ARGS
Package

bourbaki

Source

context.lisp (file)

Function: parse-varspec TYPE NAMES CLASS
Package

bourbaki

Source

parse.lisp (file)

Function: pat-var-p EXPR
Package

bourbaki

Source

pattern.lisp (file)

Function: pat-vars-in EXPR
Package

bourbaki

Source

pattern.lisp (file)

Function: pattern-to-ref PAT &optional CLASS
Package

bourbaki

Source

symref.lisp (file)

Function: pattern-tree-p OBJECT
Package

bourbaki

Source

types.lisp (file)

Function: permute-ref REF SMAP
Package

bourbaki

Source

pattern.lisp (file)

Function: permute-vars PAT REF
Package

bourbaki

Source

pattern.lisp (file)

Function: potential-vars LST DIST EXPR

List of variables that potentially occur in a symtree

Package

bourbaki

Source

symtree.lisp (file)

Function: print-symtree-aux STREAM STR &optional MODE FOO
Package

bourbaki

Source

print.lisp (file)

Function: print-symtree-debug STR
Package

bourbaki

Source

print.lisp (file)

Function: push-second X LST
Package

bourbaki

Source

util.lisp (file)

Function: r-int-list N
Package

bourbaki

Source

util.lisp (file)

Function: read-names STREAM
Package

bourbaki

Source

read.lisp (file)

Function: read-segment STREAM
Package

bourbaki

Source

read.lisp (file)

Function: ref-to-pattern REF
Package

bourbaki

Source

symref.lisp (file)

Function: replace-proof-vars PF SMAP

Substitute some variables in a proof

Package

bourbaki

Source

symtree.lisp (file)

Function: seek-ctx-exports NAME REF
Package

bourbaki

Source

context.lisp (file)

Function: seek-ctx-imports NAME &optional CONTEXT

Helper function for seek-sym.
Seeks for a theorem or symbol in imported contexts.

Package

bourbaki

Source

context.lisp (file)

Function: simple-splice LST LEN FN
Package

bourbaki

Source

util.lisp (file)

Function: splice LST LEN FN
Package

bourbaki

Source

util.lisp (file)

Function: subproof-p OBJECT
Package

bourbaki

Source

types.lisp (file)

Function: symkind-eq-op INSTANCE
Function: (setf symkind-eq-op) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symkind-meta INSTANCE
Function: (setf symkind-meta) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symkind-name INSTANCE
Function: (setf symkind-name) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symkind-p OBJECT
Package

bourbaki

Source

types.lisp (file)

Function: symkind-super INSTANCE
Function: (setf symkind-super) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-class INSTANCE
Function: (setf symref-class) VALUE INSTANCE
Package

bourbaki

Source

types.lisp (file)

Function: symref-p OBJECT
Package

bourbaki

Source

types.lisp (file)

Function: symref-printer OBJ STREAM
Package

bourbaki

Source

types.lisp (file)

Function: symstr-reader STREAM CHAR
Package

bourbaki

Source

read.lisp (file)

Function: symstr-reader-aux STREAM ALT
Package

bourbaki

Source

read.lisp (file)

Function: symtree-parse-aux ()

Helper function for symtree-parse

Package

bourbaki

Source

context.lisp (file)

Function: symtree-reparse STR

Helper function for replace-vars

Package

bourbaki

Source

symtree.lisp (file)

Function: symtree-reparse-aux STR

Helper function for replace-vars

Package

bourbaki

Source

symtree.lisp (file)

Function: theorem-sym-p SYM
Package

bourbaki

Source

symbol.lisp (file)

Function: thref-reader STREAM CHAR
Package

bourbaki

Source

read.lisp (file)

Function: verify-1 THR

Verify that the hypotheses and assertion of thr are wff and the proof is correct.

Package

bourbaki

Source

verify.lisp (file)

Function: verify-def DEFN

Verify soundness of a definition

Package

bourbaki

Source

verify.lisp (file)

Function: verify-subproof PF VARLIST DVC NUM
Package

bourbaki

Source

verify.lisp (file)

Function: walk-proof-tree THR FN &optional NESTED
Package

bourbaki

Source

proof.lisp (file)


Previous: , Up: Top   [Contents][Index]

Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts

Jump to:   B   F   L   M  
Index Entry  Section

B
bourbaki.asd: The bourbaki<dot>asd file
bourbaki/bourbaki: The bourbaki/bourbaki module
bourbaki/bourbaki/context.lisp: The bourbaki/bourbaki/context<dot>lisp file
bourbaki/bourbaki/define.lisp: The bourbaki/bourbaki/define<dot>lisp file
bourbaki/bourbaki/distinct.lisp: The bourbaki/bourbaki/distinct<dot>lisp file
bourbaki/bourbaki/metatheorem.lisp: The bourbaki/bourbaki/metatheorem<dot>lisp file
bourbaki/bourbaki/package.lisp: The bourbaki/bourbaki/package<dot>lisp file
bourbaki/bourbaki/parse-proof.lisp: The bourbaki/bourbaki/parse-proof<dot>lisp file
bourbaki/bourbaki/parse.lisp: The bourbaki/bourbaki/parse<dot>lisp file
bourbaki/bourbaki/pattern.lisp: The bourbaki/bourbaki/pattern<dot>lisp file
bourbaki/bourbaki/print.lisp: The bourbaki/bourbaki/print<dot>lisp file
bourbaki/bourbaki/proof.lisp: The bourbaki/bourbaki/proof<dot>lisp file
bourbaki/bourbaki/read.lisp: The bourbaki/bourbaki/read<dot>lisp file
bourbaki/bourbaki/stats.lisp: The bourbaki/bourbaki/stats<dot>lisp file
bourbaki/bourbaki/symbol.lisp: The bourbaki/bourbaki/symbol<dot>lisp file
bourbaki/bourbaki/symref.lisp: The bourbaki/bourbaki/symref<dot>lisp file
bourbaki/bourbaki/symtree.lisp: The bourbaki/bourbaki/symtree<dot>lisp file
bourbaki/bourbaki/types.lisp: The bourbaki/bourbaki/types<dot>lisp file
bourbaki/bourbaki/util.lisp: The bourbaki/bourbaki/util<dot>lisp file
bourbaki/bourbaki/variables.lisp: The bourbaki/bourbaki/variables<dot>lisp file
bourbaki/bourbaki/verify.lisp: The bourbaki/bourbaki/verify<dot>lisp file

F
File, Lisp, bourbaki.asd: The bourbaki<dot>asd file
File, Lisp, bourbaki/bourbaki/context.lisp: The bourbaki/bourbaki/context<dot>lisp file
File, Lisp, bourbaki/bourbaki/define.lisp: The bourbaki/bourbaki/define<dot>lisp file
File, Lisp, bourbaki/bourbaki/distinct.lisp: The bourbaki/bourbaki/distinct<dot>lisp file
File, Lisp, bourbaki/bourbaki/metatheorem.lisp: The bourbaki/bourbaki/metatheorem<dot>lisp file
File, Lisp, bourbaki/bourbaki/package.lisp: The bourbaki/bourbaki/package<dot>lisp file
File, Lisp, bourbaki/bourbaki/parse-proof.lisp: The bourbaki/bourbaki/parse-proof<dot>lisp file
File, Lisp, bourbaki/bourbaki/parse.lisp: The bourbaki/bourbaki/parse<dot>lisp file
File, Lisp, bourbaki/bourbaki/pattern.lisp: The bourbaki/bourbaki/pattern<dot>lisp file
File, Lisp, bourbaki/bourbaki/print.lisp: The bourbaki/bourbaki/print<dot>lisp file
File, Lisp, bourbaki/bourbaki/proof.lisp: The bourbaki/bourbaki/proof<dot>lisp file
File, Lisp, bourbaki/bourbaki/read.lisp: The bourbaki/bourbaki/read<dot>lisp file
File, Lisp, bourbaki/bourbaki/stats.lisp: The bourbaki/bourbaki/stats<dot>lisp file
File, Lisp, bourbaki/bourbaki/symbol.lisp: The bourbaki/bourbaki/symbol<dot>lisp file
File, Lisp, bourbaki/bourbaki/symref.lisp: The bourbaki/bourbaki/symref<dot>lisp file
File, Lisp, bourbaki/bourbaki/symtree.lisp: The bourbaki/bourbaki/symtree<dot>lisp file
File, Lisp, bourbaki/bourbaki/types.lisp: The bourbaki/bourbaki/types<dot>lisp file
File, Lisp, bourbaki/bourbaki/util.lisp: The bourbaki/bourbaki/util<dot>lisp file
File, Lisp, bourbaki/bourbaki/variables.lisp: The bourbaki/bourbaki/variables<dot>lisp file
File, Lisp, bourbaki/bourbaki/verify.lisp: The bourbaki/bourbaki/verify<dot>lisp file

L
Lisp File, bourbaki.asd: The bourbaki<dot>asd file
Lisp File, bourbaki/bourbaki/context.lisp: The bourbaki/bourbaki/context<dot>lisp file
Lisp File, bourbaki/bourbaki/define.lisp: The bourbaki/bourbaki/define<dot>lisp file
Lisp File, bourbaki/bourbaki/distinct.lisp: The bourbaki/bourbaki/distinct<dot>lisp file
Lisp File, bourbaki/bourbaki/metatheorem.lisp: The bourbaki/bourbaki/metatheorem<dot>lisp file
Lisp File, bourbaki/bourbaki/package.lisp: The bourbaki/bourbaki/package<dot>lisp file
Lisp File, bourbaki/bourbaki/parse-proof.lisp: The bourbaki/bourbaki/parse-proof<dot>lisp file
Lisp File, bourbaki/bourbaki/parse.lisp: The bourbaki/bourbaki/parse<dot>lisp file
Lisp File, bourbaki/bourbaki/pattern.lisp: The bourbaki/bourbaki/pattern<dot>lisp file
Lisp File, bourbaki/bourbaki/print.lisp: The bourbaki/bourbaki/print<dot>lisp file
Lisp File, bourbaki/bourbaki/proof.lisp: The bourbaki/bourbaki/proof<dot>lisp file
Lisp File, bourbaki/bourbaki/read.lisp: The bourbaki/bourbaki/read<dot>lisp file
Lisp File, bourbaki/bourbaki/stats.lisp: The bourbaki/bourbaki/stats<dot>lisp file
Lisp File, bourbaki/bourbaki/symbol.lisp: The bourbaki/bourbaki/symbol<dot>lisp file
Lisp File, bourbaki/bourbaki/symref.lisp: The bourbaki/bourbaki/symref<dot>lisp file
Lisp File, bourbaki/bourbaki/symtree.lisp: The bourbaki/bourbaki/symtree<dot>lisp file
Lisp File, bourbaki/bourbaki/types.lisp: The bourbaki/bourbaki/types<dot>lisp file
Lisp File, bourbaki/bourbaki/util.lisp: The bourbaki/bourbaki/util<dot>lisp file
Lisp File, bourbaki/bourbaki/variables.lisp: The bourbaki/bourbaki/variables<dot>lisp file
Lisp File, bourbaki/bourbaki/verify.lisp: The bourbaki/bourbaki/verify<dot>lisp file

M
Module, bourbaki/bourbaki: The bourbaki/bourbaki module

Jump to:   B   F   L   M  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   (  
A   B   C   D   E   F   G   H   I   L   M   O   P   R   S   T   V   W  
Index Entry  Section

(
(setf context-assert): Exported functions
(setf context-class): Exported functions
(setf context-distinct): Exported functions
(setf context-exports): Exported functions
(setf context-hypo): Exported functions
(setf context-imports): Exported functions
(setf context-meta): Exported functions
(setf context-name): Exported functions
(setf context-proof): Exported functions
(setf context-syms): Exported functions
(setf context-type): Exported functions
(setf context-vars): Exported functions
(setf pattern-tree-ref): Exported functions
(setf pattern-tree-syms): Exported functions
(setf subproof-assert): Exported functions
(setf subproof-hypo): Exported functions
(setf subproof-prev): Exported functions
(setf subproof-ref): Exported functions
(setf subproof-sub): Exported functions
(setf symkind-eq-op): Internal functions
(setf symkind-meta): Internal functions
(setf symkind-name): Internal functions
(setf symkind-super): Internal functions
(setf symref-args-needed): Exported functions
(setf symref-class): Internal functions
(setf symref-fn): Exported functions
(setf symref-proof): Exported functions
(setf symref-target): Exported functions

A
acond: Exported macros
aif: Exported macros
alias: Exported macros
apply-ref: Internal functions
apply-ref-proof: Internal functions
args: Internal functions
ass: Exported macros
ax: Exported macros

B
bsym-reader: Internal functions

C
cartesian-product: Internal functions
collect-stats: Exported functions
collect-stats-thr: Internal functions
collect-vars: Internal functions
collecting: Exported macros
compose-proof: Internal functions
compose-ref: Internal functions
context-assert: Exported functions
context-class: Exported functions
context-distinct: Exported functions
context-exports: Exported functions
context-hypo: Exported functions
context-imports: Exported functions
context-meta: Exported functions
context-name: Exported functions
context-p: Internal functions
context-printer: Internal functions
context-proof: Exported functions
context-syms: Exported functions
context-type: Exported functions
context-vars: Exported functions
copy-context: Internal functions
copy-items: Internal functions
copy-pattern-tree: Internal functions
copy-subproof: Internal functions
copy-symkind: Internal functions
copy-symref: Internal functions
copy-th: Exported macros
create-context: Exported functions

D
def: Exported macros
defcontext: Exported macros
dist: Exported macros
do-proof: Internal macros
dvc: Internal functions
dvc-1: Internal functions
dvc-list: Exported functions
dvc-satisfied: Internal functions
dvc-var: Exported functions

E
export: Exported functions
extend-metath: Exported macros

F
flatten: Exported functions
flatten-1: Internal functions
flush: Exported functions
Function, (setf context-assert): Exported functions
Function, (setf context-class): Exported functions
Function, (setf context-distinct): Exported functions
Function, (setf context-exports): Exported functions
Function, (setf context-hypo): Exported functions
Function, (setf context-imports): Exported functions
Function, (setf context-meta): Exported functions
Function, (setf context-name): Exported functions
Function, (setf context-proof): Exported functions
Function, (setf context-syms): Exported functions
Function, (setf context-type): Exported functions
Function, (setf context-vars): Exported functions
Function, (setf pattern-tree-ref): Exported functions
Function, (setf pattern-tree-syms): Exported functions
Function, (setf subproof-assert): Exported functions
Function, (setf subproof-hypo): Exported functions
Function, (setf subproof-prev): Exported functions
Function, (setf subproof-ref): Exported functions
Function, (setf subproof-sub): Exported functions
Function, (setf symkind-eq-op): Internal functions
Function, (setf symkind-meta): Internal functions
Function, (setf symkind-name): Internal functions
Function, (setf symkind-super): Internal functions
Function, (setf symref-args-needed): Exported functions
Function, (setf symref-class): Internal functions
Function, (setf symref-fn): Exported functions
Function, (setf symref-proof): Exported functions
Function, (setf symref-target): Exported functions
Function, apply-ref: Internal functions
Function, apply-ref-proof: Internal functions
Function, args: Internal functions
Function, bsym-reader: Internal functions
Function, cartesian-product: Internal functions
Function, collect-stats: Exported functions
Function, collect-stats-thr: Internal functions
Function, collect-vars: Internal functions
Function, compose-proof: Internal functions
Function, compose-ref: Internal functions
Function, context-assert: Exported functions
Function, context-class: Exported functions
Function, context-distinct: Exported functions
Function, context-exports: Exported functions
Function, context-hypo: Exported functions
Function, context-imports: Exported functions
Function, context-meta: Exported functions
Function, context-name: Exported functions
Function, context-p: Internal functions
Function, context-printer: Internal functions
Function, context-proof: Exported functions
Function, context-syms: Exported functions
Function, context-type: Exported functions
Function, context-vars: Exported functions
Function, copy-context: Internal functions
Function, copy-items: Internal functions
Function, copy-pattern-tree: Internal functions
Function, copy-subproof: Internal functions
Function, copy-symkind: Internal functions
Function, copy-symref: Internal functions
Function, create-context: Exported functions
Function, dvc: Internal functions
Function, dvc-1: Internal functions
Function, dvc-list: Exported functions
Function, dvc-satisfied: Internal functions
Function, dvc-var: Exported functions
Function, export: Exported functions
Function, flatten: Exported functions
Function, flatten-1: Internal functions
Function, flush: Exported functions
Function, get-symkind: Internal functions
Function, highest-number-in: Internal functions
Function, import: Exported functions
Function, in-tree: Exported functions
Function, insert-export: Exported functions
Function, insert-import: Exported functions
Function, insert-pat: Exported functions
Function, insert-sym: Exported functions
Function, insert-wff: Exported functions
Function, int-list: Internal functions
Function, lib-path-name: Internal functions
Function, load-aux: Exported functions
Function, make-context: Exported functions
Function, make-pattern-tree: Exported functions
Function, make-subproof: Exported functions
Function, make-symkind: Internal functions
Function, make-symref: Exported functions
Function, makevarlist: Exported functions
Function, makevarlist-r: Internal functions
Function, match-tree: Exported functions
Function, matcher-fn: Internal functions
Function, mkcontext: Exported functions
Function, mklist: Exported functions
Function, mkrootctx: Internal functions
Function, mkvar: Exported functions
Function, op: Internal functions
Function, pair-eq: Internal functions
Function, parse-subproof: Exported functions
Function, parse-thr-ref: Internal functions
Function, parse-varspec: Internal functions
Function, pat-var-p: Internal functions
Function, pat-vars-in: Internal functions
Function, pattern-to-ref: Internal functions
Function, pattern-tree-p: Internal functions
Function, pattern-tree-ref: Exported functions
Function, pattern-tree-syms: Exported functions
Function, permute-ref: Internal functions
Function, permute-vars: Internal functions
Function, potential-vars: Internal functions
Function, print-symtree: Exported functions
Function, print-symtree-aux: Internal functions
Function, print-symtree-debug: Internal functions
Function, print-theorem: Exported functions
Function, provenp: Exported functions
Function, push-second: Internal functions
Function, r-int-list: Internal functions
Function, read-names: Internal functions
Function, read-segment: Internal functions
Function, ref-to-pattern: Internal functions
Function, replace-proof-vars: Internal functions
Function, replace-vars: Exported functions
Function, require: Exported functions
Function, seek-create-ctx: Exported functions
Function, seek-ctx-exports: Internal functions
Function, seek-ctx-imports: Internal functions
Function, seek-sym: Exported functions
Function, show-proof: Exported functions
Function, show-stats: Exported functions
Function, show-unused: Exported functions
Function, simple-splice: Internal functions
Function, smap: Exported functions
Function, splice: Internal functions
Function, subkindp: Exported functions
Function, subproof-assert: Exported functions
Function, subproof-hypo: Exported functions
Function, subproof-p: Internal functions
Function, subproof-prev: Exported functions
Function, subproof-ref: Exported functions
Function, subproof-sub: Exported functions
Function, symkind-eq-op: Internal functions
Function, symkind-meta: Internal functions
Function, symkind-name: Internal functions
Function, symkind-p: Internal functions
Function, symkind-super: Internal functions
Function, symref-args-needed: Exported functions
Function, symref-class: Internal functions
Function, symref-fn: Exported functions
Function, symref-p: Internal functions
Function, symref-printer: Internal functions
Function, symref-proof: Exported functions
Function, symref-target: Exported functions
Function, symstr-reader: Internal functions
Function, symstr-reader-aux: Internal functions
Function, symtree-parse: Exported functions
Function, symtree-parse-aux: Internal functions
Function, symtree-reparse: Internal functions
Function, symtree-reparse-aux: Internal functions
Function, theorem-sym-p: Internal functions
Function, thref-reader: Internal functions
Function, verify: Exported functions
Function, verify-1: Internal functions
Function, verify-def: Internal functions
Function, verify-subproof: Internal functions
Function, walk-proof-tree: Internal functions
Function, wff-equal: Exported functions
Function, wff-type: Exported functions
Function, wffp: Exported functions
Function, wrap-ctx: Exported functions

G
get-symkind: Internal functions

H
highest-number-in: Internal functions
hypo: Exported macros

I
if-match: Exported macros
import: Exported functions
in-context: Exported macros
in-tree: Exported functions
insert-export: Exported functions
insert-import: Exported functions
insert-pat: Exported functions
insert-sym: Exported functions
insert-wff: Exported functions
int-list: Internal functions

L
let-once: Exported macros
lib-path-name: Internal functions
linear-subproof: Exported macros
load-aux: Exported functions
loc: Exported macros
local: Exported macros

M
Macro, acond: Exported macros
Macro, aif: Exported macros
Macro, alias: Exported macros
Macro, ass: Exported macros
Macro, ax: Exported macros
Macro, collecting: Exported macros
Macro, copy-th: Exported macros
Macro, def: Exported macros
Macro, defcontext: Exported macros
Macro, dist: Exported macros
Macro, do-proof: Internal macros
Macro, extend-metath: Exported macros
Macro, hypo: Exported macros
Macro, if-match: Exported macros
Macro, in-context: Exported macros
Macro, let-once: Exported macros
Macro, linear-subproof: Exported macros
Macro, loc: Exported macros
Macro, local: Exported macros
Macro, match-case: Exported macros
Macro, meta: Exported macros
Macro, metath: Exported macros
Macro, module: Exported macros
Macro, parse-vars: Exported macros
Macro, pattern: Exported macros
Macro, prim: Exported macros
Macro, proof: Exported macros
Macro, providing: Exported macros
Macro, set-symkind-eq-op: Exported macros
Macro, subproof: Exported macros
Macro, symkind: Exported macros
Macro, th: Exported macros
Macro, th-pattern: Exported macros
Macro, theory: Exported macros
Macro, var: Exported macros
Macro, var2: Exported macros
Macro, virtual-metath: Exported macros
Macro, with-gensyms: Exported macros
make-context: Exported functions
make-pattern-tree: Exported functions
make-subproof: Exported functions
make-symkind: Internal functions
make-symref: Exported functions
makevarlist: Exported functions
makevarlist-r: Internal functions
match-case: Exported macros
match-tree: Exported functions
matcher-fn: Internal functions
meta: Exported macros
metath: Exported macros
mkcontext: Exported functions
mklist: Exported functions
mkrootctx: Internal functions
mkvar: Exported functions
module: Exported macros

O
op: Internal functions

P
pair-eq: Internal functions
parse-subproof: Exported functions
parse-thr-ref: Internal functions
parse-vars: Exported macros
parse-varspec: Internal functions
pat-var-p: Internal functions
pat-vars-in: Internal functions
pattern: Exported macros
pattern-to-ref: Internal functions
pattern-tree-p: Internal functions
pattern-tree-ref: Exported functions
pattern-tree-syms: Exported functions
permute-ref: Internal functions
permute-vars: Internal functions
potential-vars: Internal functions
prim: Exported macros
print-symtree: Exported functions
print-symtree-aux: Internal functions
print-symtree-debug: Internal functions
print-theorem: Exported functions
proof: Exported macros
provenp: Exported functions
providing: Exported macros
push-second: Internal functions

R
r-int-list: Internal functions
read-names: Internal functions
read-segment: Internal functions
ref-to-pattern: Internal functions
replace-proof-vars: Internal functions
replace-vars: Exported functions
require: Exported functions

S
seek-create-ctx: Exported functions
seek-ctx-exports: Internal functions
seek-ctx-imports: Internal functions
seek-sym: Exported functions
set-symkind-eq-op: Exported macros
show-proof: Exported functions
show-stats: Exported functions
show-unused: Exported functions
simple-splice: Internal functions
smap: Exported functions
splice: Internal functions
subkindp: Exported functions
subproof: Exported macros
subproof-assert: Exported functions
subproof-hypo: Exported functions
subproof-p: Internal functions
subproof-prev: Exported functions
subproof-ref: Exported functions
subproof-sub: Exported functions
symkind: Exported macros
symkind-eq-op: Internal functions
symkind-meta: Internal functions
symkind-name: Internal functions
symkind-p: Internal functions
symkind-super: Internal functions
symref-args-needed: Exported functions
symref-class: Internal functions
symref-fn: Exported functions
symref-p: Internal functions
symref-printer: Internal functions
symref-proof: Exported functions
symref-target: Exported functions
symstr-reader: Internal functions
symstr-reader-aux: Internal functions
symtree-parse: Exported functions
symtree-parse-aux: Internal functions
symtree-reparse: Internal functions
symtree-reparse-aux: Internal functions

T
th: Exported macros
th-pattern: Exported macros
theorem-sym-p: Internal functions
theory: Exported macros
thref-reader: Internal functions

V
var: Exported macros
var2: Exported macros
verify: Exported functions
verify-1: Internal functions
verify-def: Internal functions
verify-subproof: Internal functions
virtual-metath: Exported macros

W
walk-proof-tree: Internal functions
wff-equal: Exported functions
wff-type: Exported functions
wffp: Exported functions
with-gensyms: Exported macros
wrap-ctx: Exported functions

Jump to:   (  
A   B   C   D   E   F   G   H   I   L   M   O   P   R   S   T   V   W  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.3 Variables

Jump to:   *  
A   C   D   E   F   H   I   M   N   P   R   S   T   V  
Index Entry  Section

*
*bourbaki-debug*: Exported special variables
*bourbaki-library-path*: Exported special variables
*bourbaki-version*: Exported special variables
*current-context*: Exported special variables
*current-proof*: Exported special variables
*meta-context*: Exported special variables
*mkvar-counter*: Internal special variables
*root-context*: Exported special variables
*theorem-patterns*: Exported special variables

A
args-needed: Exported structures
assert: Exported structures
assert: Exported structures

C
class: Exported structures
class: Exported structures

D
distinct: Exported structures

E
eq-op: Exported structures
exports: Exported structures

F
fn: Exported structures

H
hypo: Exported structures
hypo: Exported structures

I
imports: Exported structures

M
meta: Exported structures
meta: Exported structures

N
name: Exported structures
name: Exported structures

P
prev: Exported structures
proof: Exported structures
proof: Exported structures

R
ref: Exported structures
ref: Exported structures

S
Slot, args-needed: Exported structures
Slot, assert: Exported structures
Slot, assert: Exported structures
Slot, class: Exported structures
Slot, class: Exported structures
Slot, distinct: Exported structures
Slot, eq-op: Exported structures
Slot, exports: Exported structures
Slot, fn: Exported structures
Slot, hypo: Exported structures
Slot, hypo: Exported structures
Slot, imports: Exported structures
Slot, meta: Exported structures
Slot, meta: Exported structures
Slot, name: Exported structures
Slot, name: Exported structures
Slot, prev: Exported structures
Slot, proof: Exported structures
Slot, proof: Exported structures
Slot, ref: Exported structures
Slot, ref: Exported structures
Slot, sub: Exported structures
Slot, super: Exported structures
Slot, syms: Exported structures
Slot, syms: Exported structures
Slot, target: Exported structures
Slot, type: Exported structures
Slot, vars: Exported structures
Special Variable, *bourbaki-debug*: Exported special variables
Special Variable, *bourbaki-library-path*: Exported special variables
Special Variable, *bourbaki-version*: Exported special variables
Special Variable, *current-context*: Exported special variables
Special Variable, *current-proof*: Exported special variables
Special Variable, *meta-context*: Exported special variables
Special Variable, *mkvar-counter*: Internal special variables
Special Variable, *root-context*: Exported special variables
Special Variable, *theorem-patterns*: Exported special variables
sub: Exported structures
super: Exported structures
syms: Exported structures
syms: Exported structures

T
target: Exported structures
type: Exported structures

V
vars: Exported structures

Jump to:   *  
A   C   D   E   F   H   I   M   N   P   R   S   T   V  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   B   C   P   S  
Index Entry  Section

B
bourbaki: The bourbaki system
bourbaki: The bourbaki package
bourbaki-system: The bourbaki-system package
bourbaki-user: The bourbaki-user package

C
context: Exported structures

P
Package, bourbaki: The bourbaki package
Package, bourbaki-system: The bourbaki-system package
Package, bourbaki-user: The bourbaki-user package
pattern-tree: Exported structures

S
Structure, context: Exported structures
Structure, pattern-tree: Exported structures
Structure, subproof: Exported structures
Structure, symkind: Exported structures
Structure, symref: Exported structures
subproof: Exported structures
symkind: Exported structures
symref: Exported structures
System, bourbaki: The bourbaki system

Jump to:   B   C   P   S