MicroKanren - what are the terms?

Question

Having a little trouble understanding the core terms of the MicroKanren DSL. Section 4 says:

Terms of the language are defined by the unify operator. Here, terms of the language consist of variables, objects deemed identical under eqv?, and pairs of the foregoing.

But they never describe what the "pairs" actually mean. Are the pairs supposed to represent equality of two subterms, like so:

type 'a ukanren = KVar of int | KVal of 'a | KEq of 'a kanren * 'a kanren

So a term like:

(call/fresh (λ (a) (≡ a 7)))

Generates a pair for (≡ a 7)?

Edit: upon further thought, I don't think this is it. The mentions of "pair" in the paper seem to come much later, with extensions and refinements to the basic system, which would mean the pairs have no meaning in the terms for the basic intro. Is this correct?

Answer 1

In this context, "pair" just means a cons pair, such as (5 . 6) or (foo . #t). An example unification between two pairs is:

(call/fresh
  (λ (a)
    (call/fresh
      (λ (b)
        (≡ (cons a b) (cons 5 6))))))

which associates a with 5 and b with 6.