-- define one of put_, put. Use of put_ is recommended because it
-- is more likely that tail-calls can kick in, and we rarely need the
-- position return value.
-- define one of put_, put. Use of put_ is recommended because it
-- is more likely that tail-calls can kick in, and we rarely need the
-- position return value.