...although the mkStuff way of writing things is ugly in one way: it means that if you want to desugar quotes inside quotes, you may need to introduce mkMkStuff functions, as in,

"x = 'a + #[y]'" = "x = mkPlus('a', y)" = mkEq('x', mkMkPlus(repr('a'), 'y')).

(Recall that 'a' denotes the Gödel number of the variable a; repr('a') is the Gödel number of an expression that evaluates to the Gödel number of a, which is what we need in that place.)

It would be better to introduce functions call(name,arg) and pair(x,y) such that

mkRepr(x) = call('repr', x)
mkEq(x,y) = call('eq', pair(x,y))
mkSubst(x,y) = call('subst', pair(x,y))

etc. Then we can apply the desugaring recursively--

"'repr(x)'" = "call('repr', 'x')" = call('call', pair(repr('repr'), repr('x'))).

HTH more than it confuses :-/