gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

suspensions.lisp #89

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFMETHOD SUSPENSION-1 (CHAIN-COMPLEX) ; (DEFMETHOD CAT::SUSPENSION-1 ((CAT::CHCM CAT::CHAIN-COMPLEX)) ; (THE CAT::CHAIN-COMPLEX ; (WITH-SLOTS (CAT::CMPR CAT::BASIS CAT::DFFR) ; CAT::CHCM ; (CAT::BUILD-CHCM :CMPR (CAT::SUSPENSION-CMPR CAT::CMPR) :BASIS ; (CAT::SUSPENSION-BASIS CAT::BASIS) :BSGN :S-BSGN ; :INTR-DFFR (CAT::SUSPENSION-INTR-DFFR CAT::DFFR) ; :STRT :CMBN :ORGN ...)))) ; --> PROGN EVAL-WHEN SB-PCL::%DEFMETHOD-EXPANDER PROGN SB-PCL::LOAD-DEFMETHOD ; --> SB-PCL::LOAD-DEFMETHOD LIST* LET* SB-INT:NAMED-LAMBDA FUNCTION ; --> SYMBOL-MACROLET SB-PCL::FAST-LEXICAL-METHOD-FUNCTIONS ; --> SB-PCL::BIND-FAST-LEXICAL-METHOD-FUNCTIONS FLET SB-PCL::BIND-ARGS LET* ; --> LOCALLY SYMBOL-MACROLET BLOCK ; ==> ; (THE CAT::CHAIN-COMPLEX ; (LET ((#:G66 CAT::CHCM)) ; (DECLARE (IGNORABLE #:G66)) ; (DECLARE (SB-PCL::%VARIABLE-REBINDING #:G66 CAT::CHCM)) ; #:G66 ; (SYMBOL-MACROLET ((CAT::CMPR #) (CAT::BASIS #) (CAT::DFFR #)) ; (CAT::BUILD-CHCM :CMPR (CAT::SUSPENSION-CMPR #) :BASIS ; (CAT::SUSPENSION-BASIS #) :BSGN :S-BSGN :INTR-DFFR ; (CAT::SUSPENSION-INTR-DFFR #) :STRT :CMBN :ORGN ; ...)))) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFMETHOD SUSPENSION-1 (MORPHISM) ; (THE CAT::MORPHISM ; (LET ((CAT::ORGN (CAT::ORGN CAT::MRPH))) ; (DECLARE (LIST CAT::ORGN)) ; (WHEN (EQ (FIRST CAT::ORGN) 'CAT::ZERO-MRPH) ; (RETURN-FROM CAT::SUSPENSION-1 (CAT::ZERO-MRPH # # #))) ; (WHEN (EQ (FIRST CAT::ORGN) 'CAT::IDNT-MRPH) ; (RETURN-FROM CAT::SUSPENSION-1 (CAT::IDNT-MRPH #))) ; (CAT::BUILD-MRPH :SORC (CAT::SUSPENSION (CAT::SORC CAT::MRPH)) :TRGT ; (CAT::SUSPENSION (CAT::TRGT CAT::MRPH)) :DEGR ; (CAT::DEGR CAT::MRPH) :INTR ; (CAT::SUSPENSION-INTR CAT::MRPH) :STRT :CMBN :ORGN ; ...))) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFMETHOD SUSPENSION-1 (REDUCTION) ; (THE CAT::REDUCTION ; (PROGN ; (WHEN (EQ (FIRST #) 'CAT::TRIVIAL-RDCT) ; (RETURN-FROM CAT::SUSPENSION-1 (CAT::TRIVIAL-RDCT #))) ; (CAT::BUILD-RDCT :F (CAT::SUSPENSION (CAT::F CAT::RDCT)) :G ; (CAT::SUSPENSION (CAT::G CAT::RDCT)) :H ; (CAT::SUSPENSION (CAT::H CAT::RDCT)) :ORGN ; `(CAT::SUSPENSION ,CAT::RDCT)))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFMETHOD SUSPENSION-1 (HOMOTOPY-EQUIVALENCE) ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (PROGN ; (WHEN (EQ (FIRST #) 'CAT::TRIVIAL-HMEQ) ; (RETURN-FROM CAT::SUSPENSION-1 (CAT::TRIVIAL-HMEQ #))) ; (CAT::BUILD-HMEQ :LRDCT (CAT::SUSPENSION (CAT::LRDCT CAT::HMEQ)) :RRDCT ; (CAT::SUSPENSION (CAT::RRDCT CAT::HMEQ)) :ORGN ; `(CAT::SUSPENSION ,CAT::HMEQ)))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).