The bourbaki Reference Manual

This is the bourbaki Reference Manual, version 3.5, generated automatically by Declt version 4.0 beta 2 "William Riker" on Wed May 15 03:30:25 2024 GMT+0.

Table of Contents


1 Systems

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


1.1 bourbaki

Version

3.5

Source

bourbaki.asd.

Child Component

bourbaki (module).


2 Modules

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


2.1 bourbaki/bourbaki

Source

bourbaki.asd.

Parent Component

bourbaki (system).

Child Components

3 Files

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


3.1 Lisp


3.1.1 bourbaki/bourbaki.asd

Source

bourbaki.asd.

Parent Component

bourbaki (system).

ASDF Systems

bourbaki.

Packages

bourbaki-system.


3.1.2 bourbaki/bourbaki/package.lisp

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Packages

3.1.3 bourbaki/bourbaki/types.lisp

Dependency

package.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.4 bourbaki/bourbaki/variables.lisp

Dependency

types.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

mkrootctx (function).


3.1.5 bourbaki/bourbaki/symbol.lisp

Dependency

types.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.6 bourbaki/bourbaki/util.lisp

Dependency

variables.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.7 bourbaki/bourbaki/symref.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Internals

3.1.8 bourbaki/bourbaki/pattern.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.9 bourbaki/bourbaki/proof.lisp

Dependency

pattern.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface

provenp (function).

Internals

3.1.10 bourbaki/bourbaki/print.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.11 bourbaki/bourbaki/distinct.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.12 bourbaki/bourbaki/symtree.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.13 bourbaki/bourbaki/context.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.14 bourbaki/bourbaki/verify.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface

verify (function).

Internals

3.1.15 bourbaki/bourbaki/stats.lisp

Dependency

verify.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

collect-stats-thr (function).


3.1.16 bourbaki/bourbaki/parse.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface
Internals

3.1.17 bourbaki/bourbaki/define.lisp

Dependency

parse.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface

3.1.18 bourbaki/bourbaki/read.lisp

Dependency

package.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Internals

3.1.19 bourbaki/bourbaki/metatheorem.lisp

Dependency

context.lisp (file).

Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface

3.1.20 bourbaki/bourbaki/parse-proof.lisp

Dependencies
Source

bourbaki.asd.

Parent Component

bourbaki (module).

Public Interface

4 Packages

Packages are listed by definition order.


4.1 bourbaki

Source

package.lisp.

Use List

common-lisp.

Used By List

bourbaki-user.

Public Interface
Internals

4.2 bourbaki-user

Source

package.lisp.

Use List

4.3 bourbaki-system

Source

bourbaki.asd.

Use List
  • asdf/interface.
  • common-lisp.

5 Definitions

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


5.1 Public Interface


5.1.1 Special variables

Special Variable: *bourbaki-debug*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *bourbaki-library-path*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *bourbaki-version*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *current-context*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *current-proof*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *meta-context*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *root-context*
Package

bourbaki.

Source

variables.lisp.

Special Variable: *theorem-patterns*
Package

bourbaki.

Source

variables.lisp.


5.1.2 Macros

Macro: acond (&body conds)
Package

bourbaki.

Source

util.lisp.

Macro: aif (test then &optional else)
Package

bourbaki.

Source

util.lisp.

Macro: alias (alias-name vars rhs)
Package

bourbaki.

Source

define.lisp.

Macro: ass (&rest lst)

Axiom or theorem assertion

Package

bourbaki.

Source

parse.lisp.

Macro: ax (name vars &body body)
Package

bourbaki.

Source

parse.lisp.

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.

Macro: copy-th (thr suffix items &body body)
Package

bourbaki.

Source

parse.lisp.

Macro: def (df-name sym-type sym-name vars dummy rhs &body body)
Package

bourbaki.

Source

define.lisp.

Macro: defcontext (class name vars &body body)
Package

bourbaki.

Source

parse.lisp.

Macro: dist (&rest lst)

Distinct variable conditions

Package

bourbaki.

Source

parse.lisp.

Macro: extend-metath (ref args &body body)
Package

bourbaki.

Source

metatheorem.lisp.

Macro: hypo (&rest lst)

Axiom or theorem hypotheses

Package

bourbaki.

