# Author: Paul Fitzpatrick, paulfitz@ai.mit.edu
# Copyright (c) 2003 Paul Fitzpatrick
#
# This file is part of CosmicOS.
#
# CosmicOS is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# CosmicOS is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with CosmicOS; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
#

# MATH introduce numbers (in unary notation)
(intro (unary (.)));
(intro (unary (:)(.)));
(intro (unary (:)(:)(.)));
(intro (unary (:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(.)));
(intro (unary (:)(:)(.)));
(intro (unary (:)(.)));
(intro (unary (.)));
(intro (unary (.)));
(intro (unary (:)(.)));
(intro (unary (:)(:)(.)));
(intro (unary (:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (.)));
(intro (unary (:)(.)));
(intro (unary (:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (.)));
(intro (unary (:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)));
(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
# MATH now show equality
(intro =);
(= (unary (.)) (unary (.)));
(= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)));
(= (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)));
(= (unary (:)(:)(.)) (unary (:)(:)(.)));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
# MATH now show other relational operators
(intro >);
(> (unary (:)(:)(:)(.)) (unary (:)(.)));
(> (unary (:)(.)) (unary (.)));
(> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (.)));
(> (unary (:)(:)(:)(:)(.)) (unary (.)));
(> (unary (:)(:)(:)(:)(:)(.)) (unary (.)));
(> (unary (:)(:)(:)(:)(.)) (unary (.)));
(> (unary (:)(.)) (unary (.)));
(> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(.)));
(> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(.)));
(> (unary (:)(:)(:)(.)) (unary (:)(.)));
(> (unary (:)(:)(:)(:)(:)(.)) (unary (.)));
(intro <);
(< (unary (.)) (unary (:)(:)(:)(:)(:)(:)(.)));
(< (unary (.)) (unary (:)(.)));
(< (unary (.)) (unary (:)(.)));
(< (unary (.)) (unary (:)(:)(.)));
(< (unary (:)(.)) (unary (:)(:)(:)(.)));
(< (unary (.)) (unary (:)(:)(.)));
(< (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.)));
(< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
(< (unary (.)) (unary (:)(:)(.)));
(< (unary (.)) (unary (:)(:)(:)(:)(:)(.)));
(< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)));
(< (unary (:)(:)(.)) (unary (:)(:)(:)(.)));
(> (unary (:)(:)(.)) (unary (:)(.)));
(> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(.)));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(> (unary (:)(.)) (unary (.)));
(< (unary (:)(.)) (unary (:)(:)(:)(:)(.)));
(= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)));
(> (unary (:)(:)(:)(.)) (unary (:)(:)(.)));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
# MATH introduce the NOT logical operator
(intro not);
(= (unary (:)(.)) (unary (:)(.)));
(not (< (unary (:)(.)) (unary (:)(.))));
(not (> (unary (:)(.)) (unary (:)(.))));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(not (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(= (unary (.)) (unary (.)));
(not (< (unary (.)) (unary (.))));
(not (> (unary (.)) (unary (.))));
(= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(not (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(= (unary (:)(.)) (unary (:)(.)));
(not (< (unary (:)(.)) (unary (:)(.))));
(not (> (unary (:)(.)) (unary (:)(.))));
(= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(.)) (unary (:)(:)(:)(:)(.))));
(< (unary (:)(.)) (unary (:)(:)(:)(:)(.)));
(not (> (unary (:)(.)) (unary (:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(< (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.)));
(not (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(not (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(not (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(.)) (unary (:)(:)(:)(.))));
(< (unary (:)(.)) (unary (:)(:)(:)(.)));
(not (> (unary (:)(.)) (unary (:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)));
(not (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(> (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(> (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(.)) (unary (:)(.))));
(> (unary (:)(:)(:)(.)) (unary (:)(.)));
(not (< (unary (:)(:)(:)(.)) (unary (:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(> (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (= (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.)));
(not (< (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
# MATH introduce the AND logical operator
(intro and);
(and (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(and (= (unary (:)(.)) (unary (:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(and (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(.)) (unary (:)(.))));
(and (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(and (> (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(.))));
(and (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(and (= (unary (:)(:)(.)) (unary (:)(:)(.))) (< (unary (.)) (unary (:)(:)(.))));
(and (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(.))));
(and (< (unary (:)(.)) (unary (:)(:)(:)(:)(.))) (= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(and (< (unary (:)(.)) (unary (:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(.))));
(not (and (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (> (unary (.)) (unary (:)(.)))));
(not (and (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (and (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(.)) (unary (:)(:)(:)(:)(:)(.)))));
(not (and (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)))));
(not (and (= (unary (:)(.)) (unary (:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.)))));
(not (and (> (unary (:)(:)(.)) (unary (:)(:)(:)(.))) (< (unary (:)(.)) (unary (:)(:)(:)(.)))));
(not (and (< (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(.))) (> (unary (:)(:)(:)(.)) (unary (:)(:)(.)))));
(not (and (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (> (unary (:)(:)(.)) (unary (.)))));
(not (and (= (unary (:)(.)) (unary (.))) (> (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)))));
(not (and (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)))));
(not (and (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)))));
(not (and (= (unary (:)(:)(:)(:)(.)) (unary (.))) (> (unary (.)) (unary (:)(:)(:)(.)))));
(not (and (= (unary (:)(:)(:)(:)(:)(.)) (unary (.))) (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.)))));
(not (and (> (unary (.)) (unary (:)(:)(:)(:)(.))) (> (unary (:)(:)(.)) (unary (:)(:)(.)))));
(not (and (= (unary (.)) (unary (:)(:)(:)(:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(.)))));
(not (and (< (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(.)) (unary (:)(.)))));
(and (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(not (and (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (> (unary (:)(:)(.)) (unary (:)(:)(:)(.)))));
(not (and (> (unary (:)(.)) (unary (.))) (< (unary (:)(:)(:)(.)) (unary (:)(:)(.)))));
(and (< (unary (.)) (unary (:)(:)(.))) (> (unary (:)(.)) (unary (.))));
(not (and (= (unary (:)(:)(:)(:)(.)) (unary (:)(.))) (> (unary (.)) (unary (:)(:)(:)(.)))));
(not (and (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(.)))));
(not (and (= (unary (:)(:)(.)) (unary (:)(.))) (> (unary (:)(.)) (unary (:)(:)(:)(.)))));
(not (and (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (= (unary (:)(.)) (unary (:)(.)))));
(not (and (> (unary (:)(:)(.)) (unary (:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)))));
# MATH introduce the OR logical operator
(intro or);
(or (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(or (< (unary (:)(.)) (unary (:)(:)(.))) (> (unary (:)(:)(.)) (unary (.))));
(or (> (unary (:)(:)(:)(:)(.)) (unary (:)(.))) (< (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(or (< (unary (:)(.)) (unary (:)(:)(:)(:)(.))) (> (unary (:)(.)) (unary (.))));
(or (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (= (unary (.)) (unary (.))));
(or (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(or (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(or (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(:)(.))));
(or (= (unary (.)) (unary (.))) (= (unary (:)(:)(.)) (unary (:)(:)(.))));
(or (< (unary (.)) (unary (:)(:)(:)(.))) (= (unary (.)) (unary (.))));
(or (< (unary (.)) (unary (:)(:)(.))) (= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(.))));
(or (> (unary (:)(:)(:)(.)) (unary (:)(.))) (= (unary (.)) (unary (:)(:)(.))));
(or (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (= (unary (:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(or (< (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(or (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(or (> (unary (.)) (unary (:)(:)(:)(:)(.))) (= (unary (.)) (unary (.))));
(or (= (unary (:)(:)(.)) (unary (.))) (< (unary (.)) (unary (:)(:)(.))));
(or (< (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(or (= (unary (:)(:)(.)) (unary (.))) (= (unary (.)) (unary (.))));
(or (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (< (unary (:)(.)) (unary (:)(:)(.))));
(not (or (> (unary (:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (or (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)))));
(not (or (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (= (unary (:)(.)) (unary (.)))));
(not (or (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.)))));
(not (or (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (> (unary (.)) (unary (.)))));
(not (or (> (unary (.)) (unary (:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.)))));
(not (or (> (unary (:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (< (unary (:)(:)(.)) (unary (.)))));
(or (> (unary (.)) (unary (:)(:)(:)(.))) (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(or (< (unary (:)(:)(:)(:)(.)) (unary (.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(:)(.))));
(or (= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))) (= (unary (:)(:)(.)) (unary (:)(:)(.))));
(not (or (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (< (unary (:)(:)(.)) (unary (:)(.)))));
(or (> (unary (:)(:)(:)(:)(.)) (unary (:)(.))) (> (unary (:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(or (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(not (or (> (unary (.)) (unary (.))) (= (unary (:)(:)(.)) (unary (:)(:)(:)(.)))));
(or (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (< (unary (:)(:)(:)(.)) (unary (:)(.))));
# MATH use equality for truth values
(= (> (unary (:)(:)(:)(:)(.)) (unary (:)(:)(.))) (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(= (= (unary (:)(:)(.)) (unary (:)(:)(.))) (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(:)(.))));
(= (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(.)) (unary (:)(.))));
(= (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(= (= (unary (:)(:)(.)) (unary (:)(:)(.))) (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(= (= (unary (:)(:)(:)(.)) (unary (:)(:)(.))) (= (unary (:)(.)) (unary (.))));
(= (> (unary (.)) (unary (:)(.))) (< (unary (:)(:)(:)(:)(.)) (unary (:)(.))));
(= (> (unary (:)(.)) (unary (:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(= (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (< (unary (:)(.)) (unary (.))));
(= (= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (= (unary (.)) (unary (:)(:)(:)(:)(.))));
(not (= (= (unary (:)(.)) (unary (.))) (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.)))));
(not (= (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (= (unary (.)) (unary (.)))));
(not (= (< (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.)))));
(not (= (= (unary (.)) (unary (:)(.))) (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (= (> (unary (:)(.)) (unary (:)(:)(:)(:)(.))) (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (= (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (= (unary (:)(:)(:)(:)(.)) (unary (:)(.)))));
(not (= (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))) (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (= (< (unary (.)) (unary (:)(:)(.))) (= (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.)))));
(not (= (> (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (< (unary (:)(:)(.)) (unary (.)))));
(not (= (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (= (unary (:)(:)(:)(.)) (unary (.)))));
(intro true);
(intro false);
(= (true) (= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(= (true) (= (unary (.)) (unary (.))));
(= (true) (> (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))));
(= (true) (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(= (true) (> (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))));
(= (< (unary (:)(.)) (unary (:)(:)(:)(:)(.))) (true));
(= (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (true));
(= (= (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))) (true));
(= (< (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (true));
(= (= (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (true));
(= (false) (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(= (false) (= (unary (:)(:)(.)) (unary (:)(:)(:)(:)(.))));
(= (false) (< (unary (:)(:)(.)) (unary (.))));
(= (false) (> (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(:)(:)(.))));
(= (false) (< (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))));
(= (> (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (false));
(= (= (unary (:)(:)(.)) (unary (:)(.))) (false));
(= (= (unary (:)(:)(.)) (unary (:)(:)(:)(:)(:)(.))) (false));
(= (< (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (false));
(= (< (unary (:)(:)(:)(.)) (unary (:)(.))) (false));
(= (true) (true));
(= (false) (false));
(not (= (true) (false)));
(not (= (false) (true)));
# MATH introduce addition
(intro +);
(= (+ (unary (:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(= (+ (unary (.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(.)));
(= (+ (unary (.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(.)));
(= (+ (unary (:)(.)) (unary (.))) (unary (:)(.)));
(= (+ (unary (.)) (unary (.))) (unary (.)));
(= (+ (unary (:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(.)));
(= (+ (unary (:)(.)) (unary (.))) (unary (:)(.)));
(= (+ (unary (:)(.)) (unary (.))) (unary (:)(.)));
(= (+ (unary (:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(:)(.)));
(= (+ (unary (.)) (unary (.))) (unary (.)));
# MATH introduce subtraction
(intro -);
(= (- (unary (:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(.)));
(= (- (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(.)));
(= (- (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (unary (:)(:)(:)(.)));
(= (- (unary (:)(:)(:)(:)(:)(.)) (unary (:)(:)(.))) (unary (:)(:)(:)(.)));
(= (- (unary (:)(.)) (unary (:)(.))) (unary (.)));
(= (- (unary (.)) (unary (.))) (unary (.)));
(= (- (unary (:)(:)(.)) (unary (.))) (unary (:)(:)(.)));
(= (- (unary (:)(:)(:)(:)(:)(:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(.)));
(= (- (unary (:)(:)(:)(:)(.)) (unary (:)(:)(:)(:)(.))) (unary (.)));
(= (- (unary (:)(:)(:)(.)) (unary (.))) (unary (:)(:)(:)(.)));
# MATH introduce multiplication
(intro *);
(= (* (unary (.)) (unary (.))) (unary (.)));
(= (* (unary (.)) (unary (:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(:)(:)(.))) (unary (.)));
(= (* (unary (:)(.)) (unary (.))) (unary (.)));
(= (* (unary (:)(.)) (unary (:)(.))) (unary (:)(.)));
(= (* (unary (:)(.)) (unary (:)(:)(.))) (unary (:)(:)(.)));
(= (* (unary (:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(.)));
(= (* (unary (:)(:)(.)) (unary (.))) (unary (.)));
(= (* (unary (:)(:)(.)) (unary (:)(.))) (unary (:)(:)(.)));
(= (* (unary (:)(:)(.)) (unary (:)(:)(.))) (unary (:)(:)(:)(:)(.)));
(= (* (unary (:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(:)(:)(.)));
(= (* (unary (:)(:)(:)(.)) (unary (.))) (unary (.)));
(= (* (unary (:)(:)(:)(.)) (unary (:)(.))) (unary (:)(:)(:)(.)));
(= (* (unary (:)(:)(:)(.)) (unary (:)(:)(.))) (unary (:)(:)(:)(:)(:)(:)(.)));
(= (* (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (* (unary (:)(:)(:)(.)) (unary (.))) (unary (.)));
(= (* (unary (.)) (unary (:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(:)(.))) (unary (.)));
(= (* (unary (:)(:)(:)(.)) (unary (:)(.))) (unary (:)(:)(:)(.)));
(= (* (unary (:)(:)(:)(.)) (unary (:)(:)(:)(.))) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (* (unary (:)(.)) (unary (:)(:)(.))) (unary (:)(:)(.)));
(= (* (unary (.)) (unary (:)(.))) (unary (.)));
(= (* (unary (.)) (unary (:)(:)(:)(.))) (unary (.)));
# MATH introduce a simple form of binary notation
# After this lesson, in the higher-level version of the message,
# will expand decimal to stand for the binary notation given.
(= (unary (.)) (.));
(= (unary (:)(.)) (:));
(= (unary (:)(:)(.)) (:.));
(= (unary (:)(:)(:)(.)) (::));
(= (unary (:)(:)(:)(:)(.)) (:..));
(= (unary (:)(:)(:)(:)(:)(.)) (:.:));
(= (unary (:)(:)(:)(:)(:)(:)(.)) (::.));
(= (unary (:)(:)(:)(:)(:)(:)(:)(.)) (:::));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(.)) (:...));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (:..:));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (:.:.));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (:.::));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (::..));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (::.:));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (:::.));
(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)) (::::));
(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (::) (unary (:)(:)(:)(.)));
(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (:.:) (unary (:)(:)(:)(:)(:)(.)));
(= (:..:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (:.:) (unary (:)(:)(:)(:)(:)(.)));
(= (::::) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (:..:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (::.) (unary (:)(:)(:)(:)(:)(:)(.)));
(= (:::) (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(= (:..) (unary (:)(:)(:)(:)(.)));
(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (:::) (unary (:)(:)(:)(:)(:)(:)(:)(.)));
(= (:::.) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(.)));
(= (:.:) (unary (:)(:)(:)(:)(:)(.)));
(= (+ (:.) (:.:)) (:::));
(= (+ (::.) (::.)) (::..));
(= (+ (::..) (::)) (::::));
(= (+ (:.) (::)) (:.:));
(= (+ (:...) (:...)) (:....));
(= (+ (::.:) (:::.)) (::.::));
(= (+ (:::) (:.:.)) (:...:));
(= (+ (::..) (:.::)) (:.:::));
(= (* (::.:) (:..:)) (:::.:.:));
(= (* (::..) (::.:)) (:..:::..));
(= (* (::..) (:.:.)) (::::...));
(= (* (::..) (::::)) (:.::.:..));
(= (* (:) (::.)) (::.));
(= (* (::.) (:.:.)) (::::..));
(= (* (:..) (:::.)) (:::...));
(= (* (::::) (:..:)) (:....:::));
# MATH demonstrate idea of leaving gaps in an expression
# and then filling them in afterwards
# the examples given leave a lot to be desired!
((? x (= (+ 2 (x)) 13)) 11);
((? x (= (+ 11 (x)) 21)) 10);
((? x (= (+ 9 (x)) 11)) 2);
((? x (= (+ 12 (x)) 18)) 6);
((? x (= (+ 6 (x)) 20)) 14);
((? x (= (+ 8 (x)) 10)) 2);
((? x (= (+ 11 (x)) 18)) 7);
((? x (= (+ 8 (x)) 13)) 5);
(((? x (? y (= (* (x) (y)) 12))) 6) 2);
(((? x (? y (= (* (x) (y)) 84))) 12) 7);
(((? x (? y (= (* (x) (y)) 45))) 15) 3);
(((? x (? y (= (* (x) (y)) 18))) 3) 6);
(((? x (? y (= (* (x) (y)) 90))) 15) 6);
(((? x (? y (= (* (x) (y)) 36))) 3) 12);
(((? x (? y (= (* (x) (y)) 30))) 2) 15);
(((? x (? y (= (* (x) (y)) 32))) 8) 4);
((((? x (? y (? z (= (* (x) (y)) (z))))) 11) 1) 11);
((((? x (? y (? z (= (* (x) (y)) (z))))) 121) 11) 11);
((((? x (? y (? z (= (* (x) (y)) (z))))) 156) 12) 13);
((((? x (? y (? z (= (* (x) (y)) (z))))) 16) 2) 8);
((((? x (? y (? z (= (* (x) (y)) (z))))) 0) 4) 0);
((((? x (? y (? z (= (* (x) (y)) (z))))) 108) 12) 9);
((((? x (? y (? z (= (* (x) (y)) (z))))) 80) 10) 8);
((((? x (? y (? z (= (* (x) (y)) (z))))) 8) 8) 1);
# MATH show some simple function calls
# and show a way to remember functions across statements
(= ((? square (square 1)) (? x (* (x) (x)))) 1);
(= ((? square (square 2)) (? x (* (x) (x)))) 4);
(= ((? square (square 0)) (? x (* (x) (x)))) 0);
(= ((? square (square 8)) (? x (* (x) (x)))) 64);
(= ((? square (square 5)) (? x (* (x) (x)))) 25);
(= ((? square (square 1)) (? x (* (x) (x)))) 1);
(= ((? square (square 8)) (? x (* (x) (x)))) 64);
(= ((? square (square 3)) (? x (* (x) (x)))) 9);
(define square (? x (* (x) (x))));
(= (square 0) 0);
(= (square 7) 49);
(= (square 5) 25);
(= (square 6) 36);
(define plusone (? x (+ (x) 1)));
(= (plusone 7) 8);
(= (plusone 3) 4);
(= (plusone 6) 7);
(= (plusone 9) 10);
# MATH show mechanisms for branching
(intro if);
(= (if (true) 8 4) 8);
(= (if (true) 0 0) 0);
(= (if (true) 2 7) 2);
(= (if (true) 9 7) 9);
(= (if (true) 0 3) 0);
(= (if (true) 0 4) 0);
(= (if (true) 4 9) 4);
(= (if (false) 7 9) 9);
(= (if (false) 0 8) 8);
(= (if (false) 6 3) 3);
(= (if (false) 2 8) 8);
(= (if (false) 0 3) 3);
(= (if (true) 8 0) 8);
(= (if (false) 2 1) 1);
(= (if (true) 4 7) 4);
(= (if (false) 2 6) 6);
# MATH some pure lambda calculus definitions - optional
# these definitions are not quite what we want
# since thinking of everything as a function requires headscratching
# it would be better to use these as a parallel means of evaluation
# ... for expressions
(define if (? x (? y (? z (x (y) (z))))));
(define true (? y (? z (y))));
(define false (? y (? z (z))));
(define cons (? x (? y (? z (if (z) (x) (y))))));
(define car (? x (x (true))));
(define cdr (? x (x (false))));
(define zero (? f (? x (x))));
(define one (? f (? x (f (x)))));
(define two (? f (? x (f (f (x))))));
(define succ (? n (? f (? x (f ((n (f)) (x)))))));
(define add (? a (? b ((a (succ)) (b)))));
(define mult (? a (? b ((a (add (b))) (zero)))));
(define pred (? n (cdr ((n (? p (cons (succ (car (p))) (car (p))))) (cons (zero) (zero))))));
(define is-zero (? n ((n (? dummy (false)) (true)))));
(define fixed-point (? f ((? x (f (x (x)))) (? x (f (x (x)))))));
# .. but for rest of message will assume that define does fixed-point for us
# now build a link between numbers and church number functions
(define unchurch (? c (c (? x (+ (x) 1)) 0)));
(= 0 (unchurch (zero)));
(= 1 (unchurch (one)));
(= 2 (unchurch (two)));
(define church (? x (if (= 0 (x)) (zero) (succ (church (- (x) 1))))));
# MATH show an example of recursive evaluation
# skipping over a lot of definitions and desugarings
(define factorial (? x (if (> (x) 0) (* (x) (factorial (- (x) 1))) 1)));
(= (factorial 0) 1);
(= (factorial 1) 1);
(= (factorial 2) 2);
(= (factorial 3) 6);
(= (factorial 4) 24);
(= (factorial 5) 120);
# show a definition for the unary function used early on
(define unary (? x (if (= (x) 0) 0 (+ (unary) 1))));
# MATH introduce universal quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(intro forall);
(< 5 (+ 5 1));
(< 4 (+ 4 1));
(< 3 (+ 3 1));
(< 2 (+ 2 1));
(< 1 (+ 1 1));
(< 0 (+ 0 1));
(forall (? x (< (x) (+ (x) 1))));
(< 5 (* 5 2));
(< 4 (* 4 2));
(< 3 (* 3 2));
(< 2 (* 2 2));
(< 1 (* 1 2));
(not (< 0 (* 0 2)));
(not (forall (? x (< (x) (* (x) 2)))));
# MATH introduce existential quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(not (= 5 (* 2 2)));
(= 4 (* 2 2));
(not (= 3 (* 2 2)));
(not (= 2 (* 2 2)));
(not (= 1 (* 2 2)));
(not (= 0 (* 2 2)));
(intro exists);
(exists (? x (= (x) (* 2 2))));
(not (= 5 (+ 5 2)));
(not (= 4 (+ 4 2)));
(not (= 3 (+ 3 2)));
(not (= 2 (+ 2 2)));
(not (= 1 (+ 1 2)));
(not (= 0 (+ 0 2)));
(not (exists (? x (= (x) (+ (x) 2)))));
# MATH introduce logical implication
(intro =>);
(=> (true) (true));
(not (=> (true) (false)));
(=> (false) (true));
(=> (false) (false));
(forall (? x (forall (? y (=> (=> (x) (y)) (=> (not (y)) (not (x))))))));
# MATH illustrate lists and some list operators
# to make list describable as a function, need to preceed lists
# ... with an argument count
# lists will be written as [1 2 1] = (list 3 1 2 1) after this lesson
# it would be nice to include such syntactic sugar in the message but that
# ... is a fight for another day
# finally, lists keep an explicit record of their length
# this is to avoid the need for using a special 'nil' symbol
# ... which cannot itself be placed in the list.
(define list (? n (if (= (n) 0) (cons 0 0) (? x (if (= (n) 1) (cons 1 (x)) (cons (n) (cons (x) (cdr (list (- (n) 1))))))))));
(define head (? lst (if (= (car (lst)) 0) (undefined) (if (= (car (lst)) 1) (cdr (lst)) (car (cdr (lst)))))));
(define tail (? lst (if (= (car (lst)) 0) (undefined) (if (= (car (lst)) 1) (cons 0 0) (cons (- (car (lst)) 1) (cdr (cdr (lst))))))));
(define list-length (? lst (car (lst))));
(define list-ref (? lst (? n (if (= (list-ref (lst)) 0) (undefined) (if (= (n) 0) (head (lst)) (list-ref (tail (lst)) (- (n) 1)))))));
(define prepend (? x (? lst (if (= (get-length (lst)) 0) (cons 1 (x)) (cons (+ (get-length (lst)) 1) (cons (x) (lst)))))));
(= (list-length ((list 1) 3)) 1);
(= (list-length ((list 8) 9 8 0 4 7 3 6 5)) 8);
(= (list-length ((list 5) 8 6 4 2 5)) 5);
(= (list-length ((list 9) 5 8 4 3 9 6 1 7 2)) 9);
(= (list-length ((list 7) 2 4 9 6 5 0 8)) 7);
(= (head ((list 8) 12 1 4 13 17 3 10 4)) 12);
(= (tail ((list 8) 12 1 4 13 17 3 10 4)) ((list 7) 1 4 13 17 3 10 4));
(= (head ((list 9) 6 13 15 4 12 1 0 5 6)) 6);
(= (tail ((list 9) 6 13 15 4 12 1 0 5 6)) ((list 8) 13 15 4 12 1 0 5 6));
(= (head ((list 6) 19 4 12 2 15 12)) 19);
(= (tail ((list 6) 19 4 12 2 15 12)) ((list 5) 4 12 2 15 12));
(= (head ((list 10) 3 4 4 2 15 3 17 6 11 3)) 3);
(= (tail ((list 10) 3 4 4 2 15 3 17 6 11 3)) ((list 9) 4 4 2 15 3 17 6 11 3));
(= (head ((list 2) 15 2)) 15);
(= (tail ((list 2) 15 2)) ((list 1) 2));
(= (head ((list 10) 15 12 17 11 0 12 14 8 17 5)) 15);
(= (tail ((list 10) 15 12 17 11 0 12 14 8 17 5)) ((list 9) 12 17 11 0 12 14 8 17 5));
(= (head ((list 5) 11 1 10 7 9)) 11);
(= (tail ((list 5) 11 1 10 7 9)) ((list 4) 1 10 7 9));
(= (head ((list 3) 19 10 14)) 19);
(= (tail ((list 3) 19 10 14)) ((list 2) 10 14));
(= (head ((list 5) 4 2 7 12 18)) 4);
(= (tail ((list 5) 4 2 7 12 18)) ((list 4) 2 7 12 18));
(= (head ((list 5) 13 1 0 5 10)) 13);
(= (tail ((list 5) 13 1 0 5 10)) ((list 4) 1 0 5 10));
(= (list-ref ((list 1) 9) 0) 9);
(= (list-ref ((list 10) 4 4 14 0 14 4 17 7 3 17) 0) 4);
(= (list-ref ((list 8) 10 13 6 14 3 13 9 18) 0) 10);
(= (list-ref ((list 4) 3 1 0 2) 2) 0);
(= (list-ref ((list 5) 13 7 18 13 12) 1) 7);
(= (list-ref ((list 3) 19 16 9) 2) 9);
(= (list-ref ((list 5) 12 14 5 14 4) 4) 4);
(= (list-ref ((list 2) 10 17) 1) 17);
(= (list-ref ((list 4) 1 12 10 18) 3) 18);
(= (list-ref ((list 8) 17 7 2 4 19 15 4 9) 0) 17);
(= ((list 0)) ((list 0)));
(= ((list 1) 7) ((list 1) 7));
(= ((list 2) 1 19) ((list 2) 1 19));
(= ((list 3) 18 1 18) ((list 3) 18 1 18));
(= ((list 4) 13 15 10 6) ((list 4) 13 15 10 6));
# this next batch of examples are a bit misleading, should streamline
(not (= ((list 0)) ((list 1) 0)));
(not (= ((list 0)) ((list 1) 6)));
(not (= ((list 1) 9) ((list 2) 6 9)));
(not (= ((list 1) 9) ((list 2) 9 7)));
(not (= ((list 2) 1 6) ((list 3) 2 1 6)));
(not (= ((list 2) 1 6) ((list 3) 1 6 0)));
(not (= ((list 3) 10 9 12) ((list 4) 5 10 9 12)));
(not (= ((list 3) 10 9 12) ((list 4) 10 9 12 3)));
(not (= ((list 4) 17 9 1 0) ((list 5) 4 17 9 1 0)));
(not (= ((list 4) 17 9 1 0) ((list 5) 17 9 1 0 4)));
# some helpful functions
(= (prepend 12 ((list 0))) ((list 1) 12));
(= (prepend 0 ((list 1) 14)) ((list 2) 0 14));
(= (prepend 10 ((list 2) 8 19)) ((list 3) 10 8 19));
(= (prepend 12 ((list 3) 10 2 1)) ((list 4) 12 10 2 1));
(= (prepend 14 ((list 4) 6 16 14 5)) ((list 5) 14 6 16 14 5));
(= (prepend 4 ((list 5) 15 2 3 11 8)) ((list 6) 4 15 2 3 11 8));
(= (prepend 12 ((list 6) 9 2 19 7 2 0)) ((list 7) 12 9 2 19 7 2 0));
(= (prepend 11 ((list 7) 17 17 2 4 16 5 14)) ((list 8) 11 17 17 2 4 16 5 14));
(define pair (? x (? y ((list 2) (x) (y)))));
(= (pair 3 6) ((list 2) 3 6));
(= (first (pair 3 6)) 3);
(= (second (pair 3 6)) 6);
(= (pair 8 8) ((list 2) 8 8));
(= (first (pair 8 8)) 8);
(= (second (pair 8 8)) 8);
(= (pair 9 2) ((list 2) 9 2));
(= (first (pair 9 2)) 9);
(= (second (pair 9 2)) 2);
(define list-find-helper (? lst (? key (? fail (? idx (if (= (list-length (lst)) 0) (fail 0) (if (= (head (lst)) (key)) (idx) (list-find-helper (tail (lst)) (key) (fail) (+ (idx) 1)))))))));
(define list-find (? lst (? key (? fail (list-find-helper (lst) (key) (fail) 0)))));
(define example-fail (? x 100));
(= (list-find ((list 1) 15) 15 (example-fail)) 0);
(= (list-find ((list 2) 9 6) 9 (example-fail)) 0);
(= (list-find ((list 4) 19 7 14 6) 19 (example-fail)) 0);
(= (list-find ((list 8) 10 0 6 9 5 10 2 2) 5 (example-fail)) 4);
(= (list-find ((list 4) 14 5 7 6) 6 (example-fail)) 3);
(= (list-find ((list 1) 2) 2 (example-fail)) 0);
(= (list-find ((list 7) 19 7 12 4 18 8 7) 4 (example-fail)) 3);
(= (list-find ((list 1) 2) 2 (example-fail)) 0);
(= (list-find ((list 4) 5 19 13 13) 19 (example-fail)) 1);
(= (list-find ((list 10) 17 14 17 8 6 1 2 12 10 4) 1 (example-fail)) 5);
(= (list-find ((list 4) 15 13 6 17) 14 (example-fail)) 100);
(= (list-find ((list 6) 16 13 10 3 0 19) 2 (example-fail)) 100);
(= (list-find ((list 8) 13 19 4 17 11 9 2 3) 15 (example-fail)) 100);
# the is-list function is now on dubious ground
# this stuff is being replaced with typing
(is-list ((list 2) 1 3));
(is-list ((list 0)));
(not (is-list 23));
(not (is-list (? x (+ (x) 10))));
(is-list ((list 3) ((list 2) 2 3) 1 (? x (+ (x) 10))));
# MATH introduce sets and set membership
(element 0 (set [6 1 3 0 7]));
(element 6 (set [6 1 3 0 7]));
(element 0 (set [6 1 3 0 7]));
(element 7 (set [8 1 7 9 2]));
(element 9 (set [8 1 7 9 2]));
(element 1 (set [8 1 7 9 2]));
(element 0 (set [6 0 3 7]));
(element 7 (set [6 0 3 7]));
(element 3 (set [6 0 3 7]));
(element 1 (set [1 0 9]));
(element 1 (set [1 0 9]));
(element 1 (set [1 0 9]));
(element 5 (set [1 3 5]));
(element 3 (set [1 3 5]));
(element 3 (set [1 3 5]));
(not (element 8 (set [3 7 5])));
(not (element 8 (set [4 5])));
(not (element 8 (set [3 9 2 5])));
(not (element 4 (set [0 3 9 5])));
(not (element 1 (set [4 3 7 9])));
(= (set [1 5 9]) (set [5 1 9]));
(= (set [1 5 9]) (set [9 1 5]));
(not (= (set [1 5 9]) (set [1 5])));
# let's go leave ourselves wide open to Russell's paradox
# ... by using characteristic functions
# ... since it doesn't really matter for communication purposes
(element 5 (all (? x (= (+ (x) 10) 15))));
(element 3 (all (? x (= (* (x) 3) (+ (x) 6)))));
(define empty_set (set []));
(element 0 (natural_set));
(forall (? x (=> (element (x) (natural_set)) (element (+ (x) 1) (natural_set)))));
(element 1 (natural_set));
(element 2 (natural_set));
(element 3 (natural_set));
(element 4 (natural_set));
(element 5 (natural_set));
(element 6 (natural_set));
(element 7 (natural_set));
(element 8 (natural_set));
(element 9 (natural_set));
(not (element (true) (natural_set)));
(not (element (false) (natural_set)));
(define boolean_set (set [(true) (false)]));
(element (true) (boolean_set));
(element (false) (boolean_set));
(not (element 0 (boolean_set)));
(define even_natural_set (all (? x (exists (? y (and (element (y) (natural_set)) (equals (* 2 (y)) (x))))))));
(element 0 (natural_set));
(element 0 (even_natural_set));
(element 1 (natural_set));
(not (element 1 (even_natural_set)));
(element 2 (natural_set));
(element 2 (even_natural_set));
(element 3 (natural_set));
(not (element 3 (even_natural_set)));
(element 4 (natural_set));
(element 4 (even_natural_set));
(element 5 (natural_set));
(not (element 5 (even_natural_set)));
(element 6 (natural_set));
(element 6 (even_natural_set));
# MATH build up functions of several variables
(= ((? x (? y (- (x) (y)))) 11 4) 7);
(= ((? x (? y (- (x) (y)))) 12 8) 4);
(= ((? x (? y (- (x) (y)))) 8 8) 0);
(= ((? x (? y (- (x) (y)))) 10 7) 3);
(= ((? x (? y (- (x) (y)))) 7 5) 2);
(intro lambda);
(= (? x (- (x) 5)) (lambda (x) (- (x) 5)));
(= (? x (? y (- (x) (y)))) (lambda (x y) (- (x) (y))));
(= ((lambda (x y) (- (x) (y))) 10 3) 7);
(= ((lambda (x y) (- (x) (y))) 4 0) 4);
(= ((lambda (x y) (- (x) (y))) 14 8) 6);
(= ((lambda (x y) (- (x) (y))) 13 6) 7);
(= ((lambda (x y) (- (x) (y))) 9 5) 4);
(define apply (lambda (x y) (if (= (y) (list)) (x) (apply ((x) (head (y))) (tail (y))))));
(= (apply (lambda (x y) (- (x) (y))) [11 6]) 5);
(= (apply (lambda (x y) (- (x) (y))) [14 9]) 5);
(= (apply (lambda (x y) (- (x) (y))) [5 1]) 4);
(= (apply (lambda (x y) (- (x) (y))) [8 3]) 5);
(= (apply (lambda (x y) (- (x) (y))) [13 9]) 4);
# MATH show map function for applying a function across the elements of a list
(define map (lambda (p lst) (if (> (list-length (lst)) 0) (prepend (p (head (lst))) (map (p) (tail (lst)))) [])));
(= (map (? x (* (x) 2)) [19 6 10]) [38 12 20]);
(= (map (? x (* (x) 2)) [4 9 2 10]) [8 18 4 20]);
(= (map (? x (* (x) 2)) [9 17 13 14 19]) [18 34 26 28 38]);
(= (map (? x (* (x) 2)) [11 10 5 8 1 14]) [22 20 10 16 2 28]);
(= (map (? x 42) [18 14 4]) [42 42 42]);
(= (map (? x 42) [6 16 11 8]) [42 42 42 42]);
(= (map (? x 42) [1 14 3 18 0]) [42 42 42 42 42]);
(= (map (? x 42) [6 17 13 16 10 1]) [42 42 42 42 42 42]);
(define crunch (lambda (p lst) (if (> (list-length (lst)) 2) (p (head (lst)) (crunch (p) (tail (lst)))) (if (= (list-length (lst)) 2) (head (lst)) (undefined)))));
(= (crunch + [14 15 13]) 42);
(= (crunch + [11 7 9 0]) 27);
(= (crunch + [6 16 8 5 2]) 37);
(= (crunch + [6 10 7 8 13 4]) 48);
# MATH introduce mutable objects, and side-effects
(intro make-cell);
(intro set!);
(intro get!);
(define demo-mut1 (make-cell 0));
(set! (demo-mut1) 15);
(= (get! (demo-mut1)) 15);
(set! (demo-mut1) 5);
(set! (demo-mut1) 7);
(= (get! (demo-mut1)) 7);
(define demo-mut2 (make-cell 11));
(= (get! (demo-mut2)) 11);
(set! (demo-mut2) 22);
(= (get! (demo-mut2)) 22);
(= (get! (demo-mut1)) 7);
(= (+ (get! (demo-mut1)) (get! (demo-mut2))) 29);
(if (= (get! (demo-mut1)) 7) (set! (demo-mut1) 88) (set! (demo-mut1) 99));
(= (get! (demo-mut1)) 88);
(if (= (get! (demo-mut1)) 7) (set! (demo-mut1) 88) (set! (demo-mut1) 99));
(= (get! (demo-mut1)) 99);
# MATH show how to execute a sequence of instructions
(intro begin);
(= (begin 1 7 2 4) 4);
(= (begin (set! (demo-mut1) 88) (set! (demo-mut1) 6) (get! (demo-mut1))) 6);
(= (begin (set! (demo-mut2) 88) (set! (demo-mut1) 6) (get! (demo-mut2))) 88);
(= (begin (set! (demo-mut1) 88) (set! (demo-mut1) 6) (get! (demo-mut1)) 4) 4);
# MATH introduce sugar for let
# if would be good to introduce desugarings more rigorously, but for now...
# ... just a very vague sketch
(intro let);
(= (let ((x 10)) (+ (x) 5)) ((? x (+ (x) 5)) 10));
(= (let ((x 10) (y 5)) (+ (x) (y))) (((? x (? y (+ (x) (y)))) 10) 5));
# MATH introduce environment/hashmap structure
# this section needs a LOT more examples :-)
# note that at the time of writing (h 1 2) is same as ((h) 1 2)
(define hash-add (lambda (h x y z) (if (= (z) (x)) (y) (h (z)))));
(define hash-ref (lambda (h x) (h (x))));
(define hash-null (? x (undefined)));
(define test-hash (hash-add (hash-add (hash-null) 3 2) 4 9));
(= (hash-ref (test-hash) 4) 9);
(= (hash-ref (test-hash) 3) 2);
(= (hash-ref (test-hash) 8) (undefined));
(= (hash-ref (test-hash) 15) (undefined));
(= (hash-ref (hash-add (test-hash) 15 33) 15) 33);
(= (hash-ref (test-hash) 15) (undefined));
(define make-hash (? x (= (x) (list)) (hash-null) (hash-add (make-hash (tail (x))) (first (head (x))) (second (head (x))))));
(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 3) 10);
(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 1) 30);
# MATH show a pattern matching mechanism
# just by example, not definition, for now
# it is a bit subtle to be relying on examples only.
# especially as few as there are right now.
(intro match);
(= ((match x (pair (true) 2) (pair (false) 3) (pair (true) (x))) 42) 2);
(= ((match x (pair (false) 3) (pair (true) (x)) (pair (true) 2)) 42) 42);
(= ((match x (pair (true) 2) (pair (false) 3) (pair (true) 4)) 42) 2);
(= ((match x (pair (false) 3) (pair (true) 4) (pair (true) 2)) 42) 4);
(define test-match1 (match x (pair (= (x) 42) 10) (? y (pair (and (= (x) (* (y) 2)) (element (y) (natural_set))) (y))) (pair (true) 3)));
(= (test-match1 42) 10);
(= (test-match1 100) 50);
(= (test-match1 30) 15);
(= (test-match1 33) 3);
(= (test-match1 39) 3);
# MATH introduce a basic type system
# not really sure how this is going to work out
# need to implement domain constructors T+T / T*T / T->T / etc
(intro type);
(define typed (? x ((match e (list (pair (element (e) (natural_set)) (pair integer (e))) (pair (element (e) (boolean_set)) (pair boolean (e))) (? T (pair (= (first (e)) (type (T))) (pair (T) (second (e))))) (? T (pair (crunch and (prepend (is-list (e)) (map (? x (= (first (typed (x))) (T))) (e)))) (pair (listof (T)) (e)))) (pair (is-list (e)) (pair (listof unknown) (e))) (pair (true) (pair (undefined) (e))))) (x))));
(define get-type (? x (first (typed (x)))));
(define get-raw (? x (second (typed (x)))));
(= (get-type 17) integer);
(= (get-type 8) integer);
(= (get-type 16) integer);
(= (get-type 0) integer);
(= (get-type 16) integer);
(forall (? x (=> (element (x) (natural_set)) (= (get-type (x)) integer))));
(= (get-type (true)) boolean);
(= (get-type (false)) boolean);
(= (get-type [1 4 5]) (listof integer));
(= (get-type [(true) (true) (false)]) (listof boolean));
# don't think I deal adequately with empty list at the moment
(= (typed 16) (type integer 16));
(= (typed 13) (type integer 13));
(= (typed 5) (type integer 5));
(= (typed (type integer 8)) (type integer 8));
(= (typed (type integer 6)) (type integer 6));
(= (typed (type integer 1)) (type integer 1));
(forall (? x (forall (? y (=> (and (= (get-type (x)) integer) (= (get-type (y)) integer)) (= (+ (x) (y)) (+ (get-raw (x)) (get-raw (y)))))))));
(= (+ (type integer 5) (type integer 10)) 15);
(define type-compatible-integer-primop (? op (forall (? x (forall (? y (=> (and (= (get-type (x)) integer) (= (get-type (y)) integer)) (= (op (x) (y)) (op (get-raw (x)) (get-raw (y)))))))))));
(type-compatible-integer-primop +);
(type-compatible-integer-primop *);
(type-compatible-integer-primop -);
(type-compatible-integer-primop =);
# note constraint to integers for now
(= (type integer 5) 5);
# There is a lot to add here to layer types over existing infrastructure.
# Let's just pretend it is here and doesn't involve any serious contradictions!
# give a typed version of lambda by example - really need to define this!
(= (lambda ((x integer) (y boolean)) (if (y) (x) 0)) (lambda (x y) (if (and (= (get-type (x)) integer) (= (get-type (y)) boolean)) (if (y) (x) 0) (undefined))));
# MATH introduce graph structures
# really need some type templating - will define this later
# type system needs a little bit of dis-ambiguating!
(pending template);
(define tuple (template (T) (lambda ((lst (listof (T)))) (type (tupleof (T) (list-length (lst))) (lst)))));
(define tuple-ref (template (T len) (lambda ((x (tupleof (T) (len))) (y integer)) (list-ref (get-raw (x)) (get-raw (y))))));
define make-graph (lambda ((nodes (listof integer)) (links (listof (tupleof integer 2)))) (type graph (tuple (list (nodes) (links)))));
(define test-graph (make-graph [g1 g2 g3 g4] (list (tuple [g1 g2]) (tuple [g2 g3]) (tuple [g1 g4]))));
(define graph-linked (lambda ((g graph) (n1 integer) (n2 integer)) (exists (? idx (= (tuple-ref (tuple-ref (g) 1) (idx)) (tuple (list (n1) (n2))))))));
(= (graph-linked (test-graph) g1 g2) (true));
(= (graph-linked (test-graph) g1 g3) (false));
(= (graph-linked (test-graph) g2 g4) (false));
(define graph-linked* (lambda (g n1 n2) (or (= (n1) (n2)) (or (graph-linked (g) (n1) (n2)) (exists (? n3 (and (graph-linked (g) (n1) (n3)) (graph-linked* (g) (n3) (n2)))))))));
(= (graph-linked* (test-graph) g1 g2) (true));
(= (graph-linked* (test-graph) g1 g3) (true));
(= (graph-linked* (test-graph) g2 g4) (false));
# OBJECT introduce simple mutable structures
(define mutable-struct (? lst (let ((data (map (? x (make-cell 0)) (lst)))) (? key (list-ref (data) (find-list (lst) (key)))))));
(define test-struct1 (mutable-struct [item1 item2 item3]));
(set! (test-struct1 item1) 15);
(= (get! (test-struct1 item1)) 15);
# OBJECT introduce method handler wrappers
define add-method (lambda (object name method) (hash-add (object) (name) (method (object))));
(define mutable-struct (? lst (let ((data (map (? x (make-cell 0)) (lst)))) (? key (list-ref (data) (find-list (lst) (key)))))));
(define test-struct2 (mutable-struct [x y]));
(set! (test-struct2 x) 10);
(set! (test-struct2 y) 20);
(= (get! (test-struct2 x)) 10);
(= (get! (test-struct2 y)) 20);
(define test-struct3 (add-method (test-struct2) sum (? self (+ (get! (self x)) (get! (self y))))));
(= (get! (test-struct3 x)) 10);
(= (get! (test-struct3 y)) 20);
(= (test-struct3 sum) 30);
(set! (test-struct3 y) 10);
(= (test-struct3 sum) 20);
(set! (test-struct2 y) 5);
(= (test-struct3 sum) 15);
# MUD under development
# currently just use this section to play around
(pending thing);
(define make-mud (lambda ((g graph) (t thing)) (let ((self (make-cell (mutable-struct [map stuff])))) (begin (set! ((get! (self)) map) (g)) (set! ((get! (self)) stuff) (t)) (set! (self) (add-method (get! (self)) get42 (? this 42))) (get! (self))))));
(define tpair (lambda (x y) (tuple [(x) (y)])));
(pending make-undirected-graph);
# the following map is not at all accurate!
# just something arbitrary to play with
# remember that none of the semantic info in names is captured in the message
(define cambridge-map (make-undirected-graph [mit-lobby-7 mit-lobby-10 mit-killian-court mit-student-center mit-26-100 mit-stata mit-tech-square mit-ashdown mit-green mit-media mit-medical mit-kendall-tstop mit-coop central-tstop harvard-tstop harvard-coop] (list (tpair mit-lobby-7 mit-lobby-10) (tpair mit-lobby-7 mit-student-center) (tpair mit-student-center mit-ashdown) (tpair mit-ashdown mit-lobby-7) (tpair mit-lobby-10 mit-killian-court) (tpair mit-lobby-10 mit-26-100) (tpair mit-26-100 mit-green) (tpair mit-green mit-media) (tpair mit-media mit-medical) (tpair mit-medical mit-kendall-tstop) (tpair mit-kendall-tstop mit-coop) (tpair mit-kendall-tstop central-tstop) (tpair central-tstop harvard-tstop) (tpair harvard-tstop harvard-coop))));