<div dir="ltr">Thank you to Wolfram and Nils!<div><br></div><div>Wolfram's suggestion worked!</div><div><br></div><div>Nils's suggestions C-u C-c C-n is great for testing, but doesn't help if I want to document the results of the test in the file. I'm writing a textbook, so including examples in the file is important! It would also be important if one wanted to include tests for documentation and reliability.<br></div><div><br></div><div>Nils's suggestion to disable reduction with () is neat, but possibly not the best pedagogy for a textbook.</div><div><div><br></div><div><blockquote class="gmail_quote" style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">However, there is no way to<br></span><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">turn off abstract while type-checking (because this could lead to<br></span><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">problems with subject reduction).</span></blockquote><div><br></div><div>So, I have an equality that is proved under abstraction, that fails when the abstraction is removed. Isn't that also a failure of subject reduction, or stability under substitution, or some other important property that we care about?</div><div><br></div><div>Cheers, -- P</div><br class="gmail-Apple-interchange-newline"><br></div><br></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 16 May 2018 at 02:52, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-05-16 00:27, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there any way to *both* be able to compute fresh names *and* retain<br>
my related proofs, in particular, the proof that `fresh x xs`<br>
generates a name not in `xs`?<br>
</blockquote>
<br></span>
When normalising an expression you can make abstract definitions compute<br>
by using C-u C-c C-n instead of C-c C-n. However, there is no way to<br>
turn off abstract while type-checking (because this could lead to<br>
problems with subject reduction).<br>
<br>
There are other ways to control reduction. Wolfram suggested one.<br>
Another is to match on a value of the unit type, and not supply a<br>
concrete constructor until you want the code to compute.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>