Source

parse.lisp.

Macro: if-match (pat expr then &optional else)
Package

bourbaki.

Source

pattern.lisp.

Macro: in-context (ref &body body)

Enter an existing context

Package

bourbaki.

Source

parse.lisp.

Macro: let-once ((var expr) &body body)
Package

bourbaki.

Source

pattern.lisp.

Macro: linear-subproof (hyp ass &body lines)
Package

bourbaki.

Source

parse-proof.lisp.

Macro: loc (&rest varspec)
Package

bourbaki.

Source

parse.lisp.

Macro: local (name &body body)

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

Package

bourbaki.

Source

parse.lisp.

Macro: match-case (expr &body cases)
Package

bourbaki.

Source

pattern.lisp.

Macro: meta (&rest specs)
Package

bourbaki.

Source

parse.lisp.

Macro: metath (name args &body body)
Package

bourbaki.

Source

metatheorem.lisp.

Macro: module (name &body body)

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

Package

bourbaki.

Source

parse.lisp.

Macro: parse-vars (varlist &optional class)
Package

bourbaki.

Source

parse.lisp.

Macro: pattern (vars rhs)
Package

bourbaki.

Source

define.lisp.

Macro: prim (type name vars &body body)

A primitive symbol

Package

bourbaki.

Source

parse.lisp.

Macro: proof (&body lines)
Package

bourbaki.

Source

parse-proof.lisp.

Macro: providing (ctx &body body)
Package

bourbaki.

Source

parse.lisp.

Macro: set-symkind-eq-op (kind op)
Package

bourbaki.

Source

parse.lisp.

Macro: subproof ((&key hypo assert) &body body)
Package

bourbaki.

Source

parse-proof.lisp.

Macro: symkind (name &key super)
Package

bourbaki.

Source

parse.lisp.

Macro: th (name vars &body body)
Package

bourbaki.

Source

parse.lisp.

Macro: th-pattern (ref)
Package

bourbaki.

Source

parse.lisp.

Macro: theory (name vars &body body)
Package

bourbaki.

Source

parse.lisp.

Macro: var (type class)
Package

bourbaki.

Source

parse.lisp.

Macro: var2 (type name class)
Package

bourbaki.

Source

parse.lisp.

Macro: virtual-metath (name args &body body)
Package

bourbaki.

Source

metatheorem.lisp.

Macro: with-gensyms (syms &body body)
Package

bourbaki.

Source

util.lisp.


5.1.3 Ordinary functions

Function: collect-stats (ref)
Package

bourbaki.

Source

stats.lisp.

Reader: context-assert (instance)
Writer: (setf context-assert) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

assert.

Reader: context-class (instance)
Writer: (setf context-class) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

class.

Reader: context-distinct (instance)
Writer: (setf context-distinct) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

distinct.

Reader: context-exports (instance)
Writer: (setf context-exports) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

exports.

Reader: context-hypo (instance)
Writer: (setf context-hypo) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

hypo.

Reader: context-imports (instance)
Writer: (setf context-imports) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

imports.

Reader: context-meta (instance)
Writer: (setf context-meta) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

meta.

Reader: context-name (instance)
Writer: (setf context-name) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

name.

Reader: context-proof (instance)
Writer: (setf context-proof) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

proof.

Reader: context-syms (instance)
Writer: (setf context-syms) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

syms.

Reader: context-type (instance)
Writer: (setf context-type) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

type.

Reader: context-vars (instance)
Writer: (setf context-vars) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

vars.

Function: create-context (&key name type parent class)

Create a subcontext of ‘parent’ with specified type

Package

bourbaki.

Source

context.lisp.

Function: dvc-list (lst thr)
Package

bourbaki.

Source

distinct.lisp.

Function: dvc-var (var thr)
Package

bourbaki.

Source

distinct.lisp.

Function: export (str &key proof)
Package

bourbaki.

Source

parse.lisp.

Function: flatten (lst)
Package

bourbaki.

Source

util.lisp.

Function: flush ()
Package

bourbaki.

Source

context.lisp.

Function: import (str &key proof)
Package

bourbaki.

Source

parse.lisp.

Function: in-tree (tree wff)
Package

bourbaki.

Source

pattern.lisp.

