diff --git a/implementations/SWIProlog/eval_joy_ast b/implementations/SWIProlog/eval_joy_ast
new file mode 100755
index 0000000..ea19de5
Binary files /dev/null and b/implementations/SWIProlog/eval_joy_ast differ
diff --git a/implementations/SWIProlog/eval_joy_ast.prolog b/implementations/SWIProlog/eval_joy_ast.prolog
index e6f7392..e6a5970 100644
--- a/implementations/SWIProlog/eval_joy_ast.prolog
+++ b/implementations/SWIProlog/eval_joy_ast.prolog
@@ -103,20 +103,18 @@ assert_def(Symbol, Body) :-
 foo(Var, Name=Var) :- gensym('A', Name).
 
 
-barzs([], []).
-barzs([Var|Bs], [(Name=Var)|Ls]) :-
+names_for_variables([], []).
+names_for_variables([Var|Bs], [(Name=Var)|Ls]) :-
     gensym('A', Name),
-    barzs(Bs, Ls).
+    names_for_variables(Bs, Ls).
 
 main :-
     read_term(Expression, []),
     thun(Expression, Si, So),
-    term_variables((Si, So), L),
-    barzs(L, LL),
-    %write_canonical(LL), writeln(""),
-    write_term(Si, [quoted(true),fullstop(true),variable_names(LL)]),
-    write_term(So, [quoted(true),fullstop(true),variable_names(LL)]),
-    writeln("").
+    term_variables((Si, So), Vars),
+    names_for_variables(Vars, Names),
+    write_term(Si, [quoted(true),variable_names(Names)]), writeln(","),
+    write_term(So, [quoted(true),variable_names(Names)]), writeln("").
     
     
     
diff --git a/implementations/SWIProlog/f.joyast b/implementations/SWIProlog/f.joyast
new file mode 100644
index 0000000..019f698
--- /dev/null
+++ b/implementations/SWIProlog/f.joyast
@@ -0,0 +1 @@
+[symbol(clear),list([symbol(base),int(2147483648)])].
diff --git a/implementations/SWIProlog/joy_to_ast.prolog b/implementations/SWIProlog/joy_to_ast.prolog
index 6e1a146..70c407d 100644
--- a/implementations/SWIProlog/joy_to_ast.prolog
+++ b/implementations/SWIProlog/joy_to_ast.prolog
@@ -34,8 +34,15 @@ joy_term(list(J)) --> [lbracket], !, joy_parse(J), [rbracket].
 joy_term(Token) --> [tok(Codes)], {joy_token(Token, Codes)}.
 
 joy_token(int(I), Codes) :- catch(number_codes(I, Codes), _Err, fail), !.
-joy_token(bool(true), "true") :- !.
-joy_token(bool(false), "false") :- !.
+% Leaving the literals below as "true" and "false" caused those
+% to be encoded as symbols instead of bools!  I tried '--traditional'
+% but then compilation failed with
+% > ERROR: atomics_to_string/3: Type error: `text' expected, found `[61]' (a list)
+% Which was less helpful than it sounds.
+% Anyway, since this is SWI-specific code anyway, why not use ``'s and get on with life?
+% https://www.swi-prolog.org/pldoc/man?section=string
+joy_token(bool(true), `true`) :- !.
+joy_token(bool(false), `false`) :- !.
 joy_token(symbol(S), Codes) :- atom_codes(S, Codes).
 
 text_to_expression(Text, Expression) :-
