<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg <span dir="ltr">&lt;<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
<br>
On Apr 8, 2013, at 3:12 PM, Paul Brauner &lt;<a href="mailto:polux2001@gmail.com">polux2001@gmail.com</a>&gt; wrote:<br>
<br>
&gt; from the output of -ddump-splices I dont think it is the case but I&#39;m asking anyway: is there any way to deduce a ~ b from a :==: b?<br>
<br>
</div>Not easily. You would have to write a (potentially recursive) function that explicitly matches singleton constructors, similarly to what you wrote. (You could say that this function is a (potentially inductive) proof that the generated definition of :==: is correct.) </blockquote>

<div><br></div><div style>Ok.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I agree that this is boilerplate and could easily be generated. I&#39;ve added it to the list of features to be included in the next version of singletons. I&#39;m surprised myself that it hasn&#39;t occurred to me to include this before.<br>


<span class="HOEnZb"><font color="#888888"><br></font></span></blockquote><div><br></div><div style>Great!</div><div style><br></div><div style>Paul</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<span class="HOEnZb"><font color="#888888">
Richard<br>
<br>
<br>
</font></span></blockquote></div><br></div></div>