Function: insert-export (target &key where proof)
Package

bourbaki.

Source

context.lisp.

Function: insert-import (target &key where proof)
Package

bourbaki.

Source

context.lisp.

Function: insert-pat (tree ref)
Package

bourbaki.

Source

pattern.lisp.

Function: insert-sym (ref &optional context name)
Package

bourbaki.

Source

context.lisp.

Function: insert-wff (tree wff &optional val)
Package

bourbaki.

Source

pattern.lisp.

Function: load-aux (filename &optional type)
Package

bourbaki.

Source

util.lisp.

Function: make-context (&key syms imports exports type class meta name vars distinct hypo assert proof)
Package

bourbaki.

Source

types.lisp.

Function: make-pattern-tree (&key syms ref)
Package

bourbaki.

Source

types.lisp.

Function: make-subproof (&key ref hypo assert prev sub)
Package

bourbaki.

Source

types.lisp.

Function: make-symref (&key target args-needed fn class proof)
Package

bourbaki.

Source

types.lisp.

Function: makevarlist (thr)
Package

bourbaki.

Source

symtree.lisp.

Function: match-tree (tree wff)
Package

bourbaki.

Source

pattern.lisp.

Function: mkcontext (ref)
Package

bourbaki.

Source

context.lisp.

Function: mklist (x)
Package

bourbaki.

Source

util.lisp.

Function: mkvar (type class &key name bound)

Create a symbol of specified type

Package

bourbaki.

Source

symbol.lisp.

Function: parse-subproof (item)
Package

bourbaki.

Source

parse-proof.lisp.

Reader: pattern-tree-ref (instance)
Writer: (setf pattern-tree-ref) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

ref.

Reader: pattern-tree-syms (instance)
Writer: (setf pattern-tree-syms) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

syms.

Function: print-symtree (tree &optional stream mode)
Package

bourbaki.

Source

print.lisp.

Function: print-theorem (ref &optional mode)
Package

bourbaki.

Source

print.lisp.

Function: provenp (wff)
Package

bourbaki.

Source

proof.lisp.

Function: replace-vars (str smap)

Substitute some variables in a wff

Package

bourbaki.

Source

symtree.lisp.

Function: require (name module &key provide)
Package

bourbaki.

Source

context.lisp.

Function: seek-create-ctx (name &optional class context)
Package

bourbaki.

Source

context.lisp.

Function: seek-sym (mode name1 &rest names)

Seeks for a theorem or context or symbol.

Package

bourbaki.

Source

context.lisp.

Function: show-proof (ref &optional mode)
Package

bourbaki.

Source

print.lisp.

Function: show-stats (ref)
Package

bourbaki.

Source

stats.lisp.

Function: show-unused (ref)
Package

bourbaki.

Source

stats.lisp.

Function: smap (thr expr)
Package

bourbaki.

Source

symtree.lisp.

Function: subkindp (type1 type2)
Package

bourbaki.

Source

symbol.lisp.

Reader: subproof-assert (instance)
Writer: (setf subproof-assert) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

assert.

Reader: subproof-hypo (instance)
Writer: (setf subproof-hypo) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

hypo.

Reader: subproof-prev (instance)
Writer: (setf subproof-prev) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

prev.

Reader: subproof-ref (instance)
Writer: (setf subproof-ref) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

ref.

Reader: subproof-sub (instance)
Writer: (setf subproof-sub) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

sub.

Reader: symref-args-needed (instance)
Writer: (setf symref-args-needed) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

args-needed.

Reader: symref-fn (instance)
Writer: (setf symref-fn) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

fn.

Reader: symref-proof (instance)
Writer: (setf symref-proof) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

proof.

Reader: symref-target (instance)
Writer: (setf symref-target) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

target.

Function: symtree-parse (str)

Parse an expression returned by symstr-reader

Package

bourbaki.

Source

context.lisp.

Function: verify (ref &optional nested)
Package

bourbaki.

Source

verify.lisp.

Function: wff-equal (lhs rhs)

Check if two symtrees are equal

Package

bourbaki.

Source

symtree.lisp.

Function: wff-type (str)

Type of a symtree

Package

bourbaki.

Source

symtree.lisp.

Function: wffp (str)

Check if str is a well-formed symtree

Package

