From 0618ca6ac08311a1325cb1860d8078ddfdb9dac0 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 5 Jun 2020 19:02:07 +0100
Subject: Add a comment to recursive definitions

---
 main.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index 5fe26c7..4e2dfb9 100644
--- a/main.tex
+++ b/main.tex
@@ -217,7 +217,7 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.}
 
-\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.}
+\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now.  One more thing I noticed though is that recursive definitions will need an \texttt{option} type.}
 
 \begin{align}
     \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\
-- 
cgit 

