From 087f6f027741728f4dd3d2455261c3546d9ebd33 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 9 Jun 2020 11:36:10 +0100 Subject: Add another comment --- main.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'main.tex') diff --git a/main.tex b/main.tex index a988a1f..b3c9846 100644 --- a/main.tex +++ b/main.tex @@ -222,7 +222,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{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.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} +\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.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.} \begin{align} \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\ -- cgit