The informal description of the semantics in the SRFI describes the lazyversion of the hygiene algorithm. If I remember correctly, the original syntax-case paper described the algorithm in the first few sections as if it
were eager, only introducing the lazy version in a later section for efficiency.
Does the semantics depend on the laziness? This is not clear to me, but if not, the eager description may be easier to understand in the informal decription.
Regards Andre
