;;; (C) 2008-2009 Dr. Gergo ERDI (in-package :alef) (parse-and-run `(,@*library* (deftype nat () zero (succ nat)) (define +/nat (x zero) x) (define +/nat (x (succ y)) (succ (+/nat x y))) (define one () (succ zero)) (define two () (succ one)) (define three () (succ two)) (define =/nat (zero zero) true) (define =/nat ((succ x) (succ y)) (=/nat x y)) (define =/nat (_ _) false) (define