Hey @holguinj,

I'm working through the appendix in the Little Prover, and the first few examples aren't simplifying for me. It looks like some issue with the paths code. I ran the following snippets in clj-bob.repl.

This works great:

(J-Bob-step (prelude)
            '(car (cons 'ham '(cheese)))
            '((() (car-cons 'ham '(cheese)))))

The code returns 'ham, as expected. Once I add a path in to a new focus, however, the simplification rules stop working:

(J-Bob-step (prelude)
            '(equal 'flapjack (atom (cons a b)))
            '(((2) (atom-cons a b))
              (() (equal 'flapjack 'nil))))

This code just returns the original expression, '(equal 'flapjack (atom (cons a b))). If I replace the (2) with an empty list and un-nest the (atom ,,,) snippet, that section gets simplified to nil.

Same problem with the second example:

(J-Bob-step (prelude)
            '(atom (cdr (cons (car (cons p q)) '())))
            '(((1 1 1) (car-cons p q))
              ((1) (cdr-cons p '()))
              (() (atom '()))))

Even a single step with a path specified seems to fail. Am I missing something obvious here?

Thanks so much for the awesome port!