bourbaki.

Source

symtree.lisp.

Function: wrap-ctx (ctx &optional nvars)
Package

bourbaki.

Source

context.lisp.


5.1.4 Standalone methods

Method: print-object ((object symref) stream)
Source

types.lisp.

Method: print-object ((object context) stream)
Source

types.lisp.


5.1.5 Structures

Structure: context

Symbol, theorem or context

Package

bourbaki.

Source

types.lisp.

Direct superclasses

structure-object.

Direct methods

print-object.

Direct slots
Slot: syms
Initform

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

Readers

context-syms.

Writers

(setf context-syms).

Slot: imports
Readers

context-imports.

Writers

(setf context-imports).

Slot: exports
Readers

context-exports.

Writers

(setf context-exports).

Slot: type
Package

common-lisp.

Readers

context-type.

Writers

(setf context-type).

Slot: class
Package

common-lisp.

Readers

context-class.

Writers

(setf context-class).

Slot: meta
Initform

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

Readers

context-meta.

Writers

(setf context-meta).

Slot: name
Readers

context-name.

Writers

(setf context-name).

Slot: vars
Readers

context-vars.

Writers

(setf context-vars).

Slot: distinct
Readers

context-distinct.

Writers

(setf context-distinct).

Slot: hypo
Readers

context-hypo.

Writers

(setf context-hypo).

Slot: assert
Package

common-lisp.

Readers

context-assert.

Writers

(setf context-assert).

Slot: proof
Readers

context-proof.

Writers

(setf context-proof).

Structure: pattern-tree
Package

bourbaki.

Source

types.lisp.

Direct superclasses

structure-object.

Direct slots
Slot: syms
Initform

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

Readers

pattern-tree-syms.

Writers

(setf pattern-tree-syms).

Slot: ref
Readers

pattern-tree-ref.

Writers

(setf pattern-tree-ref).

Structure: subproof
Package

bourbaki.

Source

types.lisp.

Direct superclasses

structure-object.

Direct slots
Slot: ref
Readers

subproof-ref.

Writers

(setf subproof-ref).

Slot: hypo
Readers

subproof-hypo.

Writers

(setf subproof-hypo).

Slot: assert
Package

common-lisp.

Readers

subproof-assert.

Writers

(setf subproof-assert).

Slot: prev
Readers

subproof-prev.

Writers

(setf subproof-prev).

Slot: sub
Readers

subproof-sub.

Writers

(setf subproof-sub).

Structure: symkind

A symbol type

Package

bourbaki.

Source

types.lisp.

Direct superclasses

structure-object.

Direct slots
Slot: name
Initform

""

Readers

symkind-name.

Writers

(setf symkind-name).

Slot: eq-op
Readers

symkind-eq-op.

Writers

(setf symkind-eq-op).

Slot: meta
Initform

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

Readers

symkind-meta.

Writers

(setf symkind-meta).

Slot: super
Readers

symkind-super.

Writers

(setf symkind-super).

Structure: symref

Reference to a symbol or context

Package

bourbaki.

Source

types.lisp.

Direct superclasses

structure-object.

Direct methods

print-object.

Direct slots
Slot: target
Readers

symref-target.

Writers

(setf symref-target).

Slot: args-needed
Readers

symref-args-needed.

Writers

(setf symref-args-needed).

Slot: fn
Readers

symref-fn.

Writers

(setf symref-fn).

Slot: class
Package

common-lisp.

Readers

symref-class.

Writers

(setf symref-class).

Slot: proof
Readers

symref-proof.

Writers

(setf symref-proof).


5.2 Internals


5.2.1 Special variables

Special Variable: *mkvar-counter*
Package

bourbaki.

Source

symbol.lisp.


5.2.2 Macros

Macro: do-proof ((var pf) &body body)
Package

bourbaki.

Source

proof.lisp.


5.2.3 Ordinary functions

Function: apply-ref (ref args)
Package

bourbaki.

Source

symref.lisp.

Function: apply-ref-proof (ref args)
Package

bourbaki.

Source

symref.lisp.

Function: args (x)
Package

bourbaki.

Source

util.lisp.

Function: bsym-reader (stream alt)
Package

bourbaki.

Source

read.lisp.

