Common Lisp Package: BOURBAKI

README:

FUNCTION

Public

CONTEXT-ASSERT (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-CLASS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-DISTINCT (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-EXPORTS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-HYPO (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-IMPORTS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-META (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-NAME (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-PROOF (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-SYMS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-TYPE (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CONTEXT-VARS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

CREATE-CONTEXT (&KEY (NAME ) TYPE (PARENT *CURRENT-CONTEXT*) CLASS)

Create a subcontext of `parent' with specified type

MKVAR (TYPE CLASS &KEY (NAME (FORMAT NIL V~A (INCF *MKVAR-COUNTER*))) (BOUND NIL))

Create a symbol of specified type

PATTERN-TREE-REF (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

PATTERN-TREE-SYMS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

REPLACE-VARS (STR SMAP)

Substitute some variables in a wff

SEEK-SYM (MODE NAME1 &REST NAMES)

Seeks for a theorem or context or symbol.

SUBPROOF-ASSERT (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SUBPROOF-HYPO (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SUBPROOF-PREV (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SUBPROOF-REF (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SUBPROOF-SUB (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMREF-ARGS-NEEDED (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMREF-FN (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMREF-PROOF (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMREF-TARGET (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMTREE-PARSE (STR)

Parse an expression returned by symstr-reader

WFF-EQUAL (LHS RHS)

Check if two symtrees are equal

WFF-TYPE (STR)

Type of a symtree

WFFP (STR)

Check if str is a well-formed symtree

Undocumented

COLLECT-STATS (REF)

SETFCONTEXT-ASSERT (NEW-VALUE INSTANCE)

SETFCONTEXT-CLASS (NEW-VALUE INSTANCE)

SETFCONTEXT-DISTINCT (NEW-VALUE INSTANCE)

SETFCONTEXT-EXPORTS (NEW-VALUE INSTANCE)

SETFCONTEXT-HYPO (NEW-VALUE INSTANCE)

SETFCONTEXT-IMPORTS (NEW-VALUE INSTANCE)

SETFCONTEXT-META (NEW-VALUE INSTANCE)

SETFCONTEXT-NAME (NEW-VALUE INSTANCE)

SETFCONTEXT-PROOF (NEW-VALUE INSTANCE)

SETFCONTEXT-SYMS (NEW-VALUE INSTANCE)

SETFCONTEXT-TYPE (NEW-VALUE INSTANCE)

SETFCONTEXT-VARS (NEW-VALUE INSTANCE)

DVC-LIST (LST THR)

DVC-VAR (VAR THR)

EXPORT (STR &KEY PROOF)

FLATTEN (LST)

FLUSH

IMPORT (STR &KEY PROOF)

IN-TREE (TREE WFF)

INSERT-EXPORT (TARGET &KEY (WHERE *CURRENT-CONTEXT*) PROOF)

INSERT-IMPORT (TARGET &KEY (WHERE *CURRENT-CONTEXT*) PROOF)

INSERT-PAT (TREE REF)

INSERT-SYM (REF &OPTIONAL (CONTEXT *CURRENT-CONTEXT*) (NAME (CONTEXT-NAME (SYMREF-TARGET REF))))

INSERT-WFF (TREE WFF &OPTIONAL (VAL T))

LOAD-AUX (FILENAME &OPTIONAL TYPE)

MAKE-CONTEXT (&KEY ((SYMS DUM44) (MAKE-HASH-TABLE TEST 'EQUAL)) ((IMPORTS DUM45) NIL) ((EXPORTS DUM46) NIL) ((TYPE DUM47) NIL) ((CLASS DUM48) NIL) ((META DUM49) (MAKE-HASH-TABLE TEST 'EQ)) ((NAME DUM50) NIL) ((VARS DUM51) NIL) ((DISTINCT DUM52) NIL) ((HYPO DUM53) NIL) ((ASSERT DUM54) NIL) ((PROOF DUM55) NIL))

MAKE-PATTERN-TREE (&KEY ((SYMS DUM252) (MAKE-HASH-TABLE TEST 'EQ)) ((REF DUM253) NIL))

MAKE-SUBPROOF (&KEY ((REF DUM208) NIL) ((HYPO DUM209) NIL) ((ASSERT DUM210) NIL) ((PREV DUM211) NIL) ((SUB DUM212) NIL))

MAKE-SYMREF (&KEY ((TARGET DUM135) NIL) ((ARGS-NEEDED DUM136) NIL) ((FN DUM137) NIL) ((CLASS DUM138) NIL) ((PROOF DUM139) NIL))

MAKEVARLIST (THR)

MATCH-TREE (TREE WFF)

MKCONTEXT (REF)

MKLIST (X)

PARSE-SUBPROOF (ITEM)

SETFPATTERN-TREE-REF (NEW-VALUE INSTANCE)

SETFPATTERN-TREE-SYMS (NEW-VALUE INSTANCE)

PROVENP (WFF)

REQUIRE (NAME MODULE &KEY PROVIDE)

SEEK-CREATE-CTX (NAME &OPTIONAL (CLASS CONTEXT) (CONTEXT *CURRENT-CONTEXT*))

SHOW-PROOF (REF &OPTIONAL (MODE NIL))

SHOW-STATS (REF)

SHOW-UNUSED (REF)

SMAP (THR EXPR)

SUBKINDP (TYPE1 TYPE2)

SETFSUBPROOF-ASSERT (NEW-VALUE INSTANCE)

SETFSUBPROOF-HYPO (NEW-VALUE INSTANCE)

SETFSUBPROOF-PREV (NEW-VALUE INSTANCE)

SETFSUBPROOF-REF (NEW-VALUE INSTANCE)

SETFSUBPROOF-SUB (NEW-VALUE INSTANCE)

SETFSYMREF-ARGS-NEEDED (NEW-VALUE INSTANCE)

SETFSYMREF-FN (NEW-VALUE INSTANCE)

SETFSYMREF-PROOF (NEW-VALUE INSTANCE)

SETFSYMREF-TARGET (NEW-VALUE INSTANCE)

VERIFY (REF &OPTIONAL (NESTED T))

WRAP-CTX (CTX &OPTIONAL (NVARS (LENGTH (CONTEXT-VARS CTX))))

Private

CARTESIAN-PRODUCT (VARS1 VARS2)

Cartesian product of two lists

COLLECT-VARS (STR VARLIST)

The list of symbols from varlist that occur in str

COMPOSE-REF (LHS RHS)

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

DVC-SATISFIED (THREF SMAP CONDLIST VARLIST)

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

PAIR-EQ (LHS RHS)

Equality of unordered pairs

POTENTIAL-VARS (LST DIST EXPR)

List of variables that potentially occur in a symtree

REPLACE-PROOF-VARS (PF SMAP)

Substitute some variables in a proof

SEEK-CTX-IMPORTS (NAME &OPTIONAL (CONTEXT *CURRENT-CONTEXT*))

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

SYMKIND-EQ-OP (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMKIND-META (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMKIND-NAME (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMKIND-SUPER (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMREF-CLASS (INSTANCE)

@arg[extid]{A @class{extid}} @return[sytemid]{puri:uri or nil} Returns the System ID part of this External ID.

SYMTREE-PARSE-AUX

Helper function for symtree-parse

SYMTREE-REPARSE (STR)

Helper function for replace-vars

SYMTREE-REPARSE-AUX (STR)

Helper function for replace-vars

VERIFY-1 (THR)

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

VERIFY-DEF (DEFN)

Verify soundness of a definition

Undocumented

APPLY-REF (REF ARGS)

APPLY-REF-PROOF (REF ARGS)

ARGS (X)

BSYM-READER (STREAM ALT)

COLLECT-STATS-THR (THR)

COMPOSE-PROOF (LHS RHS)

CONTEXT-P (OBJECT)

CONTEXT-PRINTER (OBJ STREAM)

COPY-CONTEXT (INSTANCE)

COPY-ITEMS (LST FROM)

COPY-PATTERN-TREE (INSTANCE)

COPY-SUBPROOF (INSTANCE)

COPY-SYMKIND (INSTANCE)

COPY-SYMREF (INSTANCE)

DVC (LIST1 LIST2 THR)

DVC-1 (CND THR)

FLATTEN-1 (WFF)

GET-SYMKIND (SYM)

HIGHEST-NUMBER-IN (TREE)

INT-LIST (N)

LIB-PATH-NAME (FILENAME &OPTIONAL TYPE)

MAKE-SYMKIND (&KEY ((NAME DUM0) ) ((EQ-OP DUM1) NIL) ((META DUM2) (MAKE-HASH-TABLE TEST 'EQ)) ((SUPER DUM3) NIL))

MAKEVARLIST-R (THR)

MATCHER-FN (PAT)

MKROOTCTX

OP (X)

PARSE-THR-REF (TREE &OPTIONAL REF ARGS)

PARSE-VARSPEC (TYPE NAMES CLASS)

PAT-VAR-P (EXPR)

PAT-VARS-IN (EXPR)

PATTERN-TO-REF (PAT &OPTIONAL CLASS)

PATTERN-TREE-P (OBJECT)

PERMUTE-REF (REF SMAP)

PERMUTE-VARS (PAT REF)

PUSH-SECOND (X LST)

R-INT-LIST (N)

READ-NAMES (STREAM)

READ-SEGMENT (STREAM)

REF-TO-PATTERN (REF)

SEEK-CTX-EXPORTS (NAME REF)

SIMPLE-SPLICE (LST LEN FN)

SPLICE (LST LEN FN)

SUBPROOF-P (OBJECT)

SETFSYMKIND-EQ-OP (NEW-VALUE INSTANCE)

SETFSYMKIND-META (NEW-VALUE INSTANCE)

SETFSYMKIND-NAME (NEW-VALUE INSTANCE)

SYMKIND-P (OBJECT)

SETFSYMKIND-SUPER (NEW-VALUE INSTANCE)

SETFSYMREF-CLASS (NEW-VALUE INSTANCE)

SYMREF-P (OBJECT)

SYMREF-PRINTER (OBJ STREAM)

SYMSTR-READER (STREAM CHAR)

SYMSTR-READER-AUX (STREAM ALT)

THEOREM-SYM-P (SYM)

THREF-READER (STREAM CHAR)

VERIFY-SUBPROOF (PF VARLIST DVC NUM)

WALK-PROOF-TREE (THR FN &OPTIONAL (NESTED NIL))

MACRO

Public

ASS (&REST LST)

Axiom or theorem assertion

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.

DIST (&REST LST)

Distinct variable conditions

HYPO (&REST LST)

Axiom or theorem hypotheses

IN-CONTEXT (REF &BODY BODY)

Enter an existing context

LOCAL (NAME &BODY BODY)

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

MODULE (NAME &BODY BODY)

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

PRIM (TYPE NAME VARS &BODY BODY)

A primitive symbol

Undocumented

ACOND (&BODY CONDS)

AIF (TEST THEN &OPTIONAL ELSE)

ALIAS (ALIAS-NAME VARS RHS)

AX (NAME VARS &BODY BODY)

COPY-TH (THR SUFFIX ITEMS &BODY BODY)

DEF (DF-NAME SYM-TYPE SYM-NAME VARS DUMMY RHS &BODY BODY)

DEFCONTEXT (CLASS NAME VARS &BODY BODY)

EXTEND-METATH (REF ARGS &BODY BODY)

IF-MATCH (PAT EXPR THEN &OPTIONAL ELSE)

LET-ONCE ((VAR EXPR) &BODY BODY)

LINEAR-SUBPROOF (HYP ASS &BODY LINES)

LOC (&REST VARSPEC)

MATCH-CASE (EXPR &BODY CASES)

META (&REST SPECS)

METATH (NAME ARGS &BODY BODY)

PARSE-VARS (VARLIST &OPTIONAL (CLASS ARG))

PATTERN (VARS RHS)

PROOF (&BODY LINES)

PROVIDING (CTX &BODY BODY)

SET-SYMKIND-EQ-OP (KIND OP)

SUBPROOF ((&KEY HYPO ASSERT) &BODY BODY)

SYMKIND (NAME &KEY (SUPER NIL SUPER-PROVIDED-P))

TH (NAME VARS &BODY BODY)

TH-PATTERN (REF)

THEORY (NAME VARS &BODY BODY)

VAR (TYPE CLASS)

VAR2 (TYPE NAME CLASS)

VIRTUAL-METATH (NAME ARGS &BODY BODY)

WITH-GENSYMS (SYMS &BODY BODY)

Private

Undocumented

DO-PROOF ((VAR PF) &BODY BODY)

VARIABLE

Public

Undocumented

*BOURBAKI-DEBUG*

*BOURBAKI-LIBRARY-PATH*

*BOURBAKI-VERSION*

*CURRENT-CONTEXT*

*CURRENT-PROOF*

*META-CONTEXT*

*ROOT-CONTEXT*

*THEOREM-PATTERNS*

Private

Undocumented

*MKVAR-COUNTER*

CLASS

Public

CONTEXT

Symbol, theorem or context

SYMKIND (NAME &KEY (SUPER NIL SUPER-PROVIDED-P))

A symbol type

SYMREF

Reference to a symbol or context

Undocumented

PATTERN-TREE

SUBPROOF ((&KEY HYPO ASSERT) &BODY BODY)