Introduction

This is the rendered supplement to the paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language". It contains

• a reference implementation of the described do extensions using the Lean 4 macro system (lightly commented)
• a Lean formalization of the translation function, the static and dynamic semantics, and the equivalence proof described in the paper in literate style