KeenS

$ cim for abcl alisp ccl clisp ecl gcl sbcl do --no-init -e "(defun fib (n) (if (> 1 n) 1 (+ (fib (- n 1)) (fib (- n 2)))))"  -e "(time (fib 32))" 
>>>abcl --no-init -e (defun fib (n) (if (> 1 n) 1 (+ (fib (- n 1)) (fib (- n 2))))) -e (time (fib 32))
13.671 seconds real time
0 cons cells
<<<
>>>alisp --no-init -e (defun fib (n) (if (> 1 n) 1 (+ (fib (- n 1)) (fib (- n 2))))) -e (time (fib 32))
; cpu time (non-gc) 72.680028 sec (00:01:12.680028) user, 0.028029 sec system
; cpu time (gc)     19.753366 sec user, 0.059581 sec system
; cpu time (total)  92.433394 sec (00:01:32.433394) user, 0.087610 sec system
; real time  92.662947 sec (00:01:32.662947) (99.85%)

KeenS

$ cim for alisp ccl clisp ecl gcl sbcl do -qe '(print (expt 1.01 365))'
>>>alisp -qe (print (expt 1.01 365))

37.783386 ; Exiting
<<<
>>>ccl -qe (print (expt 1.01 365))

37.783386 
<<<
>>>clisp -qe (print (expt 1.01 365))

KeenS

(ql:quickload :optima)
(use-package :optima)

(defun list-slots (obj slots conc-name)
  (loop :for slot :in slots :collect
     (funcall (intern (format nil "~a~a" conc-name slot)) obj)))

(defun make-print-object (name gensyms)
  `(lambda (obj stream)
      (format stream "(~a ~{~a~^ ~})" ',name

KeenS

range
datetime (date & time)
set
sortedset
queue
tree (btree)
regexp
format scanner
lazy
copy

KeenS

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros.
  apply H0.
  assumption.
Qed.

KeenS

Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  intros.
  destruct H.
  intro.
  apply H.
  apply H0.
  apply H1.
Qed.

KeenS

Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
  intros.
  destruct H.
  destruct H0.
  apply H.
  apply H.
Qed.

KeenS

Theorem DeBolran1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
  intros.
  destruct H.
  intro.
  destruct H0.
  apply H, H0.
  intro.
  destruct H.
  destruct H0.

KeenS

Lemma NotNot : forall P : Prop, P -> ~~P.
Proof.
  intros.
  unfold not.
  intros.
  apply H0.
  apply H.
Qed.

Require Import Classical.

KeenS

Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
  intros.
  split.
  intro.
  destruct H.
  left.
  apply H0.
  intro.
  destruct H.