This is the bourbaki Reference Manual, version 3.5, generated automatically by Declt version 4.0 beta 2 "William Riker" on Sun Dec 15 04:27:33 2024 GMT+0.
bourbaki/bourbaki.asdbourbaki/bourbaki/package.lispbourbaki/bourbaki/types.lispbourbaki/bourbaki/variables.lispbourbaki/bourbaki/symbol.lispbourbaki/bourbaki/util.lispbourbaki/bourbaki/symref.lispbourbaki/bourbaki/pattern.lispbourbaki/bourbaki/proof.lispbourbaki/bourbaki/print.lispbourbaki/bourbaki/distinct.lispbourbaki/bourbaki/symtree.lispbourbaki/bourbaki/context.lispbourbaki/bourbaki/verify.lispbourbaki/bourbaki/stats.lispbourbaki/bourbaki/parse.lispbourbaki/bourbaki/define.lispbourbaki/bourbaki/read.lispbourbaki/bourbaki/metatheorem.lispbourbaki/bourbaki/parse-proof.lispThe main system appears first, followed by any subsystem dependency.
Modules are listed depth-first from the system components tree.
bourbaki/bourbakibourbaki (system).
package.lisp (file).
types.lisp (file).
variables.lisp (file).
symbol.lisp (file).
util.lisp (file).
symref.lisp (file).
pattern.lisp (file).
proof.lisp (file).
print.lisp (file).
distinct.lisp (file).
symtree.lisp (file).
context.lisp (file).
verify.lisp (file).
stats.lisp (file).
parse.lisp (file).
define.lisp (file).
read.lisp (file).
metatheorem.lisp (file).
parse-proof.lisp (file).
Files are sorted by type and then listed depth-first from the systems components trees.
bourbaki/bourbaki.asdbourbaki/bourbaki/package.lispbourbaki/bourbaki/types.lispbourbaki/bourbaki/variables.lispbourbaki/bourbaki/symbol.lispbourbaki/bourbaki/util.lispbourbaki/bourbaki/symref.lispbourbaki/bourbaki/pattern.lispbourbaki/bourbaki/proof.lispbourbaki/bourbaki/print.lispbourbaki/bourbaki/distinct.lispbourbaki/bourbaki/symtree.lispbourbaki/bourbaki/context.lispbourbaki/bourbaki/verify.lispbourbaki/bourbaki/stats.lispbourbaki/bourbaki/parse.lispbourbaki/bourbaki/define.lispbourbaki/bourbaki/read.lispbourbaki/bourbaki/metatheorem.lispbourbaki/bourbaki/parse-proof.lispbourbaki/bourbaki/types.lisppackage.lisp (file).
bourbaki (module).
context (structure).
context-assert (reader).
(setf context-assert) (writer).
context-class (reader).
(setf context-class) (writer).
context-distinct (reader).
(setf context-distinct) (writer).
context-exports (reader).
(setf context-exports) (writer).
context-hypo (reader).
(setf context-hypo) (writer).
context-imports (reader).
(setf context-imports) (writer).
context-meta (reader).
(setf context-meta) (writer).
context-name (reader).
(setf context-name) (writer).
context-proof (reader).
(setf context-proof) (writer).
context-syms (reader).
(setf context-syms) (writer).
context-type (reader).
(setf context-type) (writer).
context-vars (reader).
(setf context-vars) (writer).
make-context (function).
make-pattern-tree (function).
make-subproof (function).
make-symref (function).
pattern-tree (structure).
pattern-tree-ref (reader).
(setf pattern-tree-ref) (writer).
pattern-tree-syms (reader).
(setf pattern-tree-syms) (writer).
print-object (method).
print-object (method).
subproof (structure).
subproof-assert (reader).
(setf subproof-assert) (writer).
subproof-hypo (reader).
(setf subproof-hypo) (writer).
subproof-prev (reader).
(setf subproof-prev) (writer).
subproof-ref (reader).
(setf subproof-ref) (writer).
subproof-sub (reader).
(setf subproof-sub) (writer).
symkind (structure).
symref (structure).
symref-args-needed (reader).
(setf symref-args-needed) (writer).
symref-fn (reader).
(setf symref-fn) (writer).
symref-proof (reader).
(setf symref-proof) (writer).
symref-target (reader).
(setf symref-target) (writer).
context-p (function).
context-printer (function).
copy-context (function).
copy-pattern-tree (function).
copy-subproof (function).
copy-symkind (function).
copy-symref (function).
make-symkind (function).
pattern-tree-p (function).
subproof-p (function).
symkind-eq-op (reader).
(setf symkind-eq-op) (writer).
symkind-meta (reader).
(setf symkind-meta) (writer).
symkind-name (reader).
(setf symkind-name) (writer).
symkind-p (function).
symkind-super (reader).
(setf symkind-super) (writer).
symref-class (reader).
(setf symref-class) (writer).
symref-p (function).
symref-printer (function).
bourbaki/bourbaki/variables.lisptypes.lisp (file).
bourbaki (module).
*bourbaki-debug* (special variable).
*bourbaki-library-path* (special variable).
*bourbaki-version* (special variable).
*current-context* (special variable).
*current-proof* (special variable).
*meta-context* (special variable).
*root-context* (special variable).
*theorem-patterns* (special variable).
mkrootctx (function).
bourbaki/bourbaki/symbol.lisptypes.lisp (file).
bourbaki (module).
*mkvar-counter* (special variable).
theorem-sym-p (function).
bourbaki/bourbaki/util.lispvariables.lisp (file).
bourbaki (module).
acond (macro).
aif (macro).
collecting (macro).
flatten (function).
load-aux (function).
mklist (function).
with-gensyms (macro).
args (function).
cartesian-product (function).
flatten-1 (function).
highest-number-in (function).
int-list (function).
lib-path-name (function).
op (function).
pair-eq (function).
push-second (function).
r-int-list (function).
simple-splice (function).
splice (function).
bourbaki/bourbaki/symref.lisptypes.lisp (file).
util.lisp (file).
bourbaki (module).
apply-ref (function).
apply-ref-proof (function).
compose-proof (function).
compose-ref (function).
pattern-to-ref (function).
ref-to-pattern (function).
bourbaki/bourbaki/pattern.lisputil.lisp (file).
symtree.lisp (file).
symref.lisp (file).
bourbaki (module).
if-match (macro).
in-tree (function).
insert-pat (function).
insert-wff (function).
let-once (macro).
match-case (macro).
match-tree (function).
matcher-fn (function).
pat-var-p (function).
pat-vars-in (function).
permute-ref (function).
permute-vars (function).
bourbaki/bourbaki/proof.lisppattern.lisp (file).
bourbaki (module).
provenp (function).
do-proof (macro).
walk-proof-tree (function).
bourbaki/bourbaki/print.lisptypes.lisp (file).
util.lisp (file).
variables.lisp (file).
proof.lisp (file).
bourbaki (module).
print-symtree (function).
print-theorem (function).
show-proof (function).
print-symtree-aux (function).
print-symtree-debug (function).
bourbaki/bourbaki/distinct.lisptypes.lisp (file).
util.lisp (file).
bourbaki (module).
dvc (function).
dvc-1 (function).
dvc-satisfied (function).
bourbaki/bourbaki/symtree.lispsymbol.lisp (file).
util.lisp (file).
bourbaki (module).
makevarlist (function).
replace-vars (function).
smap (function).
wff-equal (function).
wff-type (function).
wffp (function).
collect-vars (function).
makevarlist-r (function).
potential-vars (function).
replace-proof-vars (function).
symtree-reparse (function).
symtree-reparse-aux (function).
bourbaki/bourbaki/context.lisptypes.lisp (file).
variables.lisp (file).
util.lisp (file).
symtree.lisp (file).
print.lisp (file).
symref.lisp (file).
bourbaki (module).
create-context (function).
flush (function).
insert-export (function).
insert-import (function).
insert-sym (function).
mkcontext (function).
require (function).
seek-create-ctx (function).
seek-sym (function).
symtree-parse (function).
wrap-ctx (function).
parse-thr-ref (function).
seek-ctx-exports (function).
seek-ctx-imports (function).
symtree-parse-aux (function).
bourbaki/bourbaki/verify.lispsymtree.lisp (file).
util.lisp (file).
print.lisp (file).
context.lisp (file).
proof.lisp (file).
distinct.lisp (file).
bourbaki (module).
verify (function).
verify-1 (function).
verify-def (function).
verify-subproof (function).
bourbaki/bourbaki/stats.lispverify.lisp (file).
bourbaki (module).
collect-stats (function).
show-stats (function).
show-unused (function).
collect-stats-thr (function).
bourbaki/bourbaki/parse.lispcontext.lisp (file).
symtree.lisp (file).
util.lisp (file).
distinct.lisp (file).
bourbaki (module).
ass (macro).
ax (macro).
copy-th (macro).
defcontext (macro).
dist (macro).
export (function).
hypo (macro).
import (function).
in-context (macro).
loc (macro).
local (macro).
meta (macro).
module (macro).
parse-vars (macro).
prim (macro).
providing (macro).
set-symkind-eq-op (macro).
symkind (macro).
th (macro).
th-pattern (macro).
theory (macro).
var (macro).
var2 (macro).
copy-items (function).
get-symkind (function).
parse-varspec (function).
bourbaki/bourbaki/define.lispparse.lisp (file).
bourbaki (module).
bourbaki/bourbaki/read.lisppackage.lisp (file).
bourbaki (module).
bsym-reader (function).
read-names (function).
read-segment (function).
symstr-reader (function).
symstr-reader-aux (function).
thref-reader (function).
bourbaki/bourbaki/metatheorem.lispcontext.lisp (file).
bourbaki (module).
extend-metath (macro).
metath (macro).
virtual-metath (macro).
bourbaki/bourbaki/parse-proof.lisppattern.lisp (file).
verify.lisp (file).
bourbaki (module).
linear-subproof (macro).
parse-subproof (function).
proof (macro).
subproof (macro).
Packages are listed by definition order.
bourbakicommon-lisp.
*bourbaki-debug* (special variable).
*bourbaki-library-path* (special variable).
*bourbaki-version* (special variable).
*current-context* (special variable).
*current-proof* (special variable).
*meta-context* (special variable).
*root-context* (special variable).
*theorem-patterns* (special variable).
acond (macro).
aif (macro).
alias (macro).
ass (macro).
ax (macro).
collect-stats (function).
collecting (macro).
context (structure).
context-assert (reader).
(setf context-assert) (writer).
context-class (reader).
(setf context-class) (writer).
context-distinct (reader).
(setf context-distinct) (writer).
context-exports (reader).
(setf context-exports) (writer).
context-hypo (reader).
(setf context-hypo) (writer).
context-imports (reader).
(setf context-imports) (writer).
context-meta (reader).
(setf context-meta) (writer).
context-name (reader).
(setf context-name) (writer).
context-proof (reader).
(setf context-proof) (writer).
context-syms (reader).
(setf context-syms) (writer).
context-type (reader).
(setf context-type) (writer).
context-vars (reader).
(setf context-vars) (writer).
copy-th (macro).
create-context (function).
def (macro).
defcontext (macro).
dist (macro).
dvc-list (function).
dvc-var (function).
export (function).
extend-metath (macro).
flatten (function).
flush (function).
hypo (macro).
if-match (macro).
import (function).
in-context (macro).
in-tree (function).
insert-export (function).
insert-import (function).
insert-pat (function).
insert-sym (function).
insert-wff (function).
let-once (macro).
linear-subproof (macro).
load-aux (function).
loc (macro).
local (macro).
make-context (function).
make-pattern-tree (function).
make-subproof (function).
make-symref (function).
makevarlist (function).
match-case (macro).
match-tree (function).
meta (macro).
metath (macro).
mkcontext (function).
mklist (function).
mkvar (function).
module (macro).
parse-subproof (function).
parse-vars (macro).
pattern (macro).
pattern-tree (structure).
pattern-tree-ref (reader).
(setf pattern-tree-ref) (writer).
pattern-tree-syms (reader).
(setf pattern-tree-syms) (writer).
prim (macro).
print-symtree (function).
print-theorem (function).
proof (macro).
provenp (function).
providing (macro).
replace-vars (function).
require (function).
seek-create-ctx (function).
seek-sym (function).
set-symkind-eq-op (macro).
show-proof (function).
show-stats (function).
show-unused (function).
smap (function).
subkindp (function).
subproof (macro).
subproof (structure).
subproof-assert (reader).
(setf subproof-assert) (writer).
subproof-hypo (reader).
(setf subproof-hypo) (writer).
subproof-prev (reader).
(setf subproof-prev) (writer).
subproof-ref (reader).
(setf subproof-ref) (writer).
subproof-sub (reader).
(setf subproof-sub) (writer).
symkind (macro).
symkind (structure).
symref (structure).
symref-args-needed (reader).
(setf symref-args-needed) (writer).
symref-fn (reader).
(setf symref-fn) (writer).
symref-proof (reader).
(setf symref-proof) (writer).
symref-target (reader).
(setf symref-target) (writer).
symtree-parse (function).
th (macro).
th-pattern (macro).
theory (macro).
var (macro).
var2 (macro).
verify (function).
virtual-metath (macro).
wff-equal (function).
wff-type (function).
wffp (function).
with-gensyms (macro).
wrap-ctx (function).
*mkvar-counter* (special variable).
apply-ref (function).
apply-ref-proof (function).
args (function).
bsym-reader (function).
cartesian-product (function).
collect-stats-thr (function).
collect-vars (function).
compose-proof (function).
compose-ref (function).
context-p (function).
context-printer (function).
copy-context (function).
copy-items (function).
copy-pattern-tree (function).
copy-subproof (function).
copy-symkind (function).
copy-symref (function).
do-proof (macro).
dvc (function).
dvc-1 (function).
dvc-satisfied (function).
flatten-1 (function).
get-symkind (function).
highest-number-in (function).
int-list (function).
lib-path-name (function).
make-symkind (function).
makevarlist-r (function).
matcher-fn (function).
mkrootctx (function).
op (function).
pair-eq (function).
parse-thr-ref (function).
parse-varspec (function).
pat-var-p (function).
pat-vars-in (function).
pattern-to-ref (function).
pattern-tree-p (function).
permute-ref (function).
permute-vars (function).
potential-vars (function).
print-symtree-aux (function).
print-symtree-debug (function).
push-second (function).
r-int-list (function).
read-names (function).
read-segment (function).
ref-to-pattern (function).
replace-proof-vars (function).
seek-ctx-exports (function).
seek-ctx-imports (function).
simple-splice (function).
splice (function).
subproof-p (function).
symkind-eq-op (reader).
(setf symkind-eq-op) (writer).
symkind-meta (reader).
(setf symkind-meta) (writer).
symkind-name (reader).
(setf symkind-name) (writer).
symkind-p (function).
symkind-super (reader).
(setf symkind-super) (writer).
symref-class (reader).
(setf symref-class) (writer).
symref-p (function).
symref-printer (function).
symstr-reader (function).
symstr-reader-aux (function).
symtree-parse-aux (function).
symtree-reparse (function).
symtree-reparse-aux (function).
theorem-sym-p (function).
thref-reader (function).
verify-1 (function).
verify-def (function).
verify-subproof (function).
walk-proof-tree (function).
Definitions are sorted by export status, category, package, and then by lexicographic order.
Axiom or theorem assertion
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.
Distinct variable conditions
Axiom or theorem hypotheses
Enter an existing context
Enter a subcontext, creating it if it did not already exist
Enter a top-level context, creating it if it did not already exist
A primitive symbol
hypo.
meta.
name.
syms.
type.
vars.
Create a subcontext of ‘parent’ with specified type
Create a symbol of specified type
ref.
syms.
Substitute some variables in a wff
Seeks for a theorem or context or symbol.
hypo.
prev.
ref.
sub.
Parse an expression returned by symstr-reader
Check if two symtrees are equal
Type of a symtree
Check if str is a well-formed symtree
Symbol, theorem or context
structure-object.
(make-hash-table :test (quote equal))
common-lisp.
common-lisp.
(make-hash-table :test (quote eq))
common-lisp.
A symbol type
Reference to a symbol or context
Cartesian product of two lists
The list of symbols from varlist that occur in str
Helper function for seek-sym.
Creates a composed symref from a context and a symref.
Check that distinct variable conditions are satisfied in a proof step.
List of variables that potentially occur in a symtree
Substitute some variables in a proof
Helper function for seek-sym.
Seeks for a theorem or symbol in imported contexts.
meta.
name.
Helper function for symtree-parse
Helper function for replace-vars
Helper function for replace-vars
Verify that the hypotheses and assertion of thr are wff and the proof is correct.
Verify soundness of a definition
| Jump to: | (
A B C D E F G H I L M O P R S T V W |
|---|
| Jump to: | (
A B C D E F G H I L M O P R S T V W |
|---|
| Jump to: | *
A C D E F H I M N P R S T V |
|---|
| Jump to: | *
A C D E F H I M N P R S T V |
|---|
| Jump to: | B C D F M P R S T U V |
|---|
| Jump to: | B C D F M P R S T U V |
|---|