diff --git a/implementations/check_against_defs.txt b/implementations/check_against_defs.txt
new file mode 100644
index 0000000..d1170ee
--- /dev/null
+++ b/implementations/check_against_defs.txt
@@ -0,0 +1,213 @@
+
+██╗     ██╗██████╗ ██████╗  █████╗ ██████╗ ██╗   ██╗
+██║     ██║██╔══██╗██╔══██╗██╔══██╗██╔══██╗╚██╗ ██╔╝
+██║     ██║██████╔╝██████╔╝███████║██████╔╝ ╚████╔╝
+██║     ██║██╔══██╗██╔══██╗██╔══██║██╔══██╗  ╚██╔╝
+███████╗██║██████╔╝██║  ██║██║  ██║██║  ██║   ██║
+╚══════╝╚═╝╚═════╝ ╚═╝  ╚═╝╚═╝  ╚═╝╚═╝  ╚═╝   ╚═╝
+
+
+Start with increment and decrement:
+
+    -- ≡ 1 -
+    ++ ≡ 1 +
+
+Common symbols for operations:
+
+    = ≡ eq
+    + ≡ add
+    > ≡ gt
+    < ≡ lt
+    >= ≡ ge
+    <= ≡ le
+    != ≡ ne
+    <> ≡ ne
+
+    % ≡ mod
+    + ≡ add
+    - ≡ sub
+    * ≡ mul
+    / ≡ floordiv
+    div ≡ floordiv
+
+    & ≡ and
+    | ≡ or
+    ! ≡ not
+
+    << ≡ lshift
+    >> ≡ rshift
+
+
+• ≡
+
+
+? ≡ dup bool
+
+
+&& ≡ nulco [nullary [false]] dip branch
+|| ≡ nulco [nullary] dip [true] branch
+
+
+!- ≡ 0 >=
+
+<{} ≡ [] swap
+<<{} ≡ [] rollup
+
+abs ≡ dup 0 < [] [neg] branch
+
+anamorphism ≡ [pop []] swap [dip swons] genrec
+
+app1 ≡ grba infrst
+app2 ≡ [grba swap grba swap] dip [infrst] cons ii
+app3 ≡ 3 appN
+appN ≡ [grabN] codi map reverse disenstacken
+
+at ≡ drop first
+
+b ≡ [i] dip i
+dipd ≡ [dip] codi
+genrec ≡ [[genrec] ccccons] nullary swons concat ifte
+tailrec ≡ [i] genrec
+ifte ≡ [nullary] dipd swap branch
+ii ≡ [dip] dupdip i
+infra ≡ swons swaack [i] dip swaack
+x ≡ dup i
+pam ≡ [i] map
+
+
+    nullary ≡ [stack] dip infra first
+    unary ≡ nullary popd
+    binary ≡ unary popd
+    ternary ≡ binary popd
+
+ccccons ≡ ccons ccons
+ccons ≡ cons cons
+
+clear ≡ [] swaack pop
+
+cleave ≡ fork popdd
+clop ≡ cleave popdd
+fork ≡ [i] app2
+
+cmp ≡ [[>] swap] dipd [ifte] ccons [=] swons ifte
+
+codi ≡ cons dip
+codireco ≡ codi reco
+
+dinfrirst ≡ dip infrst
+
+
+disenstacken ≡ ? [uncons ?] loop pop
+enstacken ≡ stack [clear] dip
+
+down_to_zero ≡ [0 >] [dup --] while
+
+drop ≡ [rest] times
+
+dupd ≡ [dup] dip
+dupdd ≡ [dup] dipd
+dupdip ≡ dupd dip
+dupdipd ≡ dup dipd
+
+
+      rest ≡ uncons popd
+     first ≡ uncons pop
+    second ≡ rest first
+     third ≡ rest second
+    fourth ≡ rest third
+
+
+flatten ≡ <{} [concat] step
+
+gcd ≡ true [tuck mod dup 0 >] loop pop
+
+
+grabN ≡ <{} [cons] times
+grba ≡ [stack popd] dip
+
+hypot [sqr] ii + sqrt
+
+infrst ≡ infra first
+
+make_generator ≡ [codireco] ccons
+
+manual ≡ [] words [help] step pop
+
+neg ≡ 0 swap -
+not ≡ [true] [false] branch
+
+nulco ≡ [nullary] cons
+of ≡ swap at
+
+over ≡ [dup] dip swap
+
+pm ≡ [+] [-] clop
+
+popd ≡ [pop] dip
+popdd ≡ [pop] dipd
+popop ≡ pop pop
+popopop ≡ pop popop
+popopd ≡ [popop] dip
+popopdd ≡ [popop] dipd
+
+product ≡ 1 swap [*] step
+
+quoted ≡ [unit] dip
+
+range ≡ [0 <=] [1 - dup] anamorphism
+range_to_zero ≡ unit [down_to_zero] infra
+
+reco ≡ rest cons
+
+
+reverse ≡ <{} shunt
+
+roll> ≡ swap swapd
+roll< ≡ swapd swap
+rollup ≡ roll>
+rolldown roll<
+
+rrest ≡ rest rest
+
+run ≡ <{} infra
+shift ≡ uncons [swons] dip
+shunt ≡ [swons] step
+size ≡ [pop ++] step_zero
+spiral_next ≡ [[[abs] ii <=] [[<>] [pop !-] ||] &&] [[!-] [[++]] [[--]] ifte dip] [[pop !-] [--] [++] ifte] ifte
+split_at ≡ [drop] [take] clop
+split_list ≡ [take reverse] [drop] clop
+sqr ≡ dup *
+stackd ≡ [stack] dip
+step_zero ≡ 0 roll> step
+stuncons ≡ stack uncons
+sum ≡ [+] step_zero
+swapd ≡ [swap] dip
+swons ≡ swap cons
+swoncat ≡ swap concat
+sqr ≡ dup mul
+take ≡ <<{} [shift] times pop
+tuck ≡ dup swapd
+uncons ≡ [first] [rest] cleave
+unit ≡ [] cons
+unquoted ≡ [i] dip
+unswons ≡ uncons swap
+while ≡ swap nulco dupdipd concat loop
+
+step ≡ [_step0] x
+_step0 ≡ _step1 [popopop] [_stept] branch
+_step1 ≡ [?] dipd roll<
+_stept ≡ [uncons] dipd [dupdipd] dip x
+
+times ≡ [_times0] x
+_times0 ≡ _times1 [popopop] [_timest] branch
+_times1 ≡ [dup 0 >] dipd roll<
+_timest ≡ [[--] dip dupdipd] dip x
+
+map ≡ [_map0] cons [[] [_map?] [_mape]] dip tailrec
+_map? ≡ pop bool not
+_mape ≡ popd reverse
+_map0 ≡ [_map1] dipd _map2
+_map1 ≡ stackd shift
+_map2 ≡ [infrst] cons dipd roll< swons
+
+