I construct functions 🎉 math-old : mathematics typeset in $\LaTeX$ GlowCoon : demonstration of refinement in TLA+