diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-05 19:02:07 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-05 19:02:07 +0100 |
commit | 0618ca6ac08311a1325cb1860d8078ddfdb9dac0 (patch) | |
tree | e2293cefa392a30093250707e79ff1eaab53a88b /main.tex | |
parent | 73a733bb9f1aaef6c28bfe120361ba87b34455b8 (diff) | |
download | oopsla21_fvhls-0618ca6ac08311a1325cb1860d8078ddfdb9dac0.tar.gz oopsla21_fvhls-0618ca6ac08311a1325cb1860d8078ddfdb9dac0.zip |
Add a comment to recursive definitions
Diffstat (limited to 'main.tex')
-rw-r--r-- | main.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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\\ |