From 08dfeb4f740f6431d199808ebed3f4cd11ef2674 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 6 Jun 2023 15:35:50 -0400
Subject: [PATCH] formalism: Add brief description for untyped action calculus

---
 formalism/untyped.tex | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/formalism/untyped.tex b/formalism/untyped.tex
index cd5822e..62ded55 100644
--- a/formalism/untyped.tex
+++ b/formalism/untyped.tex
@@ -7,6 +7,14 @@
 
 \section{Untyped hazelnut}
 \label{sec:untyped}
+In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be
+layered with the marked lambda calculus to yield a structure editing calculus that supports
+non-local hole fixes.
+
+In comparison with the original calculus, this untyped version is not concerned at all with typing
+but only the manipulation of syntax. As such, the action judgments are simplified considerably; in
+particular, they are no longer bidirectional. The same core metatheorems, except sensibility which
+is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}).
 
 \subsection{Syntax}
 \label{sec:untyped-syntax}
@@ -640,8 +648,6 @@ \subsubsection{Iterated actions}
 
 \subsection{Metatheorems}
 \label{sec:untyped-metatheorems}
-\begin{theorem}[name=Sensibility]
-\end{theorem}
 
 \begin{theorem}[name=Movement Erasure Invariance] \
   \begin{enumerate}