   nil
   (walk [u s] nil))
 
-(defn unify [u v s]
+;; # Unification
+
+(defn unify
+  "Given two terms *u* and *v*, and an existing substitution map *s*,
+  unify produces a new substitution map with mappings that will make u
+  and v equal."
+  [u v s]
   (let [u (walk u s),  v (walk v s)
         ulv (lvar? u), vlv (lvar? v)]
     (cond

(ns micro-logic.core
  (:require [micro-logic.protocols :refer :all]))

;;; Variable defs
;;; c: lvar id
;;; s: substitution map
;;; u, v: either literal values or logic variables.

(defrecord LVar [c])
(defn lvar [c] (LVar. c))
(defn lvar? [x] (= LVar (class x)))

(extend-protocol IWalk
  LVar
  (walk [u s] (if-let [val (get s u)]
                (walk val s)
                u))

      (= u v) s
      :default (unify-terms u v s))))

;; This unifier is extensible, in the spirit of core.logic. Only
;; unification on basic types is directly implemented here. By
;; extending the IUnifyTerms protocol, special unification logic may
;; be supplied for any data type.
;;
;; A *term* is, somewhat circularly, something you can pass to the unifier.
;; this includes lvars, regular values, and values of any type to which
;; you have extended IUnifyTerms.
(extend-protocol IUnifyTerms
  Object
  (unify-terms [u v s]