Function: cartesian-product (vars1 vars2)

Cartesian product of two lists

Package

bourbaki.

Source

util.lisp.

Function: collect-stats-thr (thr)
Package

bourbaki.

Source

stats.lisp.

Function: collect-vars (str varlist)

The list of symbols from varlist that occur in str

Package

bourbaki.

Source

symtree.lisp.

Function: compose-proof (lhs rhs)
Package

bourbaki.

Source

symref.lisp.

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.

Function: context-p (object)
Package

bourbaki.

Source

types.lisp.

Function: context-printer (obj stream)
Package

bourbaki.

Source

types.lisp.

Function: copy-context (instance)
Package

bourbaki.

Source

types.lisp.

Function: copy-items (lst from)
Package

bourbaki.

Source

parse.lisp.

Function: copy-pattern-tree (instance)
Package

bourbaki.

Source

types.lisp.

Function: copy-subproof (instance)
Package

bourbaki.

Source

types.lisp.

Function: copy-symkind (instance)
Package

bourbaki.

Source

types.lisp.

Function: copy-symref (instance)
Package

bourbaki.

Source

types.lisp.

Function: dvc (list1 list2 thr)
Package

bourbaki.

Source

distinct.lisp.

Function: dvc-1 (cnd thr)
Package

bourbaki.

Source

distinct.lisp.

Function: dvc-satisfied (thref smap condlist varlist)

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

Package

bourbaki.

Source

distinct.lisp.

Function: flatten-1 (wff)
Package

bourbaki.

Source

util.lisp.

Function: get-symkind (sym)
Package

bourbaki.

Source

parse.lisp.

Function: highest-number-in (tree)
Package

bourbaki.

Source

util.lisp.

Function: int-list (n)
Package

bourbaki.

Source

util.lisp.

Function: lib-path-name (filename &optional type)
Package

bourbaki.

Source

util.lisp.

Function: make-symkind (&key name eq-op meta super)
Package

bourbaki.

Source

types.lisp.

Function: makevarlist-r (thr)
Package

bourbaki.

Source

symtree.lisp.

Function: matcher-fn (pat)
Package

bourbaki.

Source

pattern.lisp.

Function: mkrootctx ()
Package

bourbaki.

Source

variables.lisp.

Function: op (x)
Package

bourbaki.

Source

util.lisp.

Function: pair-eq (lhs rhs)

Equality of unordered pairs

Package

bourbaki.

Source

util.lisp.

Function: parse-thr-ref (tree &optional ref args)
Package

bourbaki.

Source

context.lisp.

Function: parse-varspec (type names class)
Package

bourbaki.

Source

parse.lisp.

Function: pat-var-p (expr)
Package

bourbaki.

Source

pattern.lisp.

Function: pat-vars-in (expr)
Package

bourbaki.

Source

pattern.lisp.

Function: pattern-to-ref (pat &optional class)
Package

bourbaki.

Source

symref.lisp.

Function: pattern-tree-p (object)
Package

bourbaki.

Source

types.lisp.

Function: permute-ref (ref smap)
Package

bourbaki.

Source

pattern.lisp.

Function: permute-vars (pat ref)
Package

bourbaki.

Source

pattern.lisp.

Function: potential-vars (lst dist expr)

List of variables that potentially occur in a symtree

Package

bourbaki.

Source

symtree.lisp.

Function: print-symtree-aux (stream str &optional mode foo)
Package

bourbaki.

Source

print.lisp.

Function: print-symtree-debug (str)
Package

bourbaki.

Source

print.lisp.

Function: push-second (x lst)
Package

bourbaki.

Source

util.lisp.

Function: r-int-list (n)
Package

bourbaki.

Source

util.lisp.

Function: read-names (stream)
Package

bourbaki.

Source

read.lisp.

Function: read-segment (stream)
Package

bourbaki.

Source

read.lisp.

Function: ref-to-pattern (ref)
Package

bourbaki.

Source

symref.lisp.

Function: replace-proof-vars (pf smap)

Substitute some variables in a proof

Package

bourbaki.

Source

symtree.lisp.

Function: seek-ctx-exports (name ref)
Package

bourbaki.

Source

context.lisp.

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.

Function: simple-splice (lst len fn)
Package

bourbaki.

