From b897751a3813840f08363f5ed47ec0f86368a48c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Wed, 22 Dec 2021 16:13:22 +0000
Subject: [PATCH] Note on reduction relation

---
 thesis.tex | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/thesis.tex b/thesis.tex
index 496e813..71df85f 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -6974,6 +6974,9 @@ exists some $N$ such that $M \reducesto N$.
   of the form $\Return\; V$ for some value $V \in \ValCat$.
 \end{definition}
 %
+We write $\reducesto^\ast$ for the reflexive and transitive closure of
+the reduction relation $\reducesto$.
+%
 \begin{theorem}[Progress]\label{thm:base-language-progress}
   Suppose $\typ{}{M : C}$, then $M$ is normal or there exists
   $\typ{}{N : C}$ such that $M \reducesto^\ast N$.