Source

util.lisp.

Function: splice (lst len fn)
Package

bourbaki.

Source

util.lisp.

Function: subproof-p (object)
Package

bourbaki.

Source

types.lisp.

Reader: symkind-eq-op (instance)
Writer: (setf symkind-eq-op) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

eq-op.

Reader: symkind-meta (instance)
Writer: (setf symkind-meta) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

meta.

Reader: symkind-name (instance)
Writer: (setf symkind-name) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

name.

Function: symkind-p (object)
Package

bourbaki.

Source

types.lisp.

Reader: symkind-super (instance)
Writer: (setf symkind-super) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

super.

Reader: symref-class (instance)
Writer: (setf symref-class) (instance)
Package

bourbaki.

Source

types.lisp.

Target Slot

class.

Function: symref-p (object)
Package

bourbaki.

Source

types.lisp.

Function: symref-printer (obj stream)
Package

bourbaki.

Source

types.lisp.

Function: symstr-reader (stream char)
Package

bourbaki.

Source

read.lisp.

Function: symstr-reader-aux (stream alt)
Package

bourbaki.

Source

read.lisp.

Function: symtree-parse-aux ()

Helper function for symtree-parse

Package

bourbaki.

Source

context.lisp.

Function: symtree-reparse (str)

Helper function for replace-vars

Package

bourbaki.

Source

symtree.lisp.

Function: symtree-reparse-aux (str)

Helper function for replace-vars

Package

bourbaki.

Source

symtree.lisp.

Function: theorem-sym-p (sym)
Package

bourbaki.

Source

symbol.lisp.

Function: thref-reader (stream char)
Package

bourbaki.

Source

read.lisp.

Function: verify-1 (thr)

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

Package

bourbaki.

Source

verify.lisp.

Function: verify-def (defn)

Verify soundness of a definition

Package

bourbaki.

Source

verify.lisp.

Function: verify-subproof (pf varlist dvc num)
Package

bourbaki.

Source

verify.lisp.

Function: walk-proof-tree (thr fn &optional nested)
Package

bourbaki.

Source

proof.lisp.


Appendix A Indexes


A.1 Concepts


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): Public ordinary functions
(setf context-class): Public ordinary functions
(setf context-distinct): Public ordinary functions
(setf context-exports): Public ordinary functions
(setf context-hypo): Public ordinary functions
(setf context-imports): Public ordinary functions
(setf context-meta): Public ordinary functions
(setf context-name): Public ordinary functions
(setf context-proof): Public ordinary functions
(setf context-syms): Public ordinary functions
(setf context-type): Public ordinary functions
(setf context-vars): Public ordinary functions
(setf pattern-tree-ref): Public ordinary functions
(setf pattern-tree-syms): Public ordinary functions
(setf subproof-assert): Public ordinary functions
(setf subproof-hypo): Public ordinary functions
(setf subproof-prev): Public ordinary functions
(setf subproof-ref): Public ordinary functions
(setf subproof-sub): Public ordinary functions
(setf symkind-eq-op): Private ordinary functions
(setf symkind-meta): Private ordinary functions
(setf symkind-name): Private ordinary functions
(setf symkind-super): Private ordinary functions
(setf symref-args-needed): Public ordinary functions
(setf symref-class): Private ordinary functions
(setf symref-fn): Public ordinary functions
(setf symref-proof): Public ordinary functions
(setf symref-target): Public ordinary functions

A
acond: Public macros
aif: Public macros
alias: Public macros
apply-ref: Private ordinary functions
apply-ref-proof: Private ordinary functions
args: Private ordinary functions
ass: Public macros
ax: Public macros

B
bsym-reader: Private ordinary functions

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

D
def: Public macros
defcontext: Public macros
dist: Public macros
do-proof: Private macros
dvc: Private ordinary functions
dvc-1: Private ordinary functions
dvc-list: Public ordinary functions
dvc-satisfied: Private ordinary functions
dvc-var: Public ordinary functions

E
export: Public ordinary functions
extend-metath: Public macros

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

G
get-symkind: Private ordinary functions

H
highest-number-in: Private ordinary functions
hypo: Public macros

I
if-match: Public macros
import: Public ordinary functions
in-context: Public macros
in-tree: Public ordinary functions
insert-export: Public ordinary functions
insert-import: Public ordinary functions
insert-pat: Public ordinary functions
insert-sym: Public ordinary functions
insert-wff: Public ordinary functions
int-list: Private ordinary functions

L
let-once: Public macros
lib-path-name: Private ordinary functions
linear-subproof: Public macros
load-aux: Public ordinary functions
loc: Public macros
local: Public macros

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

O
op: Private ordinary functions

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

R
r-int-list: Private ordinary functions
read-names: Private ordinary functions
read-segment: Private ordinary functions
ref-to-pattern: Private ordinary functions
replace-proof-vars: Private ordinary functions
replace-vars: Public ordinary functions
require: Public ordinary functions

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

T
th: Public macros
th-pattern: Public macros
theorem-sym-p: Private ordinary functions
theory: Public macros
thref-reader: Private ordinary functions

V
var: Public macros
var2: Public macros
verify: Public ordinary functions
verify-1: Private ordinary functions
verify-def: Private ordinary functions
verify-subproof: Private ordinary functions
virtual-metath: Public macros

W
walk-proof-tree: Private ordinary functions
wff-equal: Public ordinary functions
wff-type: Public ordinary functions
wffp: Public ordinary functions
with-gensyms: Public macros
wrap-ctx: Public ordinary functions


A.3 Variables

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

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

A
args-needed: Public structures
assert: Public structures
assert: Public structures

C
class: Public structures
class: Public structures

D
distinct: Public structures

E
eq-op: Public structures
exports: Public structures

F
fn: Public structures

H
hypo: Public structures
hypo: Public structures

I
imports: Public structures

M
meta: Public structures
meta: Public structures

N
name: Public structures
name: Public structures

P
prev: Public structures
proof: Public structures
proof: Public structures

R
ref: Public structures
ref: Public structures

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

T
target: Public structures
type: Public structures

V
vars: Public structures


A.4 Data types

Jump to:   B   C   D   F   M   P   R   S   T   U   V  
Index Entry  Section

B
bourbaki: The bourbaki system
bourbaki: The bourbaki/bourbaki module
bourbaki: The bourbaki package
bourbaki-system: The bourbaki-system package
bourbaki-user: The bourbaki-user package
bourbaki.asd: The bourbaki/bourbaki․asd file

C
context: Public structures
context.lisp: The bourbaki/bourbaki/context․lisp file

D
define.lisp: The bourbaki/bourbaki/define․lisp file
distinct.lisp: The bourbaki/bourbaki/distinct․lisp file

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

M
metatheorem.lisp: The bourbaki/bourbaki/metatheorem․lisp file
Module, bourbaki: The bourbaki/bourbaki module

P
Package, bourbaki: The bourbaki package
Package, bourbaki-system: The bourbaki-system package
Package, bourbaki-user: The bourbaki-user package
package.lisp: The bourbaki/bourbaki/package․lisp file
parse-proof.lisp: The bourbaki/bourbaki/parse-proof․lisp file
parse.lisp: The bourbaki/bourbaki/parse․lisp file
pattern-tree: Public structures
pattern.lisp: The bourbaki/bourbaki/pattern․lisp file
print.lisp: The bourbaki/bourbaki/print․lisp file
proof.lisp: The bourbaki/bourbaki/proof․lisp file

R
read.lisp: The bourbaki/bourbaki/read․lisp file

S
stats.lisp: The bourbaki/bourbaki/stats․lisp file
Structure, context: Public structures
Structure, pattern-tree: Public structures
Structure, subproof: Public structures
Structure, symkind: Public structures
Structure, symref: Public structures
subproof: Public structures
symbol.lisp: The bourbaki/bourbaki/symbol․lisp file
symkind: Public structures
symref: Public structures
symref.lisp: The bourbaki/bourbaki/symref․lisp file
symtree.lisp: The bourbaki/bourbaki/symtree․lisp file
System, bourbaki: The bourbaki system

T
types.lisp: The bourbaki/bourbaki/types․lisp file

U
util.lisp: The bourbaki/bourbaki/util․lisp file

V
variables.lisp: The bourbaki/bourbaki/variables․lisp file
verify.lisp: The bourbaki/bourbaki/verify